Document Open Access Logo

VLDL Satisfiability and Model Checking via Tree Automata

Author Alexander Weinert

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2017.47.pdf
  • Filesize: 0.55 MB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • Visibly Linear Dynamic Logic
  • Visibly Pushdown Languages
  • Satisfiability
  • Model Checking
  • Tree Automata

Metrics

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

Abstract

We present novel algorithms solving the satisfiability problem and the model checking problem for Visibly Linear Dynamic Logic (VLDL) in asymptotically optimal time via a reduction to the emptiness problem for tree automata with Büchi acceptance.
Since VLDL allows for the specification of important properties of recursive systems, this reduction enables the efficient analysis of such systems.

Furthermore, as the problem of tree automata emptiness is well-studied, this reduction enables leveraging the mature algorithms and tools for that problem in order to solve the satisfiability problem and the model checking problem for VLDL.

Cite As Get BibTex

Alexander Weinert. VLDL Satisfiability and Model Checking via Tree Automata. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 47:1-47:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2017.47

Author Details

Alexander Weinert

References

  1. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. URL: http://dx.doi.org/10.1145/585265.585270.
  2. Rajeev Alur and P. Madhusudan. Visibly pushdown languages. In László Babai, editor, Proceedings of the 36th Annual ACM Symposium on Theory of Computing, Chicago, IL, USA, June 13-16, 2004, pages 202-211. ACM, 2004. URL: http://dx.doi.org/10.1145/1007352.1007390.
  3. Thomas Ball and Sriram K. Rajamani. Bebop: A symbolic model checker for boolean programs. In Klaus Havelund, John Penix, and Willem Visser, editors, SPIN Model Checking and Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30 - September 1, 2000, Proceedings, volume 1885 of Lecture Notes in Computer Science, pages 113-130. Springer, 2000. URL: http://dx.doi.org/10.1007/10722468_7.
  4. Thomas Ball and Sriram K. Rajamani. Bebop: a path-sensitive interprocedural dataflow engine. In John Field and Gregor Snelting, editors, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE'01, Snowbird, Utah, USA, June 18-19, 2001, pages 97-103. ACM, 2001. URL: http://dx.doi.org/10.1145/379605.379690.
  5. Laura Bozzelli. Alternating automata and a temporal fixpoint calculus for visibly pushdown languages. In Luís Caires and Vasco Thudichum Vasconcelos, editors, CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings, volume 4703 of Lecture Notes in Computer Science, pages 476-491. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-74407-8_32.
  6. Laura Bozzelli and César Sánchez. Visibly Linear Temporal Logic. J. Aut. Reas., 2018. In Press. URL: http://dx.doi.org/10.1007/s10817-017-9410-z.
  7. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Algorithms for büchi games. CoRR, abs/0805.2620, 2008. URL: http://arxiv.org/abs/0805.2620.
  8. Nathanaël Fijalkow, Sophie Pinchinat, and Olivier Serre. Emptiness of alternating tree automata using games with imperfect information. In Anil Seth and Nisheeth K. Vishnoi, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, December 12-14, 2013, Guwahati, India, volume 24 of LIPIcs, pages 299-311. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2013.299.
  9. Oliver Friedmann and Martin Lange. The PGSolver Collection of Parity Game Solvers. University of Munich, 2009. Available at URL: https://github.com/tcsprojects/pgsolver/blob/b88e86e31f2fe02ebcabdccd51ee73f2692ac884/doc/pgsolver.pdf.
  10. Jeroen Keiren. An experimental study of algorithms and optimisations for parity games, with an application to Boolean Equation Systems. Master’s thesis, Eindhoven University of Technology, 2009. Available at URL: http://www.jeroenkeiren.nl/publications.
  11. Orna Kupferman and Moshe Y. Vardi. Weak alternating automata and tree automata emptiness. In Jeffrey Scott Vitter, editor, Proceedings of the Thirtieth Annual ACM Symposium on the Theory of Computing, Dallas, Texas, USA, May 23-26, 1998, pages 224-233. ACM, 1998. URL: http://dx.doi.org/10.1145/276698.276748.
  12. Orna Kupferman and Moshe Y. Vardi. From linear time to branching time. ACM Trans. Comput. Log., 6(2):273-294, 2005. URL: http://dx.doi.org/10.1145/1055686.1055689.
  13. Christof Löding, Parthasarathy Madhusudan, and Olivier Serre. Visibly Pushdown Games. In L. Lodaya and M. Mahajan, editors, FSTTCS 2004, volume 3328 of LNCS, pages 408-420. Springer, 2005. URL: http://dx.doi.org/10.1007/978-3-540-30538-5_34.
  14. Satoru Miyano and Takeshi Hayashi. Alternating finite automata on omega-words. Theor. Comput. Sci., 32:321-330, 1984. URL: http://dx.doi.org/10.1016/0304-3975(84)90049-5.
  15. Frank Nießner. Nondeterministic tree automata. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors, Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science, pages 135-152. Springer, 2001. URL: http://dx.doi.org/10.1007/3-540-36387-4_8.
  16. 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.
  17. Yuval Rabani, editor. Proceedings of the Twenty-Third Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2012, Kyoto, Japan, January 17-19, 2012. SIAM, 2012. URL: http://dx.doi.org/10.1137/1.9781611973099.
  18. Stefan Schwoon. Model checking pushdown systems. PhD thesis, Technical University Munich, Germany, 2002. URL: http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/schwoon.html.
  19. Dejvuth Suwimonteerabuth, Stefan Schwoon, and Javier Esparza. jmoped: A java bytecode checker based on moped. In Nicolas Halbwachs and Lenore D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3440 of Lecture Notes in Computer Science, pages 541-545. Springer, 2005. URL: http://dx.doi.org/10.1007/978-3-540-31980-1_35.
  20. Wolfgang Thomas. Automata on Infinite Objects. Handbook of theoretical computer science, Volume B, pages 133-191, 1990. Google Scholar
  21. Wolfgang Thomas. Languages, Automata, and Logic. In Handbook of formal languages, pages 389-455. Springer, 1997. Google Scholar
  22. Moshe Y. Vardi. Automata-theoretic model checking revisited. In Hana Chockler and Alan J. Hu, editors, Hardware and Software: Verification and Testing, 4th International Haifa Verification Conference, HVC 2008, Haifa, Israel, October 27-30, 2008. Proceedings, volume 5394 of Lecture Notes in Computer Science, page 2. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-642-01702-5_2.
  23. Alexander Weinert. VLDL satisfiability and model checking via tree automata. CoRR, abs/1708.00699, 2017. URL: http://arxiv.org/abs/1708.00699.
  24. Alexander Weinert and Martin Zimmermann. Visibly linear dynamic logic. In Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen, editors, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, 2016, Chennai, India, volume 65 of LIPIcs, pages 28:1-28:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.28.
  25. Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci., 200(1-2):135-183, 1998. URL: http://dx.doi.org/10.1016/S0304-3975(98)00009-7.
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