Abstract
We introduce Partitioned Dependency Graphs (PDGs), an abstract framework for the specification and evaluation of arbitrarily nested alternating fixed points. The generality of PDGs subsumes that of similarly proposed models of nested fixed-point computation such as Boolean graphs, Boolean equation systems, and the propositional modal mu-calculus. Our main result is an efficient local algorithm for evaluating PDG fixed points. Our algorithm, which we call LAFP, combines the simplicity of previously proposed induction-based algorithms (such as Winskel's tableau method for v-calculus model checking) with the efficiency of semantics-based algorithms (such as the bit-vector method of Cleaveland, Klein, and Steffen for the equational Μ-calculus). In particular, LAFP is simply specified, we provide a completely rigorous proof of its correctness, and the number of fixed-point iterations required by the algorithm is asymptotically the same as that of the best existing global algorithms. Moreover, preliminary experimental results demonstrate that LAFP performs extremely well in practice. To our knowledge, this makes LAFP the first efficient local algorithm for computing fixed points of arbitrary alternation depth to appear in the literature.
Research supported in part by NSF grants CCR-9505562 and CCR-9705998, and AFOSR grants F49620-95-1-0508 and F49620-96-1-0087.
Chapter PDF
References
H. R. Andersen. Model checking and boolean graphs. Theoretical Computer Science, 126(1), 1994.
G. S. Bhat and R. Cleaveland. Efficient local model checking for fragments of the modal Μ-calculus. In T. Margaria and B. Steffen, editors, Proceedings of the Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), Vol. 1055 of Lecture Notes in Computer Science, pages 107–126. Springer-Verlag, March 1996.
G. S. Bhat and R. Cleaveland. Efficient model checking via the equational Μ-calculus. In E. M. Clarke, editor, 11th Annual Symposium on Logic in Computer Science (LICS '96), pages 304–312, New Brunswick, NJ, July 1996. Computer Society Press.
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In D. Kozen, editor, Proceedings of the Workshop on Logic of Programs, Yorktown Heights, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer-Verlag, 1981.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.
R. Cleaveland, M. Klein, and B. Steffen. Faster model checking for the modal mu-calculus. In G.v. Bochmann and D.K. Probst, editors, Proceedings of the Fourth International Conference on Computer Aided Verification (CAV '9Z), Vol. 663 of Lecture Notes in Computer Science, pages 410–422. Springer-Verlag, 1992.
R. Cleaveland. Tableau-based model checking in the propositional mucalculus. Acta Informatica, 27(8):725–747, September 1990.
E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4), December 1996.
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, pages 267–278, 1986.
D. Kozen. Results on the propositional Μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
D. E. Long, A. Browne, E. M. Clarke, S. Jha, and W. R. Marrero. An improved algorithm for the evaluation of fixpoint expressions. In D. Dill, editor, Proceedings of the Sixth International Conference on Computer Aided Verification (CAV '94), Vol. 818 of Lecture Notes in Computer Science. Springer-Verlag, 1994.
X. Liu. Specification and Decomposition in Concurrency, Technical Report No. R 92-2005. PhD thesis, Department of Computer Science, Aalborg University, 1992.
I. Niemela and P. Simons. Efficient implementation of the well-founded and stable model semantics. In Joint International Conference and Symposium on Logic Programming, pages 289–303, 1996.
V.R. Pratt. A decidable mu-calculus. In Proceedings of the 22nd IEEE Ann. Symp. on Foundations of Computer Science, Nashville, Tennessee, pages 421–427, 1981.
J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proceedings of the International Symposium in Programming, volume 137 of Lecture Notes in Computer Science, Berlin, 1982. Springer-Verlag.
Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. W. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In Proceedings of the 9th International Conference on Computer-Aided Verification (CAV '97), Haifa, Israel, July 1997. Springer-Verlag.
Y. S. Ramakrishna and S. A. Smolka. Partial-order reduction in the weak modal mu-calculus. In A. Mazurkiewicz and J. Winkowski, editors, Proceedings of the Eighth International Conference on Concurrency Theory (CONCUR '97), volume 1243 of Lecture Notes in Computer Science, Warsaw, Poland, July 1997. Springer-Verlag.
B. Steffen, A. Classen, M. Klein, J. Knoop, and T. Margaria. The fixpointanalysis machine. In I. Lee and S. A. Smolka, editors, Proceedings of the Sixth International Conference on Concurrency Theory (CONCUR '95), Vol. 962 of Lecture Notes in Computer Science, pages 72–87. Springer-Verlag, 1995.
O. Sokolsky and S. A. Smolka. Incremental model checking in the modal mu-calculus. In D. Dill, editor, Proceedings of the Sixth International Conference on Computer Aided Verification (CAV '94), Vol. 818 of Lecture Notes in Computer Science. Springer-Verlag, 1994.
K. Sagonas, T. Swift, and D.S. Warren. An abstract machine to compute fixed-order dynamically stratified programs. In International Conference on Automated Deduction (CADE), 1996.
C. Stirling and D. Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, 89(1), 1991.
B. Vergauwen and J. Lewi. Efficient local correctness checking for single and alternating boolean equation systems. In Proceedings of ICALP'94, pages 304–315. LNCS 820, 1994.
G. Winskel. A note on model checking the modal v-calculus. In Proceedings of ICALP '89, Vol. 372 of Lecture Notes in Computer Science, 1989.
XSB. The XSB logic programming system v1.7, 1997. Available by anonymous ftp from ftp.cs.sunysb.edu.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, X., Ramakrishnan, C.R., Smolka, S.A. (1998). Fully local and efficient evaluation of alternating fixed points. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054161
Download citation
DOI: https://doi.org/10.1007/BFb0054161
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive