Coupled Similarity and Contrasimilarity, and How to Compute Them

We survey and extend characterizations of coupled similarity and contrasimilarity and prove properties relevant for algorithms computing their simulation preorders and equivalences.

Coupled similarity and contrasimilarity are two weak forms of bisimilarity for systems with internal behavior. They have outstanding applications in contexts where internal choices must transparently be distributed in time or space, for example, in process calculi encodings or in action refinements.

Our key contribution is to characterize the coupled simulation and contrasimulation preorders by reachability games. We also show how preexisting definitions coincide and that they can be reformulated using coupled delay simulations. We moreover verify a polynomial-time coinductive fixed-point algorithm computing the coupled simulation preorder. Through reduction proofs, we establish that deciding coupled similarity is at least as complex as computing weak similarity; and that contrasimilarity checking is at least as hard as trace inclusion checking.