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.

, , ,
Software Engineering [SEN]

Bergstra, J.A, Ponse, A, & van der Zwaag, M.B. (2000). Branching time and orthogonal bisimulation equivalence. Software Engineering [SEN]. CWI.