Lazy Automata Techniques for WS1S

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Lazy Automata Techniques for WS1S

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Lazy Automata Techniques for WS1S

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of TACAS'17

ISBN

978-3-662-54576-8

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

18

Strana od-do

407-425

Název nakladatele

Springer Verlag

Místo vydání

Heidelberg

Místo konání akce

Uppsala

Datum konání akce

22. 4. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000440734900024