Document Open Access Logo

Positional Properties in Temporal Logic

Authors Jessica Newman , Benjamin Plummer

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.44.pdf
  • Filesize: 0.83 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Algebraic language theory
Keywords
  • Positionality
  • Temporal Logic
  • ATL
  • Games on graphs

Metrics

Abstract

We study positional properties in the context of game-based reactive synthesis. Our motivation stems from having a usable specification logic, for which tractable synthesis is guaranteed. We demonstrate that every ω-regular positional property (with respect to state- or edge-labelled game graphs), is expressible in linear-time temporal logic. Additionally, we provide some necessary and sufficient conditions for when an ω-regular property is positional, and identify well-behaved subclasses of ω-regular positional properties. Using varieties of languages, we prove that no class of ω-regular positional properties can simultaneously contain a prefix-independent property and be closed under Boolean operations. We conclude by discussing the implications on alternating-time temporal logic, where we isolate a few different fragments with tractable model checking, and compare the associated expressivity of such fragments.

Cite As Get BibTex

Jessica Newman and Benjamin Plummer. Positional Properties in Temporal Logic. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 44:1-44:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.44

Author Details

Jessica Newman
  • University of Southampton, UK
Benjamin Plummer
  • University of Southampton, UK

Acknowledgements

We thank Corina Cîrstea and Enrico Marchioni for their valuable feedback.

