Publication Details

Nested Antichains for WS1S

FIEDOR, T.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Nested Antichains for WS1S. In Proceedings of TACAS'15. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2015. p. 658-674. ISBN: 978-3-662-46680-3.
Czech title
Zanořené protiřetězce pro WS1S
Type
conference paper
Language
English
Authors
URL
Keywords

antichains WS1S finite automata subsumption nondeterministic automata

Abstract

We propose a novel approach for coping with alternating quantification as the main source of nonelementary complexity of deciding WS1S formulae. Our approach is applicable within the state-of-the-art automata-based WS1S decision procedure implemented, e.g., in MONA. The way in which the standard decision procedure processes quantifiers involves determinization, with its worst case exponential complexity, for every quantifier alternation in the prefix of a formula. Our algorithm avoids building the deterministic automata-instead, it constructs only those of their states needed for (dis)proving validity of the formula. It uses a symbolic representation of the states, which have a deeply nested structure stemming from the repeated implicit subset construction, and prunes the search space by a nested subsumption relation, a generalisation of the one used by the so-called antichain algorithms for handling non-deterministic automata. We have obtained encouraging experimental results, in some cases outperforming MONA by several orders of magnitude.

Published
2015
Pages
658–674
Proceedings
Proceedings of TACAS'15
Series
Lecture Notes in Computer Science
Volume
9035
ISBN
978-3-662-46680-3
Publisher
Springer Verlag
Place
Heidelberg
DOI
EID Scopus
BibTeX
@inproceedings{BUT119806,
  author="Tomáš {Fiedor} and Lukáš {Holík} and Ondřej {Lengál} and Tomáš {Vojnar}",
  title="Nested Antichains for WS1S",
  booktitle="Proceedings of TACAS'15",
  year="2015",
  series="Lecture Notes in Computer Science",
  volume="9035",
  pages="658--674",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-662-46681-0\{_}59",
  isbn="978-3-662-46680-3",
  url="http://dx.doi.org/10.1007/978-3-662-46681-0_59"
}
Back to top