Abstract
This paper presents a proof method for proving that infinite-state systems satisfy properties expressed in the modal μ-calculus. The method is sound and complete relative to externally proving inclusions of sets of states. It can be seen as a recast of a tableau method due to Bradfield and Stirling following lines used by Winskel for finite-state systems. Contrary to the tableau method, it avoids the use of constants when unfolding fixed points and it replaces the rather involved global success criterion in the tableau method with local success criteria. A proof tree is now merely a means of keeping track of where possible choices are made — and can be changed — and not an essential ingredient in establishing the correctness of a proof: A proof will be correct when all leaves are directly seen to be valid. Therefore, it seems well-suited for implementation as a tool, by, for instance, integration into existing general-purpose theorem provers.
This work is supported by the Danish Technical Research Council.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Henrik Reif Andersen. Verification of Temporal Properties of Concurrent Systems. PhD thesis, Department of Computer Science, Aarhus University, Denmark, June 1993. PB-445.
J.C.M. Baeten and J.W. Klop, editors. Proceedings of CONCUR '90, volume 458 of LNCS. Springer-Verlag, 1990.
Julian C. Bradfield. Verifying Temporal Properties of Systems with Applications to Petri Nets. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh, July 1991.
Julian C. Bradfield. A proof assistant for symbolic model-checking. Technical Report ECS-LFCS-92-199, Laboratory for Foundations of Computer Science, University of Edinburgh, March 1992.
Julian C. Bradfield and Colin P. Stirling. Verifying temporal properties of processes. In Baeten and Klop [2], pages 115–125.
Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27, 1983.
Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
Robin Milner and Mads Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87:209–220, 1991.
David Park. Fixpoint induction and proofs of program properties. Machine Intelligence, 5, 1969.
Colin Stirling. A complete compositional modal proof system for a subset of CCS. volume 194 of Lecture Notes in Computer Science, pages 475–486. Springer-Verlag, 1985.
Colin Stirling. Modal and Temporal Logics. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 477–563. Oxford University Press, 1992.
A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.
Glynn Winskel. A note on model checking the modal v-calculus. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Proceedings of ICALP, volume 372 of LNCS, pages 761–772. Springer-Verlag, 1989.
Glynn Winskel. On the compositional checking of validity. In Baeten and Klop [2], pages 481–501.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andersen, H.R. (1994). On model checking infinite-state systems. In: Nerode, A., Matiyasevich, Y.V. (eds) Logical Foundations of Computer Science. LFCS 1994. Lecture Notes in Computer Science, vol 813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58140-5_2
Download citation
DOI: https://doi.org/10.1007/3-540-58140-5_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58140-6
Online ISBN: 978-3-540-48442-4
eBook Packages: Springer Book Archive