Document Open Access Logo

Higher-Order Nonemptiness Step by Step

Author Paweł Parys

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.53.pdf
  • Filesize: 485 kB
  • 14 pages

Document Identifiers

Author Details

Paweł Parys
  • Institute of Informatics, University of Warsaw, Poland

Funding

  • Parys, Paweł: Work supported by the National Science Centre, Poland (grant no. 2016/22/E/ST6/00041).

Cite AsGet BibTex

Paweł Parys. Higher-Order Nonemptiness Step by Step. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 53:1-53:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSTTCS.2020.53

Abstract

We show a new simple algorithm that checks whether a given higher-order grammar generates a nonempty language of trees. The algorithm amounts to a procedure that transforms a grammar of order n to a grammar of order n-1, preserving nonemptiness, and increasing the size only exponentially. After repeating the procedure n times, we obtain a grammar of order 0, whose nonemptiness can be easily checked. Since the size grows exponentially at each step, the overall complexity is n-EXPTIME, which is known to be optimal. More precisely, the transformation (and hence the whole algorithm) is linear in the size of the grammar, assuming that the arity of employed nonterminals is bounded by a constant. The same algorithm allows to check whether an infinite tree generated by a higher-order recursion scheme is accepted by an alternating safety (or reachability) automaton, because this question can be reduced to the nonemptiness problem by taking a product of the recursion scheme with the automaton. A proof of correctness of the algorithm is formalised in the proof assistant Coq. Our transformation is motivated by a similar transformation of Asada and Kobayashi (2020) changing a word grammar of order n to a tree grammar of order n-1. The step-by-step approach can be opposed to previous algorithms solving the nonemptiness problem "in one step", being compulsorily more complicated.

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
Keywords
  • Higher-order grammars
  • Nonemptiness
  • Model-checking
  • Transformation
  • Order reduction

Metrics

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

Related Versions

Supplementary Materials

References

  1. Klaus Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Log. Methods Comput. Sci., 3(3), 2007. URL: https://doi.org/10.2168/LMCS-3(3:1)2007.
  2. Kazuyuki Asada and Naoki Kobayashi. Size-preserving translations from order-(n+1) word grammars to order-n tree grammars. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 22:1-22:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.22.
  3. Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, and Olivier Serre. Recursion schemes and logical reflection. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 120-129. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/LICS.2010.40.
  4. Christopher H. Broadbent and Naoki Kobayashi. Saturation-based model checking of higher-order recursion schemes. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 129-148. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.129.
  5. Christopher H. Broadbent and C.-H. Luke Ong. On global model checking trees generated by higher-order recursion schemes. In Luca de Alfaro, editor, Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5504 of Lecture Notes in Computer Science, pages 107-121. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00596-1_9.
  6. Arnaud Carayol and Olivier Serre. Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 165-174. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/LICS.2012.73.
  7. Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz. The diagonal problem for higher-order recursion schemes is decidable. CoRR, abs/1605.00371, 2016. URL: http://arxiv.org/abs/1605.00371.
  8. Werner Damm. The IO- and OI-hierarchies. Theor. Comput. Sci., 20:95-207, 1982. URL: https://doi.org/10.1016/0304-3975(82)90009-3.
  9. Matthew Hague, Roland Meyer, Sebastian Muskalla, and Martin Zimmermann. Parity to safety in polynomial time for pushdown and collapsible pushdown systems. In Igor Potapov, Paul G. Spirakis, and James Worrell, editors, 43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018, August 27-31, 2018, Liverpool, UK, volume 117 of LIPIcs, pages 57:1-57:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.MFCS.2018.57.
  10. Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 452-461. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/LICS.2008.34.
  11. Teodor Knapik, Damian Niwiński, and Paweł Urzyczyn. Higher-order pushdown trees are easy. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 205-222. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_15.
  12. Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Zhong Shao and Benjamin C. Pierce, editors, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, pages 416-428. ACM, 2009. URL: https://doi.org/10.1145/1480881.1480933.
  13. Naoki Kobayashi. Model checking higher-order programs. J. ACM, 60(3):20:1-20:62, 2013. URL: https://doi.org/10.1145/2487241.2487246.
  14. Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 179-188. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/LICS.2009.29.
  15. Naoki Kobayashi and C.-H. Luke Ong. Complexity of model checking recursion schemes for fragments of the modal mu-calculus. Log. Methods Comput. Sci., 7(4), 2011. URL: https://doi.org/10.2168/LMCS-7(4:9)2011.
  16. Gregory M. Kobele and Sylvain Salvati. The IO and OI hierarchies revisited. Inf. Comput., 243:205-221, 2015. URL: https://doi.org/10.1016/j.ic.2014.12.015.
  17. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81-90. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.38.
  18. Paweł Parys. Recursion schemes and the WMSO+U logic. In Rolf Niedermeier and Brigitte Vallée, editors, 35th Symposium on Theoretical Aspects of Computer Science, STACS 2018, February 28 to March 3, 2018, Caen, France, volume 96 of LIPIcs, pages 53:1-53:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.53.
  19. Steven J. Ramsay, Robin P. Neatherway, and C.-H. Luke Ong. A type-directed abstraction refinement approach to higher-order model checking. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 61-72. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535873.
  20. Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. Inf. Comput., 239:340-355, 2014. URL: https://doi.org/10.1016/j.ic.2014.07.012.
  21. Sylvain Salvati and Igor Walukiewicz. A model for behavioural properties of higher-order programs. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 229-243. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CSL.2015.229.
  22. Taku Terao and Naoki Kobayashi. A ZDD-based efficient higher-order model checking algorithm. In Jacques Garrigue, editor, Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings, volume 8858 of Lecture Notes in Computer Science, pages 354-371. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-12736-1_19.
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 Imprint Privacy Contact