License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2021.140
URN: urn:nbn:de:0030-drops-142098
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14209/
Go to the corresponding LIPIcs Volume Portal

Parys, Paweł

Higher-Order Model Checking Step by Step

pdf-format:
LIPIcs-ICALP-2021-140.pdf (0.8 MB)

Abstract

We show a new simple algorithm that solves the model-checking problem for recursion schemes: check whether the tree generated by a given higher-order recursion scheme is accepted by a given alternating parity automaton. The algorithm amounts to a procedure that transforms a recursion scheme of order n to a recursion scheme of order n-1, preserving acceptance, and increasing the size only exponentially. After repeating the procedure n times, we obtain a recursion scheme of order 0, for which the problem boils down to solving a finite parity game. Since the size grows exponentially at each step, the overall complexity is n-EXPTIME, which is known to be optimal. More precisely, the transformation is linear in the size of the recursion scheme, assuming that the arity of employed nonterminals and the size of the automaton are bounded by a constant; this results in an FPT algorithm for the model-checking problem.
Our transformation is a generalization of a previous transformation of the author (2020), working for reachability automata in place of parity automata. The step-by-step approach can be opposed to previous algorithms solving the considered problem "in one step", being compulsorily more complicated.

BibTeX - Entry

@InProceedings{parys:LIPIcs.ICALP.2021.140,
  author =	{Parys, Pawe{\l}},
  title =	{{Higher-Order Model Checking Step by Step}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{140:1--140:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14209},
  URN =		{urn:nbn:de:0030-drops-142098},
  doi =		{10.4230/LIPIcs.ICALP.2021.140},
  annote =	{Keywords: Higher-order recursion schemes, Parity automata, Model-checking, Transformation, Order reduction}
}

Keywords: Higher-order recursion schemes, Parity automata, Model-checking, Transformation, Order reduction
Collection: 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)
Issue Date: 2021
Date of publication: 02.07.2021

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