Document Open Access Logo

Positive and Monotone Fragments of FO and LTL

Authors Simon Iosti, Denis Kuperberg , Quentin Moreau

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2025.162.pdf
  • Filesize: 0.79 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Regular languages
  • Theory of computation → Logic and verification
Keywords
  • Positive logic
  • LTL
  • separation
  • first-order
  • monotone

Metrics

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

Abstract

We study the positive logic FO^+ on finite words, and its fragments, pursuing and refining the work initiated in [Denis Kuperberg, 2023]. First, we transpose notorious logic equivalences into positive first-order logic: FO^+ is equivalent to LTL^+, and its two-variable fragment FO^{2+} with (resp. without) successor available is equivalent to UTL^+ with (resp. without) the "next" operator X available. This shows that despite previous negative results, the class of FO^+-definable languages exhibits some form of robustness. We then exhibit an example of an FO-definable monotone language on one predicate, that is not FO^+-definable, refining the example from [Denis Kuperberg, 2023] with 3 predicates. Moreover, we show that such a counter-example cannot be FO²-definable. Finally, we provide a new example distinguishing the positive and monotone versions of FO² without quantifier alternation. This does not rely on a variant of the previously known counter-example, and witnesses a new phenomenon.

Cite As Get BibTex

Simon Iosti, Denis Kuperberg, and Quentin Moreau. Positive and Monotone Fragments of FO and LTL. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 162:1-162:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ICALP.2025.162

Author Details

Simon Iosti
  • LIP, ENS Lyon, France
Denis Kuperberg
  • CNRS, LIP, ENS Lyon, France
Quentin Moreau
  • ENS Lyon, France

Funding

  • Kuperberg, Denis: ANR ReCiProg.

References

  1. Miklos Ajtai and Yuri Gurevich. Monotone versus positive. J. ACM, 34(4):1004-1015, October 1987. URL: https://doi.org/10.1145/31846.31852.
  2. David Baelde and Dale Miller. Least and greatest fixed points in linear logic. In Nachum Dershowitz and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 92-106, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-75560-9_9.
  3. Julian Bradfield and Igor Walukiewicz. The mu-calculus and model checking. In Handbook of Model Checking, pages 871-919. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_26.
  4. Thomas Colcombet. Regular Cost Functions, Part I: Logic and Algebra over Words. Logical Methods in Computer Science, Volume 9, Issue 3, August 2013. URL: https://doi.org/10.2168/LMCS-9(3:3)2013.
  5. Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. BRICS Report Series, 4(5), January 1997. URL: https://doi.org/10.7146/brics.v4i5.18784.
  6. Dov M. Gabbay, Ian Hodkinson, and Mark Reynolds. Temporal logic (vol. 1): mathematical foundations and computational aspects. Oxford University Press, Inc., USA, 1994. Google Scholar
  7. Michelangelo Grigni and Michael Sipser. Monotone complexity. In Poceedings of the London Mathematical Society Symposium on Boolean Function Complexity, pages 57-75, USA, 1992. Cambridge University Press. Google Scholar
  8. Neil Immerman. Relational queries computable in polynomial time. Information and Control, 68(1):86-104, 1986. URL: https://doi.org/10.1016/S0019-9958(86)80029-8.
  9. Hans Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California Los Angeles, 1968. Published as Johan Anthony Willem Kamp. URL: http://www.ims.uni-stuttgart.de/archiv/kamp/files/1968.kamp.thesis.pdf.
  10. Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing. Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership. Log. Methods Comput. Sci., 16(3), 2020. URL: https://lmcs.episciences.org/6765.
  11. Denis Kuperberg. Positive first-order logic on words and graphs. Log. Methods Comput. Sci., 19(3), 2023. URL: https://doi.org/10.46298/lmcs-19(3:7)2023.
  12. Denis Kuperberg and Michael Vanden Boom. On the expressive power of cost logics over infinite words. In Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer, editors, Automata, Languages, and Programming, pages 287-298, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-31585-5_28.
  13. Roger C. Lyndon. Properties preserved under homomorphism. Pacific J. Math., 9(1):143-154, 1959. URL: https://projecteuclid.org:443/euclid.pjm/1103039459.
  14. Charles Paperman. Semigroup online. URL: https://paperman.name/semigroup/.
  15. Jean-Éric Pin and Pascal Weil. Polynomial closure and unambiguous product. Theory of Computing Systems, 30:383-422, 1995. URL: https://api.semanticscholar.org/CorpusID:850708.
  16. Benjamin Rossman. Homomorphism preservation theorems. J. ACM, 55, July 2008. URL: https://doi.org/10.1145/1379759.1379763.
  17. Alexei P. Stolboushkin. Finitely monotone properties. In LICS, San Diego, California, USA, June 26-29, 1995, pages 324-330. IEEE Computer Society, 1995. URL: https://doi.org/10.1109/LICS.1995.523267.
  18. Denis Thérien and Thomas Wilke. Over words, two variables are as powerful as one quantifier alternation. In Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing, STOC '98, pages 234-240, New York, NY, USA, 1998. Association for Computing Machinery. URL: https://doi.org/10.1145/276698.276749.
  19. Moshe Y. Vardi. The complexity of relational query languages (extended abstract). In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC '82, pages 137-146, New York, NY, USA, 1982. Association for Computing Machinery. URL: https://doi.org/10.1145/800070.802186.
  20. Philipp Weis and Neil Immerman. Structure Theorem and Strict Alternation Hierarchy for FO2 on Words. In Thomas Schwentick, Denis Thérien, and Heribert Vollmer, editors, Circuits, Logic, and Games, volume 6451 of Dagstuhl Seminar Proceedings (DagSemProc), pages 1-22, Dagstuhl, Germany, 2007. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/DagSemProc.06451.6.
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