Publication Details

Lazy Automata Techniques for WS1S

FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej and VOJNAR Tomáš. Lazy Automata Techniques for WS1S. In: Proceedings of TACAS'17. Lecture Notes in Computer Science, vol. 10205. Heidelberg: Springer Verlag, 2017, pp. 407-425. ISBN 978-3-662-54576-8. ISSN 0302-9743.
Czech title
Líné Automatové Techniky pro WS1S
Type
conference paper
Language
english
Authors
Keywords

WS1S
finite automata
logic
antichains
lazy evaluation
subsumption
monadic second-order logic

Abstract

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 antichain-based 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.

Published
2017
Pages
407-425
Journal
Lecture Notes in Computer Science, vol. 10205, no. 1, ISSN 0302-9743
Proceedings
Proceedings of TACAS'17
Series
Lecture Notes in Computer Science
Conference
European Joint Conferences on Theory and Practice of Software, Uppsala, SE
ISBN
978-3-662-54576-8
Publisher
Springer Verlag
Place
Heidelberg, DE
DOI
UT WoS
000440734900024
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB11323,
   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 = "407--425",
   booktitle = "Proceedings of TACAS'17",
   series = "Lecture Notes in Computer Science",
   journal = "Lecture Notes in Computer Science",
   volume = 10205,
   number = 1,
   year = 2017,
   location = "Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-662-54576-8",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-662-54577-5\_24",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11323"
}
Back to top