Branching time and orthogonal bisimulation equivalence
We propose a refinement of branching bisimulation equivalence that we call orthogonal bisimulation equivalence. Typically, internal activity (i.e., the performance of $tau$-steps) may be compressed, but not completely discarded. Hence, a process with $tau$-steps cannot be equivalent to one without $tau$-steps. Also, we present a modal characterization of orthogonal bisimulation equivalence. This equivalence is a congruence for ACP extended with abstraction and priority operations. We provide a complete axiomatization, and describe some expressiveness results. Finally, we present the verification of a PAR protocol that is specified with use of priorities.
|Semantics (msc 68Q55), Specification and verification (program logics, model checking, etc.) (msc 68Q60), Algebraic theory of languages and automata (msc 68Q70), Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (msc 68Q85)|
|Software Engineering [SEN]|
Bergstra, J.A, Ponse, A, & van der Zwaag, M.B. (2000). Branching time and orthogonal bisimulation equivalence. Software Engineering [SEN]. CWI.