Document Open Access Logo

Streett Automata Model Checking of Higher-Order Recursion Schemes

Authors Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, Takeshi Tsukada

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.32.pdf
  • Filesize: 1.11 MB
  • 18 pages

Document Identifiers

Author Details

Ryota Suzuki
Koichi Fujima
Naoki Kobayashi
Takeshi Tsukada

Cite As Get BibTex

Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, and Takeshi Tsukada. Streett Automata Model Checking of Higher-Order Recursion Schemes. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.32

Abstract

We propose a practical algorithm for Streett automata model checking of higher-order recursion schemes (HORS), which checks whether the tree generated by a given HORS is accepted by a given Streett automaton. The Streett automata model checking of HORS is useful in the context of liveness verification of higher-order functional programs. The previous approach to Streett automata model checking converted Streett automata to parity automata and then invoked a parity tree automata model checker. We show through experiments that our direct approach outperforms the previous approach. Besides being able to directly deal with Streett automata, our algorithm is the first practical Streett or parity automata model checking algorithm that runs in time polynomial in the size of HORS, assuming that the other parameters are fixed. Previous practical fixed-parameter polynomial time algorithms for HORS could only deal with the class of trivial tree automata. We have confirmed through experiments that (a parity automata version of) our model checker outperforms previous parity automata model checkers for HORS.

Subject Classification

Keywords
  • Higher-order model checking
  • higher-order recursion schemes
  • Streett automata

Metrics

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

