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.FSCD.2017.32
URN: urn:nbn:de:0030-drops-77325
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7732/
Go to the corresponding LIPIcs Volume Portal

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

Streett Automata Model Checking of Higher-Order Recursion Schemes

pdf-format:
LIPIcs-FSCD-2017-32.pdf (1 MB)

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.

BibTeX - Entry

@InProceedings{suzuki_et_al:LIPIcs:2017:7732,
  author =	{Ryota Suzuki and Koichi Fujima and Naoki Kobayashi and Takeshi Tsukada},
  title =	{{Streett Automata Model Checking of Higher-Order Recursion Schemes}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{32:1--32:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7732},
  URN =		{urn:nbn:de:0030-drops-77325},
  doi =		{10.4230/LIPIcs.FSCD.2017.32},
  annote =	{Keywords: Higher-order model checking, higher-order recursion schemes, Streett automata}
}

Keywords: Higher-order model checking, higher-order recursion schemes, Streett automata
Collection: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 30.08.2017

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