Přístupnostní navigace
E-application
Search Search Close
Publication detail
FIEDOR, T. HOLÍK, L. JANKŮ, P. LENGÁL, O. VOJNAR, T.
Original Title
Lazy Automata Techniques for WS1S
Type
report
Language
English
Original 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.
Keywords
WS1Sfinite automatalogicantichainslazy evaluationsubsumptionmonadic second-order logic
Authors
FIEDOR, T.; HOLÍK, L.; JANKŮ, P.; LENGÁL, O.; VOJNAR, T.
Released
1. 2. 2017
Location
arXiv:1701.06282
Pages count
17
URL
https://arxiv.org/abs/1701.06282v2
BibTex
@techreport{BUT170107, author="Tomáš {Fiedor} and Lukáš {Holík} and Petr {Janků} and Ondřej {Lengál} and Tomáš {Vojnar}", title="Lazy Automata Techniques for WS1S", year="2017", address="arXiv:1701.06282", pages="17", url="https://arxiv.org/abs/1701.06282v2" }