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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974.
Henrik R. Andersen. Verification of Temporal Properties of Concurrent Systems. PhD thesis, Department of Computer Science, Aarhus University, Denmark, June 1993. PB–445.
Henrik R. Andersen. Model checking and boolean graphs. Theoretical Computer Science, 126(1):3–30, April 1994.
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.
Bard Bloom and Robert Paige. Computing ready simulations efficiently. 1992.
Randal E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. Computing Surveys, 24(3):293–318, September 1992.
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.
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.
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.
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.
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.
Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27, 1983.
P.C. Kanellakis and S.A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation, 86:43–68, 1990.
Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
R. Tarjan. Depth-first search and linear graph algorithms. SIAM J. Comput., 2(1), June 1972.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andersen, H.R., Vergauwen, B. (1995). Efficient checking of behavioural relations and modal assertions using fixed-point inversion. In: Wolper, P. (eds) Computer Aided Verification. CAV 1995. Lecture Notes in Computer Science, vol 939. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60045-0_47
Download citation
DOI: https://doi.org/10.1007/3-540-60045-0_47
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60045-9
Online ISBN: 978-3-540-49413-3
eBook Packages: Springer Book Archive