Abstract
We present an automated abstract verification method for infinite-state systems specified by logic programs (which are a uniform and intermediate layer to which diverse formalisms such as transition systems, pushdown processes and while programs can be mapped). We establish connections between: logic program semantics and CTL properties, set-based program analysis and pushdown processes, and also between model checking and constraint solving, viz. theorem proving. We show that set-based analysis can be used to compute supersets of the values of program variables in the states that satisfy a given CTL property.
On leave from Wroclaw University. Partially supported by Polish KBN grant 8T11C02913.
Chapter PDF
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
O. Bernholtz, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In Computer Aided Verification, Proc. 6th Int. Workshop, volume 818 of LNCS, pages 142–155, Stanford, California, June 1994. Springer-Verlag. Full version available from authors.
A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Pushdown Automata: Application to Model Checking. In CONCUR'97. LNCS 1243, 1997.
A. Bouajjani and O. Maler. Reachability Analysis of Pushdown Automata. In Infinity'96. tech. rep. MIP-9614, Univ. Passau, 1996.
F. Bourdoncle. Abstact debugging of higher-order imperative languages. In Proceedings of the SIGPLAN'93 Conference on Programming Language Design and Implementation (PLDI'93), LNCS, pages 46–55. ACM Press, 1993.
O. Burkart and B. Steffen. Composition, Decomposition and Model-Checking of Pushdown Processes. Nordic Journal of Computing, 2, 1995.
W. Charatonik, D. McAllester, D. Niwinski, A. Podelski, and I. Walukiewicz. The Horn mu-calculus. Submitted for publication. Available under www.mpisb.mpg.de/~podelski/papers/HornMuCalculus.ps, December 1997.
W. Charatonik, D. McAllester, and A. Podelski. Computing the greatest model of the set-based abstraction of logic programs. Presented at the Dagstuhl Workshop on Tree Automata, October 1997.
W. Charatonik and A. Podelski. Co-definite set constraints. In T. Nipkow, editor, Proceedings of the 9th International Conference on Rewriting Techniques and Applications, LNCS, Tsukuba, Japan, March–April 1998. Springer-Verlag. To appear.
E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. In Proceedings of the 19th Annual Symposium on Principles of Programming Languages, pages 343–354. ACM Press, 1992.
P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Proc. POPL '92, pages 83–94. ACM Press, 1992.
D. R. Dams. Abstract interpretation and partition refinement for model checking. PhD thesis, Eindhoven University of Technology, 1996.
P. Devienne, J.-M. Talbot, and S. Tison. Solving classes of set constraints with tree automata. In G. Smolka, editor, Proceedings of the Third International Conference on Principles and Practice of Constraint Programming — CP97, volume 1330 of LNCS, pages 68–83. Springer-Verlag, October 1997.
P. Devienne, J.-M. Talbot, and S. Tison. Solving classes of set constraints with tree automata. In G. Smolka, editor, Proceedings of the Third International Conference on Principles and Practice of Constraint Programming — CP97, volume 1330 of LNCS, Berlin, Germany, October 1997. Springer-Verlag.
E. Emerson and E. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241–266, 1982.
J. Esparza. Decidability of model checking for infinite-state concurrent systems. Acta Informatika, 34:85–107, 1997.
T. Frühwirth, E. Shapiro, M. Vardi, and E. Yardeni. Logic programs as types for logic programs. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 300–309, July 1991.
N. Heintze and J. Jaffar. A decision procedure for a class of set constraints (extended abstract). In Fifth Annual IEEE Symposium on Logic in Computer Science, pages 42–51, 1990.
N. Heintze and J. Jaffar. A finite presentation theorem for approximating logic programs. In Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 197–209, January 1990.
J. Jaffar and M. J. Maher. Constraint Logic Programming: A Survey. The Journal of Logic Programming, 19/20:503–582, May–July 1994.
N. D. Jones and S. S. Muchnick. Flow analysis and optimization of lisp-like structures. In Sixth Annual ACM Symposium on Principles of Programming Languages, pages 244–256, January 1979.
J. W. Lloyd. Foundations of Logic Programming. Symbolic Computation. Springer-Verlag, Berlin, Germany, second, extended edition, 1987.
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1):11–44, 1995.
D. E. Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie Mellon University, 1993.
A. Mader. Verification of Modal Properties Using Boolean Equation Systems. Phd thesis, Technische Universität München, 1997.
A. Podelski, W. Charatonik, and M. Müller. Set-based error diagnosis of concurrent constraint programs. Submitted for publication. Available under www.mpi-sb.mpg.de/~podelski/papers/diagnosis.ps, 1998.
Y. Ramakrishna, C. Ramakrishnan, I. Ramakrishnan, S. Smolka, T. Swift, and D. Warren. Efficient model checking using tabled resolution. In Computer Aided Verification (CAV'97), LNCS 1254. Springer-Verlag, June 1997.
M. Y. Vardi. Verification of concurrent programs: The automata-theoretic framework. In Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, pages 167–76, Ithaca, 1987. IEEE Computer Society Press.
I. Walukiewicz. Pushdown Processes: Games and Model Checking. In CAV'96. LNCS 1102, 1996.
C. Weidenbach. Spass version 0.49. Journal of Automated Reasoning, 18(2):247–252, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Charatonik, W., Podelski, A. (1998). Set-based analysis of reactive infinite-state systems. 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/BFb0054183
Download citation
DOI: https://doi.org/10.1007/BFb0054183
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