Efficient checking of behavioural relations and modal assertions using fixed-point inversion

  • Henrik Reif Andersen
  • Bart Vergauwen
Session 6: Invited Titorial
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)


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.


Model Check Linear Time Label Transition System Inversion Algorithm Strongly Connect Component 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [AHU74]
    Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974.Google Scholar
  2. [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
  3. [And94]
    Henrik R. Andersen. Model checking and boolean graphs. Theoretical Computer Science, 126(1):3–30, April 1994.MathSciNetGoogle Scholar
  4. [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
  5. [BP92]
    Bard Bloom and Robert Paige. Computing ready simulations efficiently. 1992.Google Scholar
  6. [Bry92]
    Randal E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. Computing Surveys, 24(3):293–318, September 1992.CrossRefGoogle Scholar
  7. [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
  8. [CES86]
    E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.CrossRefGoogle Scholar
  9. [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
  10. [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
  11. [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
  12. [Koz83]
    Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27, 1983.Google Scholar
  13. [KS90]
    P.C. Kanellakis and S.A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation, 86:43–68, 1990.CrossRefGoogle Scholar
  14. [Mil89]
    Robin Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
  15. [Tar72]
    R. Tarjan. Depth-first search and linear graph algorithms. SIAM J. Comput., 2(1), June 1972.Google Scholar
  16. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Henrik Reif Andersen
    • 1
  • Bart Vergauwen
    • 2
  1. 1.Department of Computer ScienceTechnical University of DenmarkLyngbyDenmark
  2. 2.Department of Computer ScienceK.U. LeuvenLeuvenBelgium

Personalised recommendations