References

  1. Klaus Aehlig, Jolie G. de Miranda, and C.-H. Luke Ong. The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable. In TLCA 2005, volume 3461 of LNCS, pages 39-54. Springer, 2005. URL: http://dx.doi.org/10.1007/11417170_5.
  2. Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, and Akash Lal. Detecting fair non-termination in multithreaded programs. In Proc. of CAV 2012, volume 7358 of LNCS, pages 210-226. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31424-7_19.
  3. Christopher H. Broadbent and Naoki Kobayashi. Saturation-based model checking of higher-order recursion schemes. In Proc. of CSL 2013, volume 23 of LIPIcs, pages 129-148, 2013. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2013.129.
  4. Nils Buhrke, Helmut Lescow, and Jens Vöge. Strategy construction in infinite ganes with streett and rabin chain winning conditions. In TACAS, volume 1055 of Lecture Notes in Computer Science, pages 207-224. Springer, 1996. Google Scholar
  5. Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Y. Vardi. Proving that programs eventually do something good. In Proc. of POPL, pages 265-276. ACM Press, 2007. Google Scholar
  6. Oliver Friedmann and Martin Lange. PGSolver. Available at URL: https://github.com/tcsprojects/pgsolver.
  7. Koichi Fujima, Sohei Ito, and Naoki Kobayashi. Practical alternating parity tree automata model checking of higher-order recursion schemes. In Proc. of APLAS 2013, volume 8301 of LNCS, pages 17-32, 2013. Google Scholar
  8. E. Grädel, W. Thomas, and T. Wilke. Automata, Logics, and Infinite Games: A Guide to Current Research. LNCS. Springer, 2002. Google Scholar
  9. Charles Grellois. Semantics of linear logic and higher-order model-checking. PhD thesis, Universit'e Paris Diderot, 2016. Google Scholar
  10. Charles Grellois and Paul-André Melliès. Relational semantics of linear logic and higher-order model checking. In CSL, volume 41 of LIPIcs, pages 260-276. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. Google Scholar
  11. Nevin Heintze and David McAllester. On the cubic bottleneck in subtyping and flow analysis. In Proc. of LICS, pages 342-351, 1997. Google Scholar
  12. Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Deciding monadic theories of hyperalgebraic trees. In TLCA, volume 2044 of LNCS, pages 253-267. Springer, 2001. Google Scholar
  13. Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Higher-order pushdown trees are easy. In FoSSaCS 2002, volume 2303 of LNCS, pages 205-222. Springer, 2002. Google Scholar
  14. Naoki Kobayashi. Model-checking higher-order functions. In Proc. of PPDP 2009, pages 25-36. ACM Press, 2009. Google Scholar
  15. Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Proc. of POPL, pages 416-428. ACM Press, 2009. Google Scholar
  16. Naoki Kobayashi. A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes. In Proc. of FoSSaCS 2011, volume 6604 of LNCS, pages 260-274. Springer, 2011. Google Scholar
  17. Naoki Kobayashi. Model checking higher-order programs. Journal of the ACM, 60(3), 2013. Google Scholar
  18. Naoki Kobayashi. HorSat2: A saturation-based model checker for hors. A tool available from http://www-kb.is.s.u-tokyo.ac.jp/~koba/horsat2/, 2016.
  19. Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proc. of LICS 2009, pages 179-188. IEEE Computer Society Press, 2009. Google Scholar
  20. Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. A draft of the longer version of [20], available from http://www-kb.is.s.u-tokyo.ac.jp/~koba/papers/lics09-full.pdf, 2012.
  21. Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. Predicate abstraction and CEGAR for higher-order model checking. In Proc. of PLDI, pages 222-233. ACM Press, 2011. Google Scholar
  22. Naoki Kobayashi, Naoshi Tabuchi, and Hiroshi Unno. Higher-order multi-parameter tree transducers and recursion schemes for program verification. In Proc. of POPL, pages 495-508. ACM Press, 2010. Google Scholar
  23. Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, and Naoki Kobayashi. Predicate abstraction and CEGAR for disproving termination of higher-order functional programs. In Proc. of CAV 2015, volume 9207 of LNCS, pages 287-303. Springer, 2015. Google Scholar
  24. M. M. Lester, R. P. Neatherway, C.-H. Luke Ong, and S. J. Ramsay. Model checking liveness properties of higher-order functional programs. In Proc. of ML Workshop, 2011. Google Scholar
  25. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In LICS 2006, pages 81-90. IEEE Computer Society Press, 2006. Google Scholar
  26. C.-H. Luke Ong and Steven Ramsay. Verifying higher-order programs with pattern-matching algebraic data types. In Proc. of POPL, pages 587-598. ACM Press, 2011. Google Scholar
  27. Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. Temporal verification of higher-order functional programs. In Proc. of POPL 2016, pages 57-68. ACM, 2016. Google Scholar
  28. Robin P. Neatherway and C.-H. Luke Ong. TravMC2: higher-order model checking for alternating parity tree automata. In Proc. of SPIN 2014, pages 129-132. ACM, 2014. Google Scholar
  29. Robin P. Neatherway, Steven James Ramsay, and C.-H. Luke Ong. A traversal-based algorithm for higher-order model checking. In Proc. of ICFP 2012, pages 353-364, 2012. Google Scholar
  30. Nir Piterman and Amir Pnueli. Faster solutions of Rabin and Streett games. In LICS 2006, pages 275-284. IEEE Computer Society Press, 2006. Google Scholar
  31. Steven Ramsay, Robin Neatherway, and C.-H. Luke Ong. An abstraction refinement approach to higher-order model checking. In Proc. of POPL, pages 61-72. ACM, 2014. Google Scholar
  32. Jakob Rehof and Torben Mogensen. Tractable constraints in finite semilattices. Science of Computer Programming, 35(2):191-221, 1999. Google Scholar
  33. Sylvain Salvati and Igor Walukiewicz. Recursive schemes, krivine machines, and collapsible pushdown automata. In Proc. of RP, volume 7550 of LNCS, pages 6-20. Springer, 2012. Google Scholar
  34. Ryosuke Sato, Hiroshi Unno, and Naoki Kobayashi. Towards a scalable software model checker for higher-order programs. In Proc. of PEPM, pages 53-62. ACM Press, 2013. Google Scholar
  35. Robert S. Streett. Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control, 54(1/2):121-141, 1982. Google Scholar
  36. Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, and Takeshi Tsukada. Streett automata model checking of higher-order recursion schemes. A longer version, available from http://www-kb.is.s.u-tokyo.ac.jp/~koba/papers/fscd17-long.pdf, 2017.
  37. Taku Terao and Naoki Kobayashi. A ZDD-based efficient higher-order model checking algorithm. In Proc. of APLAS 2014, volume 8858 of LNCS, pages 354-371. Springer, 2014. Google Scholar
  38. Takeshi Tsukada and C.-H. Luke Ong. Compositional higher-order model checking via ω-regular games over Böhm trees. In CSL-LICS 2014, pages 78:1-78:10. ACM, 2014. Google Scholar
  39. Hiroshi Unno, Naoshi Tabuchi, and Naoki Kobayashi. Verification of tree-processing programs via higher-order model checking. In Proc. of APLAS 2010, volume 6461 of LNCS, pages 312-327. Springer, 2010. Google Scholar
  40. Moshe Y. Vardi. Verification of concurrent programs: The automata-theoretic framework. Ann. Pure Appl. Logic, 51(1-2):79-98, 1991. Google Scholar
  41. Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, and Naoki Kobayashi. Automatically disproving fair termination of higher-order functional programs. In Proc. of ICFP 2016, pages 243-255. ACM, 2016. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact