Publication Details

Deciding S1S: Down the Rabbit Hole and Through the Looking Glass

HAVLENA Vojtěch, LENGÁL Ondřej and ŠMAHLÍKOVÁ Barbora. Deciding S1S: Down the Rabbit Hole and Through the Looking Glass. In: Proceedings of NETYS'21. Lecture notes in Computer Science. Cham: Springer Verlag, 2021, pp. 215-222. ISSN 0302-9743.
Czech title
Rozhodování S1S: Do zaječí díry a skrz zrcadlo
Type
conference paper
Language
english
Authors
Havlena Vojtěch, Ing., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Šmahlíková Barbora, Ing. (FIT BUT)
Keywords

S1S, Büchi automata, simulation, complementation

Abstract

Monadic second-order logic of one successor (S1S) is a logic for specifying omega-regular languages in a concise way. In this paper, we revisit the classical decision procedure based on translating S1S formulae into Büchi automata and employ state-of-the-art algorithms for their manipulation, in particular complementation and size reduction. We compare our implementation to the one based on loop-deterministic finite automata and observe cases where the classical approach scales better.

Published
2021
Pages
215-222
Journal
Lecture Notes in Computer Science, no. 12754, ISSN 0302-9743
Proceedings
Proceedings of NETYS'21
Series
Lecture notes in Computer Science
Conference
International Conference on Networked Systems 2021, Virtual Conference, DE
Publisher
Springer Verlag
Place
Cham, DE
DOI
10.1007/978-3-030-91014-3_15
UT WoS
000891773700015
EID Scopus
2-s2.0-85121868746
BibTeX 
@INPROCEEDINGS{FITPUB12508,
   author = "Vojt\v{e}ch Havlena and Ond\v{r}ej Leng\'{a}l and Barbora \v{S}mahl\'{i}kov\'{a}",
   title = "Deciding S1S: Down the Rabbit Hole and Through the Looking Glass",
   pages = "215--222",
   booktitle = "Proceedings of NETYS'21",
   series = "Lecture notes in Computer Science",
   journal = "Lecture Notes in Computer Science",
   number = 12754,
   year = 2021,
   location = "Cham, DE",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-030-91014-3\_15",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12508"
}
Back to top