Minimization Algorithm for Symbolic Bisimilarity

The operational semantics of interactive systems is usually decsribed by labeled transition systems. Abstract semantics is defined in terms of bisimilarity, that in the finite case, can be computed via the well-known partition refinement algorithm. However, the behavoiur of interactive systems is in many case infinite and thus checking bisimilarity in this way is unfeasible. Symbolic semantics allows to define smaller, possibly finite, transition systems, by employing symbolic actions and avoiding some source of infiniteness. Unfortunately, the standard partition refinement algorithm does not work with symbolic bisimilarity. In a previous paper, we have introduced an abstract theory of symbolic semantics. In this paper, we introduce a partition refinement algorithm for symbolic bisimilarity.