Document Open Access Logo

Realizability Problem for Constraint LTL

Authors Ashwin Bhaskar , M. Praveen

PDF
Thumbnail PDF

File

LIPIcs.TIME.2022.8.pdf
  • Filesize: 0.81 MB
  • 19 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 AsGet BibTex

Ashwin Bhaskar and M. Praveen. Realizability Problem for Constraint LTL. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TIME.2022.8

Abstract

Constraint linear-time 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 over a range of positions along a sequence, with the range being bounded by a parameter depending on the formula. The satisfiability and model checking problems for CLTL have been studied by Demri and D’Souza. We consider the realizability problem for CLTL. The set of variables is partitioned into two parts, with each part controlled by a player. Players take turns to choose valuations for their variables, generating a sequence of valuations. The winning condition is specified by a CLTL formula - the first player wins if the sequence of valuations satisfies the specified formula. We study the decidability of checking whether the first player has a winning strategy in the realizability game for a given CLTL formula. We prove that it is decidable in the case where the domain satisfies the completion property, a property introduced by Balbiani and Condotta in the context of satisfiability. We prove that it is undecidable over (ℤ, < , =), the domain of integers with order and equality. We prove that over (ℤ, < , =), it is decidable if the atomic constraints in the formula can only constrain the current valuations of variables belonging to the second player, but there are no such restrictions for the variables belonging to the first player. We call this single-sided games.

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
  • Theory of computation → Tree languages
Keywords
  • Realizability
  • constraint LTL
  • Strategy trees
  • Tree automata

Metrics

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

Related Versions

References

  1. Parosh Aziz Abdulla, Ahmed Bouajjani, and Julien d’Orso. Deciding monotonic games. In International Workshop on Computer Science Logic, pages 1-14. Springer, 2003. Google Scholar
  2. Parosh Aziz Abdulla, Richard Mayr, Arnaud Sangnier, and Jeremy Sproston. Solving parity games on integer vectors. In International Conference on Concurrency Theory, pages 106-120. Springer, 2013. Google Scholar
  3. Rajeev Alur and Thomas A Henzinger. A really temporal logic. Journal of the ACM (JACM), 41(1):181-203, 1994. Google Scholar
  4. Philippe Balbiani and Condotta Jean-François. Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In International Workshop on Frontiers of Combining Systems, pages 162-176. Springer, 2002. Google Scholar
  5. Béatrice Bérard, Benedikt Bollig, Mathieu Lehaut, and Nathalie Sznajder. Parameterized synthesis for fragments of first-order logic over data words. In FoSSaCS, pages 97-118, 2020. Google Scholar
  6. 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
  7. Ashwin Bhaskar and M. Praveen. Realizability problem for constraint ltl, 2022. URL: https://doi.org/10.48550/ARXIV.2207.06708.
  8. 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
  9. Cristian S Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasi-polynomial time. SIAM Journal on Computing, 51(2):STOC17-152, 2020. Google Scholar
  10. Alonzo Church. Logic, arithmetic, and automata. Journal of Symbolic Logic, 29(4), 1964. Google Scholar
  11. 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.
  12. 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.
  13. 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.
  14. Léo Exibard, Emmanuel Filiot, and Ayrat Khalimov. Church synthesis on register automata over linearly ordered data domains. arXiv preprint arXiv:2004.12141, 2020. Google Scholar
  15. Erich Gradel and Wolfgang Thomas. Automata, logics, and infinite games: a guide to current research, volume 2500. Springer Science & Business Media, 2002. Google Scholar
  16. Michael Kaminski and Nissim Francez. Finite-memory automata. Theoretical Computer Science, 134(2):329-363, 1994. Google Scholar
  17. Hadas Kress-Gazit, Georgios E Fainekos, and George J Pappas. Temporal-logic-based reactive mission and motion planning. IEEE transactions on robotics, 25(6):1370-1381, 2009. Google Scholar
  18. Orna Kupferman, Nir Piterman, and Moshe Vardi. From liveness to promptness. Formal Methods in System Design, 34, April 2009. URL: https://doi.org/10.1007/s10703-009-0067-z.
  19. René Mazala. Infinite Games, pages 23-38. Springer Berlin Heidelberg, Berlin, Heidelberg, 2002. URL: https://doi.org/10.1007/3-540-36387-4_2.
  20. Frank Nießner. Nondeterministic tree automata. In Automata Logics, and Infinite games, pages 135-152. Springer, 2002. Google Scholar
  21. Nir Piterman. From nondeterministic büchi and streett automata to deterministic parity automata. Logical Methods in Computer Science, 3, 2007. Google Scholar
  22. Nir Piterman, Amir Pnueli, and Yaniv Sa’ar. Synthesis of reactive (1) designs. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 364-380. Springer, 2006. Google Scholar
  23. Amir Pnueli and Roni Rosner. On the synthesis of an asynchronous reactive module. In International Colloquium on Automata, Languages, and Programming, pages 652-671. Springer, 1989. Google Scholar
  24. M Praveen, Diego Figueira, and Stephane Demri. Reasoning about data repetitions with counter systems. Logical Methods in Computer Science, 12, 2016. Google Scholar
  25. M Praveen, Anirban Majumdar, and Diego Figueira. Playing with repetitions in data words using energy games. Logical Methods in Computer Science, 16, 2020. Google Scholar
  26. Alexander Rabinovich. Decidable extensions of church’s problem. In International Workshop on Computer Science Logic, pages 424-439. Springer, 2009. Google Scholar
  27. Jean-François Raskin. An introduction to hybrid automata. In Handbook of networked and embedded control systems, pages 491-517. Springer, 2005. Google Scholar
  28. Pierre-Alain Reynier, Emmanuel Filiot, and Léo Exibard. Synthesis of data word transducers. Logical Methods in Computer Science, 17, 2021. Google Scholar
  29. A Prasad Sistla, Moshe Y Vardi, and Pierre Wolper. The complementation problem for büchi automata with applications to temporal logic. Theoretical Computer Science, 49(2-3):217-237, 1987. Google Scholar
  30. 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 Imprint Privacy Contact