Publication detail

Lazy Automata Techniques for WS1S

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

Original Title

Lazy Automata Techniques for WS1S

Type

conference paper

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

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

Authors

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

Released

17. 1. 2017

Publisher

Springer Verlag

Location

Heidelberg

ISBN

978-3-662-54576-8

Book

Proceedings of TACAS'17

Edition

Lecture Notes in Computer Science

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Year of study

10205

Number

1

State

Federal Republic of Germany

Pages from

407

Pages to

425

Pages count

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/"
}

Documents

04-TACAS17.pdf