Abstract
We apply the saturation heuristic to the bisimulation problem for deterministic discrete-event models, obtaining the fastest to date symbolic bisimulation algorithm, able to deal with large quotient spaces. We compare performance of our algorithm with that of Wimmer et al., on a collection of models. As the number of equivalence classes increases, our algorithm tends to have improved time and space consumption compared with the algorithm of Wimmer et al., while, for some models with fixed numbers of state variables, our algorithm merely produced a moderate extension of the number of classes that could be processed before succumbing to state-space explosion. We conclude that it may be possible to solve the bisimulation problem for systems having only visible deterministic transitions (e.g., Petri nets where each transition has a distinct label) even if the quotient space is large (e.g., 109 classes), as long as there is strong event locality.
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.
References
Aczel, P.: Non-Well-Founded Sets. CSLI, Stanford (1988)
Bouali, A., Simone, R.D.: Symbolic bisimulation minimisation. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 96–108. Springer, Heidelberg (1993)
Chung, M.Y., Ciardo, G., Yu, A.J.: A fine-grained fullness-guided chaining heuristic for symbolic reachability analysis. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 51–66. Springer, Heidelberg (2006)
Ciardo, G., et al.: SMART: Stochastic Model checking Analyzer for Reliability and Timing, User Manual, http://www.cs.ucr.edu/~ciardo/SMART/
Dolev, D., Klawe, M., Rodeh, M.: An O(n logn) unidirectional distributed algorithm for extrema finding in a circle. J. of Algorithms 3(3), 245–260 (1982)
Dovier, A., Piazza, C., Policriti, A.: An efficient algorithm for computing bisimulation equivalence. Theor. Comput. Sci. 311, 221–256 (2004)
Graf, S., Steffen, B., Lüttgen, G.: Compositional minimisation of finite state systems using interface specifications. Journal of Formal Aspects of Computing 8(5), 607–616 (1996)
Milner, R.: Communication and concurrency. Prentice-Hall, Inc., NJ (1989)
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Journal of Computing 16, 973–989 (1987)
Paige, R., Tarjan, R.E., Bonic, R.: A linear time solution to the single function coarsest partition problem. Theoretical Computer Science 40, 67–84 (1985)
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Tilgner, M., Takahashi, Y., Ciardo, G.: SNS 1.0: Synchronized Network Solver. In: 1st Int. Workshop on Manuf. & Petri Nets, Osaka, Japan, pp. 215–234 (June 1996)
Wan, M., Ciardo, G.: Symbolic state-space generation of asynchronous systems using extensible decision diagrams. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tůma, P., Valencia, F. (eds.) SOFSEM 2009. LNCS, vol. 5404, pp. 582–594. Springer, Heidelberg (2009)
Wimmer, R., Herbstritt, M., Becker, B.: Forwarding, splitting, and block ordering to optimize BDD-based bisimulation computation. In: Haubelt, C., Teich, J. (eds.) Proceedings of the 10th GI/ITG/GMM-Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pp. 203–212. Shaker Verlag, Erlangen (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
Mumme, M., Ciardo, G. (2011). A Fully Symbolic Bisimulation Algorithm. In: Delzanno, G., Potapov, I. (eds) Reachability Problems. RP 2011. Lecture Notes in Computer Science, vol 6945. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24288-5_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-24288-5_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24287-8
Online ISBN: 978-3-642-24288-5
eBook Packages: Computer ScienceComputer Science (R0)