Efficient checking of behavioural relations and modal assertions using fixed-point inversion
This paper presents an algorithm for solving Boolean fixed-point equations containing one level of nesting of minimum and maximum fixed points. The algorithm assumes that the equations of the inner fixed point is of a certain restricted kind and has a worst-case time- and space-complexity that is linear in the size of the equation system. By observing that a range of behavioral relations — in particular weak bisimulation — and modal assertions can be checked using equation systems of this restricted form, the algorithm improves on existing ad hoc constructed algorithms.
Finally, we show how the key idea of inverting a fixed point can be used in decreasing the number of fixed-point iterations needed in BDD-based methods for solving the same class of problems.
KeywordsModel Check Linear Time Label Transition System Inversion Algorithm Strongly Connect Component
- [AHU74]Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974.Google Scholar
- [And93]Henrik R. Andersen. Verification of Temporal Properties of Concurrent Systems. PhD thesis, Department of Computer Science, Aarhus University, Denmark, June 1993. PB–445.Google Scholar
- [BCM+90]J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428–439. IEEE Computer Society Press, 1990.Google Scholar
- [BP92]Bard Bloom and Robert Paige. Computing ready simulations efficiently. 1992.Google Scholar
- [CDS92]Ranee Cleaveland, Marion Dreimüller, and Bernhard Steffen. Faster model checking for the modal mu-calculus. In G. v. Bochmann and D. K. Probst, editors, Proceedings of the 4th Workshop on Computer Aided Verification, CAV'92, June 29–July 1, 1992, Montreal, Quebec, Canada, volume 663 of LNCS, pages 383–394. Springer-Verlag, 1992.Google Scholar
- [EJS93]E.A. Emerson, C.S. Jutla, and A.P. Sistla. On model-checking for fragments of μ-calculus. In Costas Courcoubetis, editor, Proceedings of the 5th International Conference on Computer Aided Verification, CAV'93, volume 697 of LNCS, pages 385–396. Springer-Verlag, 1993.Google Scholar
- [ESTT91]Klaus Estenfeld, Hans-Albert Schneider, Dirk Taubner, and Erik Tidén. Computer aided verification of parallel processes. In A. Pfitzmann and E. Raubold, editors, VIS '91 Verlässliche Informationssysteme, volume 271 of Informatik Fachberichte, pages 208–226, Darmstadt, 1991. Springer-Verlag.Google Scholar
- [GV90]J.F. Groote and F. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In M.S. Paterson, editor, Proceedings of ICALP, volume 443 of LNCS. Springer-Verlag, 1990.Google Scholar
- [Koz83]Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27, 1983.Google Scholar
- [Mil89]Robin Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
- [Tar72]R. Tarjan. Depth-first search and linear graph algorithms. SIAM J. Comput., 2(1), June 1972.Google Scholar
- [VL92]Bart Vergauwen and Johan Lewi. A linear algorithm for solving fixed-point equations on transition systems. In J.-C. Raoult, editor, Proceedings of 17'th Colloquium on Trees in Algebra and Programming, CAAP'92, Rennes, France, volume 581 of LNCS, pages 322–341. Springer-Verlag, 1992.Google Scholar