Document Open Access Logo

A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic

Authors Quentin Peyras, Julien Brunel, David Chemouil

PDF

File

Thumbnail PDF
PDF
LIPIcs.TIME.2019.15.pdf
  • Filesize: 0.56 MB
  • 16 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

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

Author Details

Quentin Peyras
  • ONERA DTIS, Toulouse, France
  • Université fédérale de Toulouse, France
Julien Brunel
  • ONERA DTIS, Toulouse, France
  • Université fédérale de Toulouse, France
David Chemouil
  • ONERA DTIS, Toulouse, France
  • Université fédérale de Toulouse, France

Funding

Work partly financed by the European Regional Development Fund (ERDF) through the Operational Programme for Competitiveness and Internationalisation (COMPETE2020) and by National Funds through the Portuguese funding agency, Fundação para a Ciência e a Tecnologia (FCT) within project POCI-01-0145-FEDER-016826.

References

  1. 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.
  2. 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.
  3. 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.
  4. 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. Google Scholar
  5. 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.
  6. 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.
  7. Fred Kröger and Stephan Merz. Temporal Logic and State Systems (Texts in Theoretical Computer Science. An EATCS Series). Springer, 2008. Google Scholar
  8. 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.
  9. Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional, 2002. Google Scholar
  10. 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.
  11. 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. Google Scholar
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. Quentin Peyras, Julien Brunel, and David Chemouil. Electrum specification of a toy notificiation system, August 2019. URL: https://doi.org/10.5281/zenodo.3369542.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact