Verification by abstraction and bisimulation

The ACP Bisimulation Tool is an implementation of an action relation model for the algebraic process theory ACP_r.In the action relation model processes are denoted by process expressions. A transition system is associated with each process expression through a set of inductive transition rules; the semantics of the model are the transition systems modulo bisimulation equivalence.It is shown how the verification of a system property can be expressed as a bisimulation decision problem with abstraction, enabling automated proof with the ACP Bisimulation Tool. Verification of mutual exclusion is considered as an example.It is known that in ACP_r all computable processes are finitely expressible, hence all computable finite state models can be finitely represented in ACP_r. Thus a finite state process model called the Selection/Resolution model is shown to be contained in ACP_r by a translation [.] from S/R processes to ACP_r process expressions.