Conference paper

FIEDOR 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. 658-674. ISBN 978-3-662-46680-3. Available from: http://dx.doi.org/10.1007/978-3-662-46681-0_59
Publication language:english
Original title:Nested Antichains for WS1S
Title (cs):Zanořené protiřetězce pro WS1S
Pages:658-674
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/978-3-662-46681-0_59
ISBN:978-3-662-46680-3
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 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.
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 = {658--674},
   booktitle = {Proceedings of TACAS'15},
   series = {LNCS 9035},
   year = {2015},
   location = {Heidelberg, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-662-46680-3},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.en.iso-8859-2?id=10790}
}

Your IPv4 address: 54.158.55.5
Switch to IPv6 connection

DNSSEC [dnssec]