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 and Jan STREJČEK

Basic information

Original name

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

Authors

BLAHOUDEK, František (203 Czech Republic), Alexandre DURET-LUTZ (250 France) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

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

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

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

Publication form

electronic version available online

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/20:00114393

Organization unit

Faculty of Informatics

ISBN

978-3-030-53290-1

ISSN

DOI

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

UT WoS

000695272500002

Keywords in English

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

Abstract

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.

Links

GA19-24397S, research and development project

Name: Automaty v rozhodovacích procedurách a verifikaci (Acronym: AUTODEV)

Investor: Czech Science Foundation

Citovat

BLAHOUDEK, František, Alexandre DURET-LUTZ and 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, p. 15-27. ISBN 978-3-030-53290-1. Available from: 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 and 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, p.~15-27. ISBN~978-3-030-53290-1. Available from: https://dx.doi.org/10.1007/978-3-030-53291-8\_{}2.

Detailed Information on Publication Record