Publication detail

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

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

Original Title

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

Type

conference paper

Language

English

Original 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.

Keywords

S1S, Büchi automata, simulation, complementation

Authors

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

Released

21. 5. 2021

Publisher

Springer Verlag

Location

Cham

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Number

12754

State

Federal Republic of Germany

Pages from

215

Pages to

222

Pages count

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