References

  1. E. Allen Emerson and Chin-Laung Lei. Modalities for model checking: branching time logic strikes back. Science of Computer Programming, 8(3):275-306, 1987. URL: https://doi.org/10.1016/0167-6423(87)90036-0.
  2. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, September 2002. URL: https://doi.org/10.1145/585265.585270.
  3. Dana Angluin and Dana Fisman. Regular ω-languages with an informative right congruence. Information and Computation, 278:104598, 2021. Special Issue on Ninth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2018). URL: https://doi.org/10.1016/j.ic.2020.104598.
  4. André Arnold. A syntactic congruence for rational ω-languages. Theoretical Computer Science, 39:333-335, 1985. Third Conference on Foundations of Software Technology and Theoretical Computer Science. URL: https://doi.org/10.1016/0304-3975(85)90148-3.
  5. Sanjeev Arora and Boaz Barak. The polynomial hierarchy and alternations, pages 95-105. Cambridge University Press, 2009. Google Scholar
  6. A. Atminas and V. Lozin. Deciding atomicity of subword-closed languages. Theoretical Computer Science, 1003:114595, 2024. URL: https://doi.org/10.1016/j.tcs.2024.114595.
  7. Alessandro Bianco, Marco Faella, Fabio Mogavero, and Aniello Murano. Exploring the boundary of half-positionality. Annals of Mathematics and Artificial Intelligence, 62(1):55-77, June 2011. URL: https://doi.org/10.1007/s10472-011-9250-1.
  8. Fabian Birkmann, Stefan Milius, and Henning Urbat. On language varieties without boolean operations. In Language and Automata Theory and Applications: 15th International Conference, LATA 2021, Milan, Italy, March 1–5, 2021, Proceedings, pages 3-15, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-68195-1_1.
  9. Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann. Graph games and reactive synthesis. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 921-962. Springer International Publishing, Cham, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_27.
  10. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of reactive(1) designs. Journal of Computer and System Sciences, 78(3):911-938, 2012. In Commemoration of Amir Pnueli. URL: https://doi.org/10.1016/j.jcss.2011.08.007.
  11. Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-Positional Objectives Recognized by Deterministic Büchi Automata. In Bartek Klin, Sławomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory (CONCUR 2022), volume 243 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1-20:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.20.
  12. Patricia Bouyer, Mickael Randour, and Pierre Vandenhove. Characterizing omega-regularity through finite-memory determinacy of games on infinite graphs. TheoretiCS, Volume 2, January 2023. URL: https://doi.org/10.46298/theoretics.23.1.
  13. J. Richard Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138(0):295-311, 1969. URL: https://doi.org/10.1090/s0002-9947-1969-0280205-0.
  14. Nils Bulling and Wojciech Jamroga. Comparing variants of strategic ability: how uncertainty and memory influence general properties of games. Autonomous Agents and Multi-Agent Systems, 28(3):474-518, May 2014. URL: https://doi.org/10.1007/s10458-013-9231-3.
  15. Simon Busard, Charles Pecheur, Hongyang Qu, and Franco Raimondi. Reasoning about memoryless strategies under partial observability and unconditional fairness constraints. Information and Computation, 242:128-156, 2015. URL: https://doi.org/10.1016/j.ic.2015.03.014.
  16. Hugues Calbrix, Maurice Nivat, and Andreas Podelski. Ultimately periodic words of rational ω-languages. In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Mathematical Foundations of Programming Semantics, pages 554-566, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg. Google Scholar
  17. Olivier Carton, Dominique Perrin, and Jean-Eric Pin. Automata and semigroups recognizing infinite words. In E. Grädel J. Flum and T. Wilke, editors, Logic and Automata, History and perspectives, pages 585-596. Amsterdam University Press, 2007. URL: https://hal.science/hal-00340797.
  18. Antonio Casares and Pierre Ohlmann. Positional ω-regular languages. TheoretiCS, Volume 5, February 2026. URL: https://doi.org/10.46298/theoretics.26.5.
  19. Thomas Colcombet, Nathanaël Fijalkow, and Florian Horn. Playing safe, ten years later. Logical Methods in Computer Science, Volume 20, Issue 1, January 2024. URL: https://doi.org/10.46298/lmcs-20(1:10)2024.
  20. Thomas Colcombet and Olivier Idir. An algebraic characterisation of eve-positional languages, 2026. URL: https://doi.org/10.48550/arXiv.2604.22648.
  21. Thomas Colcombet and Damian Niwiński. On the positional determinacy of edge-labeled games. Theoretical Computer Science, 352(1):190-196, 2006. URL: https://doi.org/10.1016/j.tcs.2005.10.046.
  22. Stéphane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science: Finite-State Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781139236119.
  23. Volker Diekert and Paul Gastin. First-order definable languages. In Jörg Flum, Erich Grädel, and Thomas Wilke, editors, Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], Texts in Logic and Games, pages 261-306. Amsterdam University Press, 2008. Google Scholar
  24. E. Allen Emerson and Joseph Y. Halpern. "Sometimes" and "not never" revisited: on branching versus linear time (preliminary report). In Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '83, pages 127-140, New York, NY, USA, 1983. Association for Computing Machinery. URL: https://doi.org/10.1145/567067.567081.
  25. E.A. Emerson and C.S. Jutla. Tree automata, mu-calculus and determinacy. In [1991] Proceedings 32nd Annual Symposium of Foundations of Computer Science, pages 368-377, 1991. URL: https://doi.org/10.1109/SFCS.1991.185392.
  26. Patrick Gardy, Patricia Bouyer, and Nicolas Markey. Dependences in Strategy Logic. In Rolf Niedermeier and Brigitte Vallée, editors, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018), volume 96 of Leibniz International Proceedings in Informatics (LIPIcs), pages 34:1-34:15, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.34.
  27. Hugo Gimbert and Wiesław Zielonka. Games where you can play optimally without any memory. In Martín Abadi and Luca de Alfaro, editors, CONCUR 2005 - Concurrency Theory, pages 428-442, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  28. Aidan Harding, Mark Ryan, and Pierre-Yves Schobbens. Approximating atl* in atl. In Agostino Cortesi, editor, Verification, Model Checking, and Abstract Interpretation, pages 289-301, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-47813-2_20.
  29. Mustapha Kabil and Maurice Pouzet. Injective envelopes of transition systems and ferrers languages. RAIRO-Theor. Inf. Appl., 54:4, 2020. URL: https://doi.org/10.1051/ita/2020005.
  30. Eryk Kopczyński. Half-positional determinacy of infinite games. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Automata, Languages and Programming, pages 336-347, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  31. Eryk Kopczyński. Omega-regular half-positional winning conditions. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, pages 41-53, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  32. Eryk Kopczyński. Half-positional determinacy of infinite games. PhD thesis, University of Warsaw, 2014. Google Scholar
  33. François Laroussinie. Logique temporelle avec passé pour la spécification et la vérification des systèmes réactifs. PhD thesis, Grenoble INP, 1994. Thèse de doctorat dirigée par Schnoebelen, Philippe Informatique Grenoble INPG 1994. URL: http://www.theses.fr/1994INPG0136.
  34. Oded Maler and Ludwig Staiger. On syntactic congruences for ω-languages. Theoretical Computer Science, 183(1):93-112, 1997. Formal Language Theory. URL: https://doi.org/10.1016/S0304-3975(96)00312-X.
  35. Nicolas Markey and Philippe Schnoebelen. Model Checking a Path (Preliminary Report). In Amadio, Roberto M., Lugiez, and Denis, editors, Lecture Notes in Computer Science, volume 2761 of Lecture Notes in Computer Science, pages 251-265, Marseilles, France, 2003. Springer. URL: https://doi.org/10.1007/b11938.
  36. Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9(5):521-530, 1966. URL: https://doi.org/10.1016/S0019-9958(66)80013-X.
  37. Fabio Mogavero, Aniello Murano, and Luigi Sauro. A behavioral hierarchy of strategy logic. In Nils Bulling, Leendert van der Torre, Serena Villata, Wojtek Jamroga, and Wamberto Vasconcelos, editors, Computational Logic in Multi-Agent Systems, pages 148-165, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-09764-0_10.
  38. Jessica Newman and Benjamin Plummer. Positional properties in temporal logic, 2026. URL: https://doi.org/10.48550/arXiv.2604.25628.
  39. Pierre Ohlmann. Characterizing positionality in games of infinite duration over infinite graphs. TheoretiCS, Volume 2, January 2023. URL: https://doi.org/10.46298/theoretics.23.3.
  40. Pierre Ohlmann and Michał Skrzypczak. Positionality in Σ⁰₂ and a Completeness Result. In Olaf Beyersdorff, Mamadou Moustapha Kanté, Orna Kupferman, and Daniel Lokshtanov, editors, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024), volume 289 of Leibniz International Proceedings in Informatics (LIPIcs), pages 54:1-54:18, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.STACS.2024.54.
  41. Dominique Perrin and Jean Éric Pin. Ii - automata and semigroups. In Dominique Perrin and Jean Éric Pin, editors, Infinite Words, volume 141 of Pure and Applied Mathematics, pages 75-131. Elsevier, 2004. URL: https://doi.org/10.1016/S0079-8169(04)80003-5.
  42. Dominique Perrin and Jean Éric Pin. Vi - varieties. In Dominique Perrin and Jean Éric Pin, editors, Infinite Words, volume 141 of Pure and Applied Mathematics, pages 265-306. Elsevier, 2004. URL: https://doi.org/10.1016/S0079-8169(04)80007-2.
  43. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pages 46-57, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  44. Libor Polák. A classification of rational languages by semilattice-ordered monoids. Archivum Mathematicum, 040(4):395-406, 2004. URL: http://eudml.org/doc/249314.
  45. J. Richard Büchi. Symposium on decision problems: On a decision method in restricted second order arithmetic. In Ernest Nagel, Patrick Suppes, and Alfred Tarski, editors, Logic, Methodology and Philosophy of Science, volume 44 of Studies in Logic and the Foundations of Mathematics, pages 1-11. Elsevier, 1966. URL: https://doi.org/10.1016/S0049-237X(09)70564-6.
  46. Pierre-Yves Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85(2):82-93, 2004. LCMAS 2003, Logic and Communication in Multi-Agent Systems. URL: https://doi.org/10.1016/S1571-0661(05)82604-0.
  47. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, July 1985. URL: https://doi.org/10.1145/3828.3837.
  48. Pierre Vandenhove. Strategy complexity of zero-sum games on graphs. Theses, Université Paris-Saclay ; Université de Mons (Belgique), April 2023. URL: https://theses.hal.science/tel-04095220.
  49. Pierre Wolper. Temporal logic can be more expressive. Information and Control, 56(1):72-99, 1983. URL: https://doi.org/10.1016/S0019-9958(83)80051-5.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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