Computing Coupled Similarity

Abstract

Coupled similarity is a notion of equivalence for systems with internal actions. It has 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. No tractable algorithms for the computation of coupled similarity have been proposed up to now. Accordingly, there has not been any tool support. We present a game-theoretic algorithm to compute coupled similarity , running in cubic time and space with respect to the number of states in the input transition system. We show that one cannot hope for much better because deciding the coupled simulation preorder is at least as hard as deciding the weak simulation preorder. Our results are backed by an Isabelle/HOL formalization, as well as by a parallelized implementation using the Apache Flink framework. Data or code related to this paper is available at: [ 2 ].