License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2020.53
URN: urn:nbn:de:0030-drops-132941
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13294/
Go to the corresponding LIPIcs Volume Portal

Parys, Paweł

Higher-Order Nonemptiness Step by Step

pdf-format:
LIPIcs-FSTTCS-2020-53.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{parys:LIPIcs:2020:13294,
  author =	{Pawe{\l} Parys},
  title =	{{Higher-Order Nonemptiness Step by Step}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{53:1--53:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Nitin Saxena and Sunil Simon},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13294},
  URN =		{urn:nbn:de:0030-drops-132941},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.53},
  annote =	{Keywords: Higher-order grammars, Nonemptiness, Model-checking, Transformation, Order reduction}
}

Keywords: Higher-order grammars, Nonemptiness, Model-checking, Transformation, Order reduction
Collection: 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)
Issue Date: 2020
Date of publication: 04.12.2020
Supplementary Material: Coq formalisation: https://github.com/pparys/ho-transform-sbs

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI