Document Open Access Logo

Promptness and Fairness in Muller LTL Formulas

Authors Damien Busatto-Gaston , Youssouf Oualhadj , Léo Tible, Daniele Varacca

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2024.15.pdf
  • Filesize: 0.87 MB
  • 22 pages

Document Identifiers

Author Details

Damien Busatto-Gaston
  • Univ Paris Est Creteil, LACL, F-94010 Creteil, France
Youssouf Oualhadj
  • Univ Paris Est Creteil, LACL, F-94010 Creteil, France
  • CNRS, ReLaX, IRL 2000, Siruseri, India
Léo Tible
  • Univ Paris Est Creteil, LACL, F-94010 Creteil, France
Daniele Varacca
  • Univ Paris Est Creteil, LACL, F-94010 Creteil, France

Cite As Get BibTex

Damien Busatto-Gaston, Youssouf Oualhadj, Léo Tible, and Daniele Varacca. Promptness and Fairness in Muller LTL Formulas. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 15:1-15:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.FSTTCS.2024.15

Abstract

In this paper we consider two different views of the model checking problem for the Linear Temporal Logic (LTL). On the one hand, we consider the universal model checking problem for LTL, where one asks that for a given system and a given formula all the runs of the system satisfy the formula. On the other hand, the fair model checking problem for LTL asks that for a given system and a given formula almost all the runs of the system satisfy the formula.
It was shown that these two problems have the same theoretical complexity, i.e. PSPACE-complete. A less expensive fragment was identified in a previous work, namely the Muller fragment, which consists of combinations of repeated reachability properties.
We consider prompt LTL formulas (pLTL), that extend LTL with an additional operator, i.e. the prompt-eventually. This operator ensures the existence of a bound such that reachability properties are satisfied within this bound. This extension comes at no cost since the model checking problem remains PSPACE-complete.
We show that the corresponding Muller fragment of pLTL, with prompt repeated reachability properties, enjoys similar computational improvements. Another feature of Muller formulas is that the model checking problem becomes easier under the fairness assumption. This distinction is lost in the prompt setting, as we show that the two problems are equivalent instance-wise. Subsequently, we identify a new prefix independent fragment of pLTL for which the fair model checking problem is less expensive than the universal one.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Model checking
  • Fairness
  • Temporal logics

Metrics

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

Related Versions

References

  1. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  2. Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour. Life is random, time is not: Markov decision processes with window objectives. Log. Methods Comput. Sci., 16(4), 2020. URL: https://lmcs.episciences.org/6975.
  3. Véronique Bruyère, Quentin Hautem, and Mickael Randour. Window parity games: an alternative approach toward parity games with time bounds. In Domenico Cantone and Giorgio Delzanno, editors, Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016, volume 226 of EPTCS, pages 135-148, 2016. URL: https://doi.org/10.4204/EPTCS.226.10.
  4. Damien Busatto-Gaston, Youssouf Oualhadj, Léo Tible, and Daniele Varacca. Fairness and promptness in muller formulas, 2024. URL: https://arxiv.org/abs/2204.13215.
  5. Diego Calvanese, Giuseppe De Giacomo, and Moshe Y. Vardi. Reasoning about actions and planning in LTL action theories. In Dieter Fensel, Fausto Giunchiglia, Deborah L. McGuinness, and Mary-Anne Williams, editors, Proceedings of the Eights International Conference on Principles and Knowledge Representation and Reasoning (KR-02), Toulouse, France, April 22-25, 2002, pages 593-602. Morgan Kaufmann, 2002. Google Scholar
  6. Krishnendu Chatterjee. Concurrent games with tail objectives. Theor. Comput. Sci., 388(1-3):181-198, 2007. URL: https://doi.org/10.1016/j.tcs.2007.07.047.
  7. Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin. Looking at mean-payoff and total-payoff through windows. Inf. Comput., 242:25-52, 2015. URL: https://doi.org/10.1016/j.ic.2015.03.010.
  8. Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., 8(2):244-263, 1986. URL: https://doi.org/10.1145/5397.5399.
  9. Costas Courcoubetis and Mihalis Yannakakis. The complexity of probabilistic verification. J. ACM, 42(4):857-907, 1995. URL: https://doi.org/10.1145/210332.210339.
  10. E. Allen Emerson and Chin-Laung Lei. Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program., 8(3):275-306, 1987. URL: https://doi.org/10.1016/0167-6423(87)90036-0.
  11. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning About Knowledge. MIT Press, Cambridge, MA, USA, 2003. Google Scholar
  12. Giuseppe De Giacomo and Moshe Y. Vardi. Automata-theoretic approach to planning for temporally extended goals. In Susanne Biundo and Maria Fox, editors, Recent Advances in AI Planning, 5th European Conference on Planning, ECP'99, Durham, UK, September 8-10, 1999, Proceedings, volume 1809 of Lecture Notes in Computer Science, pages 226-238. Springer, 1999. URL: https://doi.org/10.1007/10720246_18.
  13. Hugo Gimbert and Florian Horn. Solving simple stochastic tail games. In Moses Charikar, editor, Proceedings of the Twenty-First Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2010, Austin, Texas, USA, January 17-19, 2010, pages 847-862. SIAM, 2010. URL: https://doi.org/10.1137/1.9781611973075.69.
  14. Hugo Gimbert and Edon Kelmendi. Two-player perfect-information shift-invariant submixing stochastic games are half-positional. CoRR, abs/1401.6575, 2014. URL: https://arxiv.org/abs/1401.6575.
  15. 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.
  16. Anca Muscholl and Igor Walukiewicz. An np-complete fragment of LTL. Int. J. Found. Comput. Sci., 16(4):743-753, 2005. URL: https://doi.org/10.1142/S0129054105003261.
  17. 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.
  18. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989, pages 179-190. ACM Press, 1989. URL: https://doi.org/10.1145/75277.75293.
  19. Amir Pnueli and Roni Rosner. On the synthesis of an asynchronous reactive module. In Giorgio Ausiello, Mariangiola Dezani-Ciancaglini, and Simona Ronchi Della Rocca, editors, Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11-15, 1989, Proceedings, volume 372 of Lecture Notes in Computer Science, pages 652-671. Springer, 1989. URL: https://doi.org/10.1007/BFb0035790.
  20. Jean-Pierre Queille and Joseph Sifakis. Specification and verification of concurrent systems in CESAR. In Mariangiola Dezani-Ciancaglini and Ugo Montanari, editors, International Symposium on Programming, 5th Colloquium, Torino, Italy, April 6-8, 1982, Proceedings, volume 137 of Lecture Notes in Computer Science, pages 337-351. Springer, 1982. URL: https://doi.org/10.1007/3-540-11494-7_22.
  21. Matthias Schmalz, Hagen Völzer, and Daniele Varacca. Model checking almost all paths can be less expensive than checking all paths. In Vikraman Arvind and Sanjiva Prasad, editors, FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 27th International Conference, New Delhi, India, December 12-14, 2007, Proceedings, volume 4855 of Lecture Notes in Computer Science, pages 532-543. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-77050-3_44.
  22. A. Sistla and Edmund Clarke. The complexity of propositional linear temporal logics. J. ACM, 32:733-749, July 1985. URL: https://doi.org/10.1145/800070.802189.
  23. Hagen Völzer and Daniele Varacca. Defining fairness in reactive and concurrent systems. J. ACM, 59(3):13:1-13:37, 2012. URL: https://doi.org/10.1145/2220357.2220360.
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