Lazy Automata Techniques for WS1S
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F17%3APU123247" target="_blank" >RIV/00216305:26230/17:PU123247 - isvavai.cz</a>
Result on the web
<a href="https://www.fit.vut.cz/research/publication/11323/" target="_blank" >https://www.fit.vut.cz/research/publication/11323/</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-662-54577-5_24" target="_blank" >10.1007/978-3-662-54577-5_24</a>
Alternative languages
Result language
angličtina
Original language name
Lazy Automata Techniques for WS1S
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2017
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of TACAS'17
ISBN
978-3-662-54576-8
ISSN
0302-9743
e-ISSN
—
Number of pages
18
Pages from-to
407-425
Publisher name
Springer Verlag
Place of publication
Heidelberg
Event location
Uppsala
Event date
Apr 22, 2017
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000440734900024