×

zbMATH — the first resource for mathematics

Rank-based symbolic bisimulation: (and model checking). (English) Zbl 1261.68084
de Queiroz, Ruy (ed.) et al., WoLLIC’2002. Proceedings of the 9th workshop on logic, language, information and computation, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio), Rio de Janeiro, Brazil, July 30–August 2, 2002. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 67, 166-183 (2002).
Summary: In this paper we propose an efficient symbolic algorithm for the problem of determining the maximum bisimulation on a finite structure. The starting point is an algorithm, on explicit representation of graphs, which saves both time and space exploiting the notion of rank. This notion provides a layering of the input model and allows to proceed bottom-up in the bisimulation computation. In this paper we give a procedure that allows to compute the rank of a graph working on its symbolic representation and requiring a linear number of symbolic steps. Then we embed it in a fully symbolic, rank-driven, bisimulation algorithm. Moreover, we show how the notion of rank can be employed to optimize the CTL model checking procedures.
For the entire collection see [Zbl 1109.03311].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
05C85 Graph algorithms (graph-theoretic aspects)
68Q25 Analysis of algorithms and problem complexity
Software:
CUDD
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aczel., P., “Non-well-founded sets.” Lecture Notes, Center for the Study of Language and Information 14, Stanford, 1988. · Zbl 0668.04001
[2] Akers, S.B., Binary decision diagrams, IEEE transaction on computers, 27, 509-516, (1978) · Zbl 0377.94038
[3] Bloem R., H. N. Gabow and F. Somenzi, An algorithm for strongly connected component analysis in n log n symbolic steps, in: W. A. Hunt Jr. and S. D. Johnson, editors, Proc. of Int. Conference on Formal Methods in Computer-Aided Design (FMCAD’00), LNCS \bf1954 (2000), pp. 37-54. · Zbl 1110.68161
[4] Bouajjani A., J. C. Fernandez and N. Halbwachs, Minimal model generation, in: E. M. Clarke and R. Kurshan, editors, Proc. Int’l Conference on Computer-Aided Verification CAV90, LNCS \bf531 (1990), pp. 197-203. · Zbl 0765.68114
[5] Bouali A. and R. de Simone, Symbolic bisimulation minimization, in: Proc. Int’l Conference on Computer-Aided Verification CAV92, LNCS \bf663 (1992), pp. 96-108.
[6] Bryant, R. E., Symbolic manipulation of boolean functions using a graphical representation, in: Proc. 22nd Design Automation Conference, 1985.
[7] Bryant, R.E., Graph based algorithms for Boolean function manipulation, IEEE trans. on computers, C-35, 677-691, (1986) · Zbl 0593.94022
[8] Clarke, E.M.; Grumberg, O.; Peled, D.A., “model checking”, (1999), MIT Press
[9] Dovier A., C. Piazza and A. Policriti, A fast bisimulation algorithm, in: G. Berry, H. Comon and A. Finkel, editors, Proc. of Int. Conference on Computer Aided Verification (CAV’01), LNCS \bf2102 (2001), pp. 79-90. · Zbl 0991.68553
[10] Fisler K. and M. Y. Vardi, Bisimulation and model checking, in: Proc. Correct Hardware Design and Verification Methods, LNCS \bf1703 (1999), pp. 338-341.
[11] Hopcroft, J.E., An nlogn algorithm for minimizing states in a finite automaton, (), 189-196
[12] Lee, C.Y., Binary decision programs, Bell system technical journal, 38, 985-999, (1959)
[13] Lee D. and M. Yannakakis, Online minimization of transition systems, in: Proc. 24th ACM Symposium on Theory of Computing, 1992, pp. 264-274.
[14] Lee D. and M. Yannakakis, Online minimization of transition systems, in: Proc. of 24th ACM Symposium on Theory of Computing (STOC’92) (1992), pp. 264-274.
[15] McMillan, K.L., “symbolic model checking: an approach to the state explosion problem”, (1993), Kluwer Academic Publishers
[16] Paige, R.; Tarjan, R.E., Three partition refinement algorithms, SIAM journal on computing, 16, 973-989, (1987) · Zbl 0654.68072
[17] 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) · Zbl 0574.68060
[18] Sanghavi, J. V., R. K. Ranjan, R. K. Brayton, and A. Sangiovanni-Vincentelli, High performance bdd package based on exploiting memory hierarchy, in: Proc. of ACM/IEEE Design Automation Conference, 1996.
[19] Somenzi F., Binary decision diagrams (1999), available at http://citeseer.nj.nec.com/somenzi99binary.html. · Zbl 0948.68215
[20] Somenzi F., “CUDD: CU Decision Diagram Package Release 2.3.1,” 2001, available at http://vlsi.colorado.edu/fabio/CUDD/cuddIntro.html.
[21] Tarjan, R.E., Depth first search and linear graph algorithms, SIAM journal on computing, 1, 146-160, (1972) · Zbl 0251.05107
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.