Detail publikace

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

ŠMAHLÍKOVÁ, B. HAVLENA, V. LENGÁL, O.

Originální název

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

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální 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

Autoři

ŠMAHLÍKOVÁ, B.; HAVLENA, V.; LENGÁL, O.

Vydáno

21. 5. 2021

Nakladatel

Springer Verlag

Místo

Cham

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Číslo

12754

Stát

Spolková republika Německo

Strany od

215

Strany do

222

Strany počet

8

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