Document Open Access Logo

The Complexity of Counting Models of Linear-time Temporal Logic

Authors Hazem Torfah, Martin Zimmermann

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2014.241.pdf
  • Filesize: 0.49 MB
  • 12 pages

Document Identifiers

Subject Classification

Keywords
  • Model Counting
  • Temporal Logic
  • Model Checking
  • Counting Complexity

Metrics

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

Abstract

We determine the complexity of counting models of bounded size of specifications expressed in Linear-time Temporal Logic. Counting word-models is #P-complete, if the bound is given in unary, and as hard as counting accepting runs of nondeterministic polynomial space Turing machines, if the bound is given in binary. Counting tree-models is as hard as counting accepting runs of nondeterministic exponential time Turing machines, if the bound is given in unary. For a binary encoding of the bound, the problem is at least as hard as counting accepting runs of nondeterministic exponential space Turing machines. On the other hand, it is not harder than counting accepting runs of nondeterministic doubly-exponential time Turing machines.

Cite As Get BibTex

Hazem Torfah and Martin Zimmermann. The Complexity of Counting Models of Linear-time Temporal Logic. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 241-252, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/LIPIcs.FSTTCS.2014.241

Author Details

Hazem Torfah
Martin Zimmermann

References

  1. Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, New York, NY, USA, 1st edition, 2009. Google Scholar
  2. Armin Biere. Bounded model checking. In Handbook of Satisfiability, pages 457-481. IOS Press, 2009. Google Scholar
  3. Roderick Bloem, Hans-Jürgen Gamauf, Georg Hofferek, Bettina Könighofer, and Robert Könighofer. Synthesizing robust systems with RATSY. In Doron Peled and Sven Schewe, editors, SYNT, volume 84 of EPTCS, pages 47-53. Open Publishing Association, 2012. Google Scholar
  4. Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. Acacia+, a tool for LTL synthesis. In P. Madhusudan and Sanjit A. Seshia, editors, CAV, volume 7358 of LNCS, pages 652-657. Springer, 2012. Google Scholar
  5. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 10^20 states and beyond. Inf. Comput., 98(2):142-170, 1992. Google Scholar
  6. Rüdiger Ehlers. Unbeast: Symbolic bounded synthesis. In TACAS, volume 6605 of LNCS, pages 272-275. Springer-Verlag, 2011. Google Scholar
  7. Bernd Finkbeiner and Sven Schewe. Bounded synthesis. International Journal on Software Tools for Technology Transfer, 15(5-6):519-539, 2013. Google Scholar
  8. Bernd Finkbeiner and Hazem Torfah. Counting models of linear-time temporal logic. In Adrian Horia Dediu, Carlos Martín-Vide, José Luis Sierra-Rodríguez, and Bianca Truthe, editors, LATA, volume 8370 of LNCS, pages 360-371. Springer, 2014. Google Scholar
  9. Lane A. Hemaspaandra and Heribert Vollmer. The satanic notations: counting classes beyond #P and other definitional adventures. SIGACT News, 26(1):2-13, 1995. Google Scholar
  10. Lars Kuhtz and Bernd Finkbeiner. LTL path checking is efficiently parallelizable. In Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris Nikoletseas, and Wolfgang Thomas, editors, ICALP, volume 5556 of LNCS, pages 235-246. Springer, 2009. Google Scholar
  11. Richard E. Ladner. Polynomial space counting problems. SIAM J. Comput., 18(6):1087-1097, 1989. Google Scholar
  12. Maciej Liśkiewicz, Mitsunori Ogihara, and Seinosuke Toda. The complexity of counting self-avoiding walks in subgraphs of two-dimensional grids and hypercubes. Theor. Comput. Sci., 1-3(304):129-156, 2003. Google Scholar
  13. Michael L. Littman, Stephen M. Majercik, and Toniann Pitassi. Stochastic boolean satisfiability. Journal of Automated Reasoning, 27:2001, 2000. Google Scholar
  14. Markus Lohrey and Manfred Schmidt-Schauß. Processing succinct matrices and vectors. In Edward A. Hirsch, Sergei O. Kuznetsov, Jean-Éric Pin, and Nikolay K. Vereshchagin, editors, CSR, volume 8476 of LNCS, pages 245-258. Springer, 2014. Google Scholar
  15. Daniel Morwood and Daniel Bryce. Evaluating temporal plans in incomplete domains. In Jörg Hoffmann and Bart Selman, editors, AAAI. AAAI Press, 2012. Google Scholar
  16. Amir Pnueli. The temporal logic of programs. In STOC, SFCS'77, pages 46-57, Washington, DC, USA, 1977. IEEE Computer Society. Google Scholar
  17. A. Prasad Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing, 6(5):495-511, 1994. Google Scholar
  18. A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. Google Scholar
  19. Hazem Torfah and Martin Zimmermann. The complexity of counting models of linear-time temporal logic. ArXiv e-prints, abs/1408.5752, 2014. Google Scholar
  20. Leslie G. Valiant. The complexity of computing the permanent. Theor. Comput. Sci., 8:189-201, 1979. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact