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.