Abstract
Many automated finite-state verification procedures can be viewed as fixpoint computations over a finite lattice (typically the powerset of the set of system states). Hence, fixpoint calculi such as the propositional Μ-calculus have proven useful, both as ways to describe verification algorithms and as specification formalisms in their own right. We consider the problem of evaluating expressions in a fixpoint calculus over a given model. A naive algorithm for this task may require time n q, where n is the maximum length of a chain in the lattice and q is the depth of fixpoint nesting. In 1986, Emerson and Lei presented a method requiring about n d steps, where d is the number of alternations between least and greatest fixpoints. More recent algorithms have reduced the exponent by one or two, but the complexity has remained at about n d. In this paper, we present a new algorithm that makes extensive use of monotonicity considerations to solve the problem in about nd/2 steps. Thus, the time required by our method is only about the square root of the time required by the earlier algorithms.
This research was sponsored in part by the Wright Laboratory, Aeronautical Systems Center, Air Force Material Command, USAF, and the Advanced Research Projects Agency (ARPA) under grant number F33615-93-1-1330, and in part by the Semiconductor Research Corportation (SRC) under contract 92-DJ-294, and in part by the National Science Foundation under contract number CCR-9217549. The views and conclusions contained in this document are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of Wright Laboratory, the U. S. Government, the Semiconductor Research Corporation, or the National Science Foundation. The U. S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright notation thereon.
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
H. R. Andersen. Model checking and boolean graphs. In B. Krieg-Bruckner, editor, Proceedings of the Fourth European Symposium on Programming, volume 582 of Lecture Notes in Computer Science. Springer-Verlag, February 1992.
G. V. Bochmann and D. K. Probst, editors. Proceedings of the Fourth Workshop on Computer-Aided Verification, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, July 1992.
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1990.
E. M. Clarke, I. A. Draghicescu, and R. P. Kurshan. A unified approach for showing language containment and equivalence between various types of Ω-automata. In A. Arnold and N. D. Jones, editors, Proceedings of the 15th Colloquium on Trees in Algebra and Programming, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, May 1990.
E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, 1981.
R. Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27(8):725–747, 1990.
R. Cleaveland, M. Klein, and B. Steffen. Faster model checking for the modal mu-calculus. In Bochmann and Probst [2].
R. Cleaveland and B. Steffen. A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Methods in System Design, 2(2):121–147, April 1993.
O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Proceedings of the 1989 International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, June 1989.
E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the First Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1986.
M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18:194–211, 1979.
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, December 1983.
K. G. Larsen. Efficient local correctness checking. In Bochmann and Probst [2].
A. Mader. Tableau recycling. In Bochmann and Probst [2].
R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.
C. Stirling and D. J. Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, 89(1):161–177, October 1991.
A. Tarski. A lattice-theoretic fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.
G. Winskel. Model checking in the modal Ν-calculus. In Proceedings of the Sixteenth International Colloquium on Automata, Languages, and Programming, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Long, D.E., Browne, A., Clarke, E.M., Jha, S., Marrero, W.R. (1994). An improved algorithm for the evaluation of fixpoint expressions. In: Dill, D.L. (eds) Computer Aided Verification. CAV 1994. Lecture Notes in Computer Science, vol 818. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58179-0_66
Download citation
DOI: https://doi.org/10.1007/3-540-58179-0_66
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58179-6
Online ISBN: 978-3-540-48469-1
eBook Packages: Springer Book Archive