Publication Details
Nested Antichains for WS1S
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
antichains WS1S finite automata subsumption
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 generalization of the one used
by the so-called antichain algorithms for handling nondeterministic automata. We
have obtained encouraging experimental results, in some cases outperforming Mona,
and some of the other recently proposed approaches, by several orders of
magnitude.
@article{BUT161577,
author="Tomáš {Fiedor} and Lukáš {Holík} and Ondřej {Lengál} and Tomáš {Vojnar}",
title="Nested Antichains for WS1S",
journal="Acta Informatica",
year="2019",
volume="56",
number="3",
pages="205--228",
doi="10.1007/s00236-018-0331-z",
issn="0001-5903",
url="https://www.fit.vut.cz/research/publication/11889/"
}