×

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
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aczel., P., “Non-well-founded sets.” Lecture Notes, Center for the Study of Language and Information 14; Aczel., P., “Non-well-founded sets.” Lecture Notes, Center for the Study of Language and Information 14 · 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 nn symbolic stepsProc. of Int. Conference on Formal Methods in Computer-Aided Design (FMCAD’00)1954; Bloem R., H. N. Gabow and F. Somenzi, An algorithm for strongly connected component analysis in nn symbolic stepsProc. of Int. Conference on Formal Methods in Computer-Aided Design (FMCAD’00)1954 · Zbl 1110.68161
[4] Bouajjani A., J. C. Fernandez and N. Halbwachs, Minimal model generationProc. Int’l Conference on Computer-Aided Verification CAV90531; Bouajjani A., J. C. Fernandez and N. Halbwachs, Minimal model generationProc. Int’l Conference on Computer-Aided Verification CAV90531 · Zbl 0765.68114
[5] Bouali A. and R. de Simone, Symbolic bisimulation minimizationProc. Int’l Conference on Computer-Aided Verification CAV92663; Bouali A. and R. de Simone, Symbolic bisimulation minimizationProc. Int’l Conference on Computer-Aided Verification CAV92663
[6] Bryant, R. E., Symbolic manipulation of boolean functions using a graphical representationProc. 22nd Design Automation Conference; Bryant, R. E., Symbolic manipulation of boolean functions using a graphical representationProc. 22nd Design Automation Conference
[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 algorithmProc. of Int. Conference on Computer Aided Verification (CAV’01)2102; Dovier A., C. Piazza and A. Policriti, A fast bisimulation algorithmProc. of Int. Conference on Computer Aided Verification (CAV’01)2102 · Zbl 0991.68553
[10] Fisler K. and M. Y. Vardi, Bisimulation and model checkingProc. Correct Hardware Design and Verification Methods1703; Fisler K. and M. Y. Vardi, Bisimulation and model checkingProc. Correct Hardware Design and Verification Methods1703
[11] Hopcroft, J. E., An nlogn algorithm for minimizing states in a finite automaton, (Kohavi, Zvi; Paz, Azaria, Theory of Machines and Computations (1971), Academic Press), 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 systemsProc. 24th ACM Symposium on Theory of Computing; Lee D. and M. Yannakakis, Online minimization of transition systemsProc. 24th ACM Symposium on Theory of Computing
[14] Lee D. and M. Yannakakis, Online minimization of transition systemsProc. of 24th ACM Symposium on Theory of Computing (STOC’92); Lee D. and M. Yannakakis, Online minimization of transition systemsProc. of 24th ACM Symposium on Theory of Computing (STOC’92)
[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 hierarchyProc. of ACM/IEEE Design Automation Conference; Sanghavi, J. V., R. K. Ranjan, R. K. Brayton, and A. Sangiovanni-Vincentelli, High performance bdd package based on exploiting memory hierarchyProc. of ACM/IEEE Design Automation Conference
[19] Somenzi F., Binary decision diagramshttp://citeseer.nj.nec.com/somenzi99binary.html; Somenzi F., Binary decision diagramshttp://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; 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.