Detail výsledku

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

ŠMAHLÍKOVÁ, B.; HAVLENA, V.; LENGÁL, O. Deciding S1S: Down the Rabbit Hole and Through the Looking Glass. In Proceedings of NETYS'21. Lecture Notes in Computer Science. Lecture notes in Computer Science. Cham: Springer Verlag, 2021. no. 12754, p. 215-222. ISSN: 0302-9743.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Šmahlíková Barbora, Ing.
Havlena Vojtěch, Ing., Ph.D., UIFS (FIT), UITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., UITS (FIT)
Abstrakt

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.

Klíčová slova

S1S, Büchi automata, simulation, complementation

Rok
2021
Strany
215–222
Časopis
Lecture Notes in Computer Science, č. 12754, ISSN 0302-9743
Sborník
Proceedings of NETYS'21
Řada
Lecture notes in Computer Science
Konference
International Conference on Networked Systems 2021
Vydavatel
Springer Verlag
Místo
Cham
DOI
10.1007/978-3-030-91014-3_15
UT WoS
000891773700015
EID Scopus
2-s2.0-85121868746
BibTeX 
@inproceedings{BUT175785,
  author="Barbora {Šmahlíková} and Vojtěch {Havlena} and Ondřej {Lengál}",
  title="Deciding S1S: Down the Rabbit Hole and Through the Looking Glass",
  booktitle="Proceedings of NETYS'21",
  year="2021",
  series="Lecture notes in Computer Science",
  journal="Lecture Notes in Computer Science",
  number="12754",
  pages="215--222",
  publisher="Springer Verlag",
  address="Cham",
  doi="10.1007/978-3-030-91014-3\{_}15",
  issn="0302-9743"
}
Projekty
Automaty v rozhodovacích procedurách a verifikaci, GAČR, Standardní projekty, GA19-24397S, GA19-24397S, zahájení: 2019-01-01, ukončení: 2021-12-31, řešení
Spolehlivé, bezpečné a efektivní počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-20-6427, zahájení: 2020-03-01, ukončení: 2023-02-28, ukončen
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru