Document Open Access Logo

Constraint LTL with Remote Access

Authors Ashwin Bhaskar , M. Praveen

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2023.41.pdf
  • Filesize: 0.83 MB
  • 21 pages

Document Identifiers

Author Details

Ashwin Bhaskar
  • Chennai Mathematical Institute, India
M. Praveen
  • Chennai Mathematical Institute, India
  • CNRS IRL ReLaX, Chennai, India

Funding

  • Praveen, M.: This author is partially supported by the Infosys foundation.

Cite As Get BibTex

Ashwin Bhaskar and M. Praveen. Constraint LTL with Remote Access. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 41:1-41:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSTTCS.2023.41

Abstract

Constraint Linear Temporal Logic (CLTL) is an extension of LTL that is interpreted on sequences of valuations of variables over an infinite domain. The atomic formulas are interpreted as constraints on the valuations. The atomic formulas can constrain valuations at the current position and positions that are a fixed distance apart (e.g., the previous position or the second previous position and so on). The satisfiability problem for CLTL is known to be Pspace-complete. We generalize CLTL to let atomic formulas access positions that are unboundedly far away in the past. We annotate the sequence of valuations with letters from a finite alphabet and use regular expressions on the finite alphabet to control how atomic formulas access past positions. We prove that the satisfiability problem for this extension of the logic is decidable in cases where the domain is dense and open with respect to a linear order (e.g., rational numbers with the usual linear order). We prove that it is also decidable over integers with linear order and equality.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Verification by model checking
  • Theory of computation → Automata over infinite objects
Keywords
  • Constraint LTL
  • Regular Expressions
  • MSO formulas
  • Satisfiability
  • Büchi automata

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Marcello M Bersani, Domenico Bianculli, Schahram Dustdar, Alessio Gambi, Carlo Ghezzi, and Srđan Krstić. Towards the formalization of properties of cloud-based elastic systems. In proceedings of the 6th international workshop on principles of engineering service-oriented and cloud systems, pages 38-47, 2014. Google Scholar
  2. Marcello M Bersani, Matteo Rossi, and Pierluigi San Pietro. A tool for deciding the satisfiability of continuous-time metric temporal logic. Acta Informatica, 53(2):171-206, 2016. Google Scholar
  3. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Transactions on Computational Logic (TOCL), 12(4):1-26, 2011. Google Scholar
  4. Ahmed Bouajjani and Peter Habermehl. Constrained properties, semilinear systems, and petri nets. In International Conference on Concurrency Theory, pages 481-497. Springer, 1996. Google Scholar
  5. J Richard Buchi. On a decision method in restricted second order arithmetic. Proc. Internat. Congr. on Logic, Methodology and Philosophy of Science, 1960, 1960. Google Scholar
  6. Hubert Comon and Véronique Cortier. Flatness is not a weakness. In International workshop on computer science logic, pages 262-276. Springer, 2000. Google Scholar
  7. Stephane Demri, Deepak D'Souza, and Régis Gascon. Temporal logics of repeating values. Journal of Logic and Computation, 22, October 2012. URL: https://doi.org/10.1093/logcom/exr013.
  8. Stéphane Demri and Régis Gascon. The effects of bounding syntactic resources on presburger ltl. Journal of Logic and Computation, 19(6):1541-1575, 2009. Google Scholar
  9. Stéphane Demri and Ranko Lazić. Ltl with the freeze quantifier and register automata. ACM Trans. Comput. Logic, 10(3), April 2009. URL: https://doi.org/10.1145/1507244.1507246.
  10. Stéphane Demri and Karin Quaas. Concrete domains in logics: a survey. ACM SIGLOG News, 8(3):6-29, 2021. Google Scholar
  11. Stéphane Demri and Karin Quaas. Constraint automata on infinite data trees: from ctl(z)/ctl*(z) to decision procedures. In 34th International Conference on Concurrency Theory (CONCUR 2023). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2023.29.
  12. Stéphane Demri and Deepak D’Souza. An automata-theoretic approach to constraint ltl. Information and Computation, 205(3):380-415, 2007. URL: https://doi.org/10.1016/j.ic.2006.09.006.
  13. Cindy Eisner and Dana Fisman. Functional specification of hardware via temporal logic. Handbook of Model Checking, pages 795-829, 2018. Google Scholar
  14. Bernd Finkbeiner, Philippe Heim, and Noemi Passing. Temporal stream logic modulo theories. In International Conference on Foundations of Software Science and Computation Structures, pages 325-346. Springer International Publishing Cham, 2022. Google Scholar
  15. Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito. Temporal stream logic: Synthesis beyond the bools. In International Conference on Computer Aided Verification, pages 609-629. Springer, 2019. Google Scholar
  16. Michael Kaminski and Nissim Francez. Finite-memory automata. Theoretical Computer Science, 134(2):329-363, 1994. Google Scholar
  17. Nadia Labai, Magdalena Ortiz, and Mantas Šimkus. An exptime upper bound for alc with integers. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 17, pages 614-623, 2020. Google Scholar
  18. Gabor Madl, Luis Bathen, German Flores, and Divyesh Jadav. Formal verification of smart contracts using interface automata. In 2019 IEEE International Conference on Blockchain (Blockchain), pages 556-563, 2019. URL: https://doi.org/10.1109/Blockchain.2019.00081.
  19. M Praveen, Diego Figueira, and Stephane Demri. Reasoning about data repetitions with counter systems. Logical Methods in Computer Science, 12, 2016. Google Scholar
  20. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, 1955. Google Scholar
  21. Moshe Y Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322-331. IEEE Computer Society, 1986. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact