Complementing Semi-deterministic Büchi Automata

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00088081" target="_blank" >RIV/00216224:14330/16:00088081 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007/978-3-662-49674-9_49" target="_blank" >http://link.springer.com/chapter/10.1007/978-3-662-49674-9_49</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-662-49674-9_49" target="_blank" >10.1007/978-3-662-49674-9_49</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Complementing Semi-deterministic Büchi Automata

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Complementing Semi-deterministic Büchi Automata

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Tools and Algorithms for the Construction and Analysis of Systems 22nd International Conference, TACAS 2016

ISBN

9783662496732

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

18

Strana od-do

770-787

Název nakladatele

Springer Berlin Heidelberg

Místo vydání

Berlin

Místo konání akce

Eindhoven

Datum konání akce

2. 4. 2016

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—