Conference paperFIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej and VOJNAR Tomáš. Lazy Automata Techniques for WS1S. In: Proceedings of TACAS'17. Heidelberg: Springer Verlag, 2017, pp. 407425. ISBN 9783662545768. ISSN 03029743.  Publication language:  english 

Original title:  Lazy Automata Techniques for WS1S 

Title (cs):  Líné Automatové Techniky pro WS1S 

Pages:  407425 

Proceedings:  Proceedings of TACAS'17 

Conference:  European Joint Conferences on Theory and Practice of Software 

Series:  LNCS 10205 

Place:  Heidelberg, DE 

Year:  2017 

ISBN:  9783662545768 

Journal:  Lecture Notes in Computer Science, No. 10205, DE 

ISSN:  03029743 

DOI:  10.1007/9783662545775_24 

Publisher:  Springer Verlag 

Keywords 

WS1S finite automata logic antichains lazy evaluation subsumption monadic secondorder logic 
Annotation 

We present a new decision procedure for the logic WS1S. It originates from the classical approach, which first builds an automaton accepting all models of a formula and then tests whether its language is empty. The main novelty is to test the emptiness on the fly, while constructing the automaton, and prune the constructed state space from parts irrelevant for the test. The pruning is done by a~generalization of two techniques used in antichainbased language inclusion and universality checking of finite automata: subsumption and early termination. The~richer structure of the WS1S decision problem allows us, however, to elaborate on these techniques in novel ways. Our experiments show that the proposed approach can indeed significantly outperform the classical decision procedure (implemented in the \mona~tool) as well as its recently proposed alternative based on using nondeterministic automata. 
BibTeX: 

@INPROCEEDINGS{
author = {Tom{\'{a}}{\v{s}} Fiedor and Luk{\'{a}}{\v{s}}
Hol{\'{i}}k and Petr Jank{\r{u}} and Ond{\v{r}}ej
Leng{\'{a}}l and Tom{\'{a}}{\v{s}} Vojnar},
title = {Lazy Automata Techniques for WS1S},
pages = {407425},
booktitle = {Proceedings of TACAS'17},
series = {LNCS 10205},
journal = {Lecture Notes in Computer Science},
number = {10205},
year = {2017},
location = {Heidelberg, DE},
publisher = {Springer Verlag},
ISBN = {9783662545768},
ISSN = {03029743},
doi = {10.1007/9783662545775_24},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=11323}
} 
