Conference paperFIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Nested Antichains for WS1S. In: Proceedings of TACAS'15. Heidelberg: Springer Verlag, 2015, pp. 658674. ISBN 9783662466803. Available from: http://dx.doi.org/10.1007/9783662466810_59  Publication language:  english 

Original title:  Nested Antichains for WS1S 

Title (cs):  Zanořené protiřetězce pro WS1S 

Pages:  658674 

Proceedings:  Proceedings of TACAS'15 

Conference:  European Joint Conferences on Theory and Practice of Software  ETAPS'15 (TACAS'15) 

Series:  LNCS 9035 

Place:  Heidelberg, DE 

Year:  2015 

URL:  http://dx.doi.org/10.1007/9783662466810_59 

ISBN:  9783662466803 

Publisher:  Springer Verlag 

Keywords 

antichains WS1S finite automata subsumption nondeterministic automata 
Annotation 

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 stateoftheart
automatabased 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 automatainstead, 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 socalled antichain
algorithms for handling nondeterministic automata. We have obtained
encouraging experimental results, in some cases outperforming MONA by
several orders of magnitude. 
BibTeX: 

@INPROCEEDINGS{
author = {Tom{\'{a}}{\v{s}} Fiedor and Luk{\'{a}}{\v{s}} Hol{\'{i}}k
and Ond{\v{r}}ej Leng{\'{a}}l and Tom{\'{a}}{\v{s}} Vojnar},
title = {Nested Antichains for WS1S},
pages = {658674},
booktitle = {Proceedings of TACAS'15},
series = {LNCS 9035},
year = {2015},
location = {Heidelberg, DE},
publisher = {Springer Verlag},
ISBN = {9783662466803},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=10790}
} 
