Document Open Access Logo

Model-Checking Counting Temporal Logics on Flat Structures

Authors Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, Daniel Thoma

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.29.pdf
  • Filesize: 0.69 MB
  • 17 pages

Document Identifiers

Author Details

Normann Decker
Peter Habermehl
Martin Leucker
Arnaud Sangnier
Daniel Thoma

Cite As Get BibTex

Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, and Daniel Thoma. Model-Checking Counting Temporal Logics on Flat Structures. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CONCUR.2017.29

Abstract

We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the model-checking problem is undecidable, but we show that decidability can be recovered by considering flat Kripke structures where each state belongs to at most one simple loop. Most decision procedures are based on results on (flat) counter systems where counters are used to implement the evaluation of counting operators.

Subject Classification

Keywords
  • Counting Temporal Logic
  • Model checking
  • Flat Kripke Structure

Metrics

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

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Roland Meyer, and Mehdi Seyed Salehi. What’s decidable about availability languages? In Prahladh Harsha and G. Ramalingam, editors, 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India, volume 45 of LIPIcs, pages 192-205. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.192.
  2. H. Apelt. Axiomatische Untersuchungen über einige mit der Presburgerschen Arithmetik verwandten Systeme. Z. Math. Logik Grundlagen Math., 12:131-168, 1966. Google Scholar
  3. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  4. Leonard Berman. The complexitiy of logical theories. Theor. Comput. Sci., 11:71-77, 1980. URL: http://dx.doi.org/10.1016/0304-3975(80)90037-7.
  5. Benedikt Bollig, Normann Decker, and Martin Leucker. Frequency linear-time temporal logic. In Tiziana Margaria, Zongyan Qiu, and Hongli Yang, editors, Sixth International Symposium on Theoretical Aspects of Software Engineering, TASE 2012, 4-6 July 2012, Beijing, China, pages 85-92. IEEE Computer Society, 2012. URL: http://dx.doi.org/10.1109/TASE.2012.43.
  6. Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In Antoni W. Mazurkiewicz and Józef Winkowski, editors, CONCUR '97: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings, volume 1243 of Lecture Notes in Computer Science, pages 135-150. Springer, 1997. URL: http://dx.doi.org/10.1007/3-540-63141-0_10.
  7. Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Dexter Kozen, editor, Logics of Programs, Workshop, Yorktown Heights, New York, May 1981, volume 131 of Lecture Notes in Computer Science, pages 52-71. Springer, 1981. URL: http://dx.doi.org/10.1007/BFb0025774.
  8. Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis. Model checking: algorithmic verification and debugging. Commun. ACM, 52(11):74-84, 2009. URL: http://dx.doi.org/10.1145/1592761.1592781.
  9. Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, and Daniel Thoma. Model-checking counting temporal logics on flat structures. CoRR, abs/1706.08608, 2017. URL: http://arxiv.org/abs/1706.08608.
  10. Stéphane Demri, Amit Kumar Dhar, and Arnaud Sangnier. Equivalence between model-checking flat counter systems and Presburger arithmetic. In Joël Ouaknine, Igor Potapov, and James Worrell, editors, Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings, volume 8762 of Lecture Notes in Computer Science, pages 85-97. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11439-2_7.
  11. Stéphane Demri, Amit Kumar Dhar, and Arnaud Sangnier. Taming past LTL and flat counter systems. Inf. Comput., 242:306-339, 2015. URL: http://dx.doi.org/10.1016/j.ic.2015.03.007.
  12. Stéphane Demri, Alain Finkel, Valentin Goranko, and Govert van Drimmelen. Model-checking CTL* over flat Presburger counter systems. Journal of Applied Non-Classical Logics, 20(4):313-344, 2010. URL: http://dx.doi.org/10.3166/jancl.20.313-344.
  13. Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. URL: http://dx.doi.org/10.1145/1507244.1507246.
  14. E. Allen Emerson and Joseph Y. Halpern. "Sometimes" and "not never" revisited: On branching versus linear time. In John R. Wright, Larry Landweber, Alan J. Demers, and Tim Teitelbaum, editors, Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 1983, pages 127-140. ACM Press, 1983. URL: http://dx.doi.org/10.1145/567067.567081.
  15. Alain Finkel and Jérôme Leroux. How to compose Presburger-accelerations: Applications to broadcast protocols. In Manindra Agrawal and Anil Seth, editors, FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 22nd Conference Kanpur, India, December 12-14, 2002, Proceedings, volume 2556 of Lecture Notes in Computer Science, pages 145-156. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-36206-1_14.
  16. Jochen Hoenicke, Roland Meyer, and Ernst-Rüdiger Olderog. Kleene, rabin, and scott are available. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 462-477. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15375-4_32.
  17. Lars Kuhtz and Bernd Finkbeiner. Weak Kripke structures and LTL. In Joost-Pieter Katoen and Barbara König, editors, CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 419-433. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-23217-6_28.
  18. François Laroussinie, Antoine Meyer, and Eudes Petonnet. Counting LTL. In Nicolas Markey and Jef Wijsen, editors, TIME 2010 - 17th International Symposium on Temporal Representation and Reasoning, Paris, France, 6-8 September 2010, pages 51-58. IEEE Computer Society, 2010. URL: http://dx.doi.org/10.1109/TIME.2010.20.
  19. François Laroussinie, Antoine Meyer, and Eudes Petonnet. Counting CTL. Logical Methods in Computer Science, 9(1), 2012. URL: http://dx.doi.org/10.2168/LMCS-9(1:3)2013.
  20. Jérôme Leroux and Grégoire Sutre. Flat counter automata almost everywhere! In Doron A. Peled and Yih-Kuen Tsay, editors, Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings, volume 3707 of Lecture Notes in Computer Science, pages 489-503. Springer, 2005. URL: http://dx.doi.org/10.1007/11562948_36.
  21. M. Minsky. Computation, Finite and Infinite Machines. Prentice Hall, 1967. Google Scholar
  22. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46-57. IEEE Computer Society, 1977. URL: http://dx.doi.org/10.1109/SFCS.1977.32.
  23. M. Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du premier congrès de mathématiciens des Pays Slaves, Warszawa, pages 92-101, 1929. Google Scholar
  24. William Pugh. Counting solutions to Presburger formulas: How and why. In Vivek Sarkar, Barbara G. Ryder, and Mary Lou Soffa, editors, Proceedings of the ACM SIGPLAN'94 Conference on Programming Language Design and Implementation (PLDI), Orlando, Florida, USA, June 20-24, 1994, pages 121-134. ACM, 1994. URL: http://dx.doi.org/10.1145/178243.178254.
  25. Nicole Schweikardt. Arithmetic, first-order logic, and counting quantifiers. ACM Trans. Comput. Log., 6(3):634-671, 2005. URL: http://dx.doi.org/10.1145/1071596.1071602.
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