Detail publikačního výsledku

Lazy Automata Techniques for WS1S

FIEDOR, T.; HOLÍK, L.; JANKŮ, P.; LENGÁL, O.; VOJNAR, T.

Originální název

Lazy Automata Techniques for WS1S

Anglický název

Lazy Automata Techniques for WS1S

Druh

Stať ve sborníku v databázi WoS či Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

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

Klíčová slova v angličtině

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

Autoři

FIEDOR, T.; HOLÍK, L.; JANKŮ, P.; LENGÁL, O.; VOJNAR, T.

Rok RIV

2018

Vydáno

17.01.2017

Nakladatel

Springer Verlag

Místo

Heidelberg

ISBN

978-3-662-54576-8

Kniha

Proceedings of TACAS'17

Edice

Lecture Notes in Computer Science

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Svazek

10205

Číslo

1

Stát

Spolková republika Německo

Strany od

407

Strany do

425

Strany počet

18

URL

https://www.fit.vut.cz/research/publication/11323/

BibTex

@inproceedings{BUT134716,
  author="Tomáš {Fiedor} and Lukáš {Holík} and Petr {Janků} and Ondřej {Lengál} and Tomáš {Vojnar}",
  title="Lazy Automata Techniques for WS1S",
  booktitle="Proceedings of TACAS'17",
  year="2017",
  series="Lecture Notes in Computer Science",
  journal="Lecture Notes in Computer Science",
  volume="10205",
  number="1",
  pages="407--425",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-662-54577-5\{_}24",
  isbn="978-3-662-54576-8",
  issn="0302-9743",
  url="https://www.fit.vut.cz/research/publication/11323/"
}

Dokumenty

04-TACAS17