LIPIcs.TIME.2019.15.pdf
- Filesize: 0.56 MB
- 16 pages
Document
A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic
Authors
David Chemouil 
-
Part of:
Volume:
26th International Symposium on Temporal Representation and Reasoning (TIME 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Symposium on Temporal Representation and Reasoning (TIME) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2019-10-07
File
Document Identifiers
Author Details
Cite As Get BibTex
Quentin Peyras, Julien Brunel, and David Chemouil. A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TIME.2019.15
Abstract
First-Order Linear Temporal Logic (FOLTL) is well-suited to specify infinite-state systems. However, FOLTL satisfiability is not even semi-decidable, thus preventing automated verification. To address this, a possible track is to constrain specifications to a decidable fragment of FOLTL, but known fragments are too restricted to be usable in practice. In this paper, we exhibit various fragments of increasing scope that provide a pertinent basis for abstract specification of infinite-state systems. We show that these fragments enjoy the Bounded Domain Property (any satisfiable FOLTL formula has a model with a finite, bounded FO domain), which provides a basis for complete, automated verification by reduction to LTL satisfiability. Finally, we present a simple case study illustrating the applicability and limitations of our results.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic
Keywords
- First-Order Linear Temporal Logic
- Bounded Domain Property
- Finite Domain Property
- Decidability
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Aharon Abadi, Alexander Rabinovich, and Mooly Sagiv. Decidable fragments of many-sorted logic. Journal of Symbolic Computation, 45(2):153-172, 2010. URL: https://doi.org/10.1016/j.jsc.2009.03.003.
- Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo. The Electrum Analyzer: Model Checking Relational First-Order Temporal Specifications. In 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE '18), Montpellier, France, September 2018. ACM Press. URL: https://doi.org/10.1145/3238147.3240475.
- Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997. URL: https://doi.org/10.1007/978-3-642-59207-2.
-
Dov M. Gabbay, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. Many-Dimensional Modal Logics: Theory and Applications, chapter Fragments of first-order temporal logics. Elsevier, 2003.
- Ian Hodkinson, Frank Wolter, and Michael Zakharyaschev. Decidable fragments of first-order temporal logics. Annals of Pure and Applied logic, 106(1-3):85-134, 2000. URL: https://doi.org/10.1016/S0168-0072(00)00018-X.
- Ian Hodkinson, Frank Wolter, and Michael Zakharyaschev. Monodic Fragments of First-Order Temporal Logics: 2000-2001 A.D. In Logic for Programming, Artificial Intelligence, and Reasoning, pages 1-23. Springer, 2001. URL: https://doi.org/10.1007/3-540-45653-8_1.
-
Fred Kröger and Stephan Merz. Temporal Logic and State Systems (Texts in Theoretical Computer Science. An EATCS Series). Springer, 2008.
- Denis Kuperberg, Julien Brunel, and David Chemouil. On Finite Domains in First-Order Linear Temporal Logic. In Automated Technology for Verification and Analysis, pages 211-226. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-46520-3_14.
-
Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional, 2002.
- Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, and Denis Kuperberg. Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. In Foundations of Software Engineering, Seattle, United States, November 2016. URL: https://doi.org/10.1145/2950290.2950318.
-
Timothy Nelson, Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. On the finite model property in order-sorted logic. Technical report, Worcester Polytechnic Institute, 2010.
- Timothy Nelson, Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. Toward a More Complete Alloy. In Abstract State Machines, Alloy, B, VDM, and Z, pages 136-149. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-30885-7_10.
- Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. Reducing liveness to safety in first-order logic. Proceedings of the ACM Conference on Principles of Programming Languages (POPL), 2:26, 2017. URL: https://doi.org/10.1145/3158114.
- Oded Padon, Jochen Hoenicke, Kenneth L McMillan, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. In Formal Methods in Computer Aided Design (FMCAD), 2018. URL: https://doi.org/10.23919/FMCAD.2018.8603008.
- Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. Ivy: safety verification by interactive generalization. ACM SIGPLAN Notices, 51(6):614-630, 2016. URL: https://doi.org/10.1145/2980983.2908118.
- Quentin Peyras, Julien Brunel, and David Chemouil. Electrum specification of a toy notificiation system, August 2019. URL: https://doi.org/10.5281/zenodo.3369542.