Complementing Semi-deterministic Büchi Automata

D 2016

Complementing Semi-deterministic Büchi Automata

BLAHOUDEK, František, Matthias HEIZMANN, Sven SCHEWE, Jan STREJČEK, Ming-Hsien TSAI et. al.

Základní údaje

Originální název

Complementing Semi-deterministic Büchi Automata

Autoři

BLAHOUDEK, František (203 Česká republika, domácí), Matthias HEIZMANN (276 Německo), Sven SCHEWE (276 Německo), Jan STREJČEK (203 Česká republika, garant, domácí) a Ming-Hsien TSAI (158 Tchaj-wan)

Vydání

Berlin, Tools and Algorithms for the Construction and Analysis of Systems 22nd International Conference, TACAS 2016, od s. 770-787, 18 s. 2016

Nakladatel

Springer Berlin Heidelberg

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00088081

Organizační jednotka

Fakulta informatiky

ISBN

978-3-662-49673-2

ISSN

DOI

http://dx.doi.org/10.1007/978-3-662-49674-9_49

UT WoS

000406428000049

Klíčová slova anglicky

Buchi automata;complementation

Štítky

core_A, firank_A, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 5. 2020 23:01, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We introduce an efficient complementation technique for semi-deterministic Büchi automata, which are Büchi automata that are deterministic in the limit: from every accepting state onward, their behaviour is deterministic. It is interesting to study semi-deterministic automata, because they play a role in practical applications of automata theory, such as the analysis of Markov decision processes. Our motivation to study their complementation comes from the termination analysis implemented in Ultimate Büchi Automizer, where these automata represent checked runs and have to be complemented to identify runs to be checked. We show that semi-determinism leads to a simpler complementation procedure: an extended breakpoint construction that allows for symbolic implementation. It also leads to significantly improved bounds as the complement of a semi-deterministic automaton with n states has less than 4^n states. Moreover, the resulting automaton is unambiguous, which again offers new applications, like the analysis of Markov chains. We have evaluated our construction against the semi-deterministic automata produced by the Ultimate Büchi Automizer. The evaluation confirms that our algorithm outperforms the known complementation techniques for general nondeterministic Büchi automata.

Návaznosti

GBP202/12/G061, projekt VaV

Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

MUNI/A/0935/2015, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/0945/2015, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

BLAHOUDEK, František, Matthias HEIZMANN, Sven SCHEWE, Jan STREJČEK a Ming-Hsien TSAI. Complementing Semi-deterministic Büchi Automata. In Marsha Chechik, Jean-François Raskin. Tools and Algorithms for the Construction and Analysis of Systems 22nd International Conference, TACAS 2016. Berlin: Springer Berlin Heidelberg, 2016, s. 770-787. ISBN 978-3-662-49673-2. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49674-9_49.

@inproceedings{1351787,
   author = {Blahoudek, František and Heizmann, Matthias and Schewe, Sven and Strejček, Jan and Tsai, MingandHsien},
   address = {Berlin},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems 22nd International Conference, TACAS 2016},
   doi = {http://dx.doi.org/10.1007/978-3-662-49674-9_49},
   editor = {Marsha Chechik, Jean-François Raskin},
   keywords = {Buchi automata;complementation},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Berlin},
   isbn = {978-3-662-49673-2},
   pages = {770-787},
   publisher = {Springer Berlin Heidelberg},
   title = {Complementing Semi-deterministic Büchi Automata},
   url = {http://link.springer.com/chapter/10.1007/978-3-662-49674-9_49},
   year = {2016}
}

TY  - JOUR
ID  - 1351787
AU  - Blahoudek, František - Heizmann, Matthias - Schewe, Sven - Strejček, Jan - Tsai, Ming-Hsien
PY  - 2016
TI  - Complementing Semi-deterministic Büchi Automata
PB  - Springer Berlin Heidelberg
CY  - Berlin
SN  - 9783662496732
KW  - Buchi automata;complementation
UR  - http://link.springer.com/chapter/10.1007/978-3-662-49674-9_49
L2  - http://link.springer.com/chapter/10.1007/978-3-662-49674-9_49
N2  - We introduce an efficient complementation technique for semi-deterministic Büchi automata, which are Büchi automata that are deterministic in the limit: from every accepting state onward, their behaviour is deterministic. It is interesting to study semi-deterministic automata, because they play a role in practical applications of automata theory, such as the analysis of Markov decision processes. Our motivation to study their complementation comes from the termination analysis implemented in Ultimate Büchi Automizer, where these automata represent checked runs and have to be complemented to identify runs to be checked. We show that semi-determinism leads to a simpler complementation procedure: an extended breakpoint construction that allows for symbolic implementation. It also leads to significantly improved bounds as the complement of a semi-deterministic automaton with n states has less than 4^n states. Moreover, the resulting automaton is unambiguous, which again offers new applications, like the analysis of Markov chains. We have evaluated our construction against the semi-deterministic automata produced by the Ultimate Büchi Automizer. The evaluation confirms that our algorithm outperforms the known complementation techniques for general nondeterministic Büchi automata.
ER  -

BLAHOUDEK, František, Matthias HEIZMANN, Sven SCHEWE, Jan STREJČEK a Ming-Hsien TSAI. Complementing Semi-deterministic Büchi Automata. In Marsha Chechik, Jean-Fran\c cois Raskin. \textit{Tools and Algorithms for the Construction and Analysis of Systems 22nd International Conference, TACAS 2016}. Berlin: Springer Berlin Heidelberg, 2016, s.~770-787. ISBN~978-3-662-49673-2. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49674-9\_{}49.

Podrobný výpis o publikaci