Abstract
Boolean equation systems (BESs) have been used to encode several complex verification problems, including model checking and equivalence checking. We introduce the concepts of strong bisimulation and idempotence-identifying bisimulation for BESs, and we prove that these can be used for minimising BESs prior to solving these. Our results show that large reductions of the BESs may be obtained efficiently. Minimisation is rewarding for BESs with non-trivial alternations: the time required for solving the original BES mostly exceeds the time required for quotienting plus the time for solving the quotient. Furthermore, we provide a verification example that demonstrates that bisimulation minimisation of a process prior to encoding the verification problem on that process as a BES can be arbitrarily less effective than minimising the BES that encodes the verification problem.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Chen, T., Ploeger, B., van de Pol, J., Willemse, T.A.C.: Equivalence checking for infinite systems using Parameterized Boolean Equation Systems. In: Caires, L., Li, L. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 120–135. Springer, Heidelberg (2007)
Fisler, K., Vardi, M.Y.: Bisimulation minimization and symbolic model checking. Formal Methods in System Design 21(1), 39–78 (2002)
Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 182–196. Springer, Heidelberg (2009)
Fritz, C., Wilke, T.: Simulation relations for alternating parity automata and parity games. In: Ibarra, O.H., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 59–70. Springer, Heidelberg (2006)
Groote, J.F., Willemse, T.A.C.: Parameterised Boolean Equation Systems. Theor. Comput. Sci. 343(3), 332–369 (2005)
Jurdziński, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)
Katoen, J.-P., Kemna, T., Zapreev, I.S., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007)
Keiren, J., Willemse, T.A.C.: Bisimulation minimisations for boolean equation systems. Technical Report CSR09-17, Eindhoven University of Technology (2009)
Mader, A.: Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, Technische Universität München (1997)
Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008)
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6) (1987)
Reniers, M.A., Willemse, T.A.C.: Analysis of Boolean equation systems through structure graphs. In: Proc. of SOS 2009. EPTCS (2009) (to appear)
Blom, S., Orzan, S.: Distributed state space minimization. Int. J. STTTÂ 7(3) (2005)
Schewe, S.: Solving parity games in big steps. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 449–460. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Keiren, J.J.A., Willemse, T.A.C. (2011). Bisimulation Minimisations for Boolean Equation Systems. In: Namjoshi, K., Zeller, A., Ziv, A. (eds) Hardware and Software: Verification and Testing. HVC 2009. Lecture Notes in Computer Science, vol 6405. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19237-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-19237-1_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19236-4
Online ISBN: 978-3-642-19237-1
eBook Packages: Computer ScienceComputer Science (R0)