Seminator 2 Can Complement Generalized Büchi Automata via
Improved Semi-determinization

D 2020

Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization

BLAHOUDEK, František, Alexandre DURET-LUTZ a Jan STREJČEK

Základní údaje

Originální název

Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization

Autoři

BLAHOUDEK, František (203 Česká republika), Alexandre DURET-LUTZ (250 Francie) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

Cham (Switzerland), Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, od s. 15-27, 13 s. 2020

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/20:00114393

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-53290-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-53291-8_2

UT WoS

000695272500002

Klíčová slova anglicky

semi-determinization; complementation; generalized Büchi automata; Seminator

Štítky

core_A, firank_1, formela-conference, omega-automata, Seminator, 𝜔-automata

Změněno: 29. 4. 2021 08:10, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We present the second generation of the tool Seminator that transforms transition-based generalized Büchi automata (TGBAs) into equivalent semi-deterministic automata. The tool has been extended with numerous optimizations and produces considerably smaller automata than its first version. In connection with the state-of-the-art LTL to TGBAs translator Spot, Seminator 2 produces smaller (on average) semi-deterministic automata than the direct LTL to semi-deterministic automata translator ltl2ldgba of the Owl library. Further, Seminator 2 has been extended with an improved NCSB complementation procedure for semi-deterministic automata, providing a new way to complement automata that is competitive with state-of-the-art complementation tools.

Návaznosti

GA19-24397S, projekt VaV

Název: Automaty v rozhodovacích procedurách a verifikaci (Akronym: AUTODEV)

Investor: Grantová agentura ČR, Automata for Decision Procedures and Verification

Citovat

BLAHOUDEK, František, Alexandre DURET-LUTZ a Jan STREJČEK. Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization. Online. In Shuvendu K. Lahiri and Chao Wang. Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Cham (Switzerland): Springer, 2020, s. 15-27. ISBN 978-3-030-53290-1. Dostupné z: https://dx.doi.org/10.1007/978-3-030-53291-8_2.

@inproceedings{1686896,
   author = {Blahoudek, František and DuretandLutz, Alexandre and Strejček, Jan},
   address = {Cham (Switzerland)},
   booktitle = {Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II},
   doi = {http://dx.doi.org/10.1007/978-3-030-53291-8_2},
   editor = {Shuvendu K. Lahiri and Chao Wang},
   keywords = {semi-determinization; complementation; generalized Büchi automata; Seminator},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Switzerland)},
   isbn = {978-3-030-53290-1},
   pages = {15-27},
   publisher = {Springer},
   title = {Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization},
   url = {https://link.springer.com/chapter/10.1007%2F978-3-030-53291-8_2},
   year = {2020}
}

TY  - JOUR
ID  - 1686896
AU  - Blahoudek, František - Duret-Lutz, Alexandre - Strejček, Jan
PY  - 2020
TI  - Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization
PB  - Springer
CY  - Cham (Switzerland)
SN  - 9783030532901
KW  - semi-determinization
KW  - complementation
KW  - generalized Büchi automata
KW  - Seminator
UR  - https://link.springer.com/chapter/10.1007%2F978-3-030-53291-8_2
L2  - https://link.springer.com/chapter/10.1007%2F978-3-030-53291-8_2
N2  - We present the second generation of the tool Seminator that transforms transition-based generalized Büchi automata (TGBAs) into equivalent semi-deterministic automata. The tool has been extended with numerous optimizations and produces considerably smaller automata than its first version. In connection with the state-of-the-art LTL to TGBAs translator Spot, Seminator 2 produces smaller (on average) semi-deterministic automata than the direct LTL to semi-deterministic automata translator ltl2ldgba of the Owl library. Further, Seminator 2 has been extended with an improved NCSB complementation procedure for semi-deterministic automata, providing a new way to complement automata that is competitive with state-of-the-art complementation tools.
ER  -

BLAHOUDEK, František, Alexandre DURET-LUTZ a Jan STREJČEK. Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization. Online. In Shuvendu K. Lahiri and Chao Wang. \textit{Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II}. Cham (Switzerland): Springer, 2020, s.~15-27. ISBN~978-3-030-53290-1. Dostupné z: https://dx.doi.org/10.1007/978-3-030-53291-8\_{}2.

Podrobný výpis o publikaci