Scalable Minimization Algorithm for Partial Bisimulation

J. Markovski
(Eindhoven University of Technology)

We present an efficient algorithm for computing the partial bisimulation preorder and equivalence for labeled transitions systems. The partial bisimulation preorder lies between simulation and bisimulation, as only a part of the set of actions is bisimulated, whereas the rest of the actions are simulated. Computing quotients for simulation equivalence is more expensive than for bisimulation equivalence, as for simulation one has to account for the so-called little brothers, which represent classes of states that can simulate other classes. It is known that in the absence of little brother states, (partial bi)simulation and bisimulation coincide, but still the complexity of existing minimization algorithms for simulation and bisimulation does not scale. Therefore, we developed a minimization algorithm and an accompanying tool that scales with respect to the bisimulated action subset.

In César Andrés and Luis Llana: Proceedings 2nd Workshop on Formal Methods in the Development of Software (WS-FMDS 2012), Paris, France, August 28, 2012, Electronic Proceedings in Theoretical Computer Science 86, pp. 9–16.
Published: 8th July 2012.

ArXived at: http://dx.doi.org/10.4204/EPTCS.86.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org