Seminator: A Tool for Semi-Determinization of Omega-Automata

D 2017

Seminator: A Tool for Semi-Determinization of Omega-Automata

BLAHOUDEK, František, Alexandre DURET-LUTZ, Mikuláš KLOKOČKA, Mojmír KŘETÍNSKÝ, Jan STREJČEK et. al.

Basic information

Original name

Seminator: A Tool for Semi-Determinization of Omega-Automata

Authors

BLAHOUDEK, František (203 Czech Republic, belonging to the institution), Alexandre DURET-LUTZ (250 France), Mikuláš KLOKOČKA (203 Czech Republic, belonging to the institution), Mojmír KŘETÍNSKÝ (203 Czech Republic, belonging to the institution) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

Neuveden, Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2017), p. 356-367, 12 pp. 2017

Publisher

EasyChair

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

Publication form

electronic version available online

References:

URL

RIV identification code

RIV/00216224:14330/17:00094743

Organization unit

Faculty of Informatics

ISSN

DOI

http://dx.doi.org/10.29007/k5nl

Keywords in English

semi deterministic automata; ltl to automata translation; omega automata

Abstract

V originále

We present a tool that transforms nondeterministic omega-automata to semi-deterministic omega-automata. The tool Seminator accepts transition-based generalized Büchi automata (TGBA) as an input and produces automata with two kinds of semi-determinism. The implemented procedure performs degeneralization and semi-determinization simultaneously and employs several other optimizations. We experimentally evaluate Seminator in the context of LTL to semi-deterministic automata translation.

Links

GBP202/12/G061, research and development project

Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI)

Investor: Czech Science Foundation

MUNI/A/0897/2016, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.

Investor: Masaryk University, Category A

MUNI/A/0992/2016, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

BLAHOUDEK, František, Alexandre DURET-LUTZ, Mikuláš KLOKOČKA, Mojmír KŘETÍNSKÝ and Jan STREJČEK. Seminator: A Tool for Semi-Determinization of Omega-Automata. Online. In Thomas Eiter and David Sands. Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2017). Neuveden: EasyChair, 2017, p. 356-367. ISSN 2398-7340. Available from: https://dx.doi.org/10.29007/k5nl.

@inproceedings{1380432,
   author = {Blahoudek, František and DuretandLutz, Alexandre and Klokočka, Mikuláš and Křetínský, Mojmír and Strejček, Jan},
   address = {Neuveden},
   booktitle = {Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2017)},
   doi = {http://dx.doi.org/10.29007/k5nl},
   editor = {Thomas Eiter and David Sands},
   keywords = {semi deterministic automata; ltl to automata translation; omega automata},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Neuveden},
   pages = {356-367},
   publisher = {EasyChair},
   title = {Seminator: A Tool for Semi-Determinization of Omega-Automata},
   url = {http://easychair.org/publications/paper/Seminator_A_Tool_for_Semi-Determinization_of_Omega-Automata},
   year = {2017}
}

TY  - JOUR
ID  - 1380432
AU  - Blahoudek, František - Duret-Lutz, Alexandre - Klokočka, Mikuláš - Křetínský, Mojmír - Strejček, Jan
PY  - 2017
TI  - Seminator: A Tool for Semi-Determinization of Omega-Automata
PB  - EasyChair
CY  - Neuveden
KW  - semi deterministic automata
KW  - ltl to automata translation
KW  - omega automata
UR  - http://easychair.org/publications/paper/Seminator_A_Tool_for_Semi-Determinization_of_Omega-Automata
N2  - We present a tool that transforms nondeterministic omega-automata to semi-deterministic omega-automata. The tool Seminator accepts transition-based generalized Büchi automata (TGBA) as an input and produces automata with two kinds of semi-determinism. The implemented procedure performs degeneralization and semi-determinization simultaneously and employs several other optimizations. We experimentally evaluate Seminator in the context of LTL to semi-deterministic automata translation.
ER  -

BLAHOUDEK, František, Alexandre DURET-LUTZ, Mikuláš KLOKOČKA, Mojmír KŘETÍNSKÝ and Jan STREJČEK. Seminator: A Tool for Semi-Determinization of Omega-Automata. Online. In Thomas Eiter and David Sands. \textit{Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2017)}. Neuveden: EasyChair, 2017, p.~356-367. ISSN~2398-7340. Available from: https://dx.doi.org/10.29007/k5nl.

Detailed Information on Publication Record