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

## Abstract

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.

## Keywords

Model Check Linear Time Label Transition System Inversion Algorithm Strongly Connect Component## References

- [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 - [And94]Henrik R. Andersen. Model checking and boolean graphs.
*Theoretical Computer Science*, 126(1):3–30, April 1994.MathSciNetGoogle Scholar - [BCM+90]J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 10
^{20}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
- [Bry92]Randal E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams.
*Computing Surveys*, 24(3):293–318, September 1992.CrossRefGoogle 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 - [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 - [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 - [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 - [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