Minimization Algorithm for Symbolic Bisimilarity

The operational semantics of interactive systems is usually d 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 behaviour of interactive systems is in many cases 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 sources of infiniteness. Unfortunately, the standard partition refinement algorithm does not work with symbolic bisimilarity.

• Type: Conference
• Year: 2009
• Where: ESOP
• Authors: Filippo Bonchi, Ugo Montanari
• Keywords: ESOP 2009, Interactive Systems, Partition Refinement Algorithm, Programming Languages, Transition Systems