Complementing Semi-Deterministic Büchi Automata

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. Our complementation is based on 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 states has less than states. Moreover, the resulting automaton is unambiguous, which again offers new applications, like the analysis of Markov chains. We also motivate and present an on-the-fly modification of our complementation, which does not need to know the whole automaton before the complementation starts, which is a crucial property for Ultimate Büchi Automizer that uses implicitly encoded automata. The price for the on-the-fly approach is a slightly worse upper bound on the size of the produced automaton for the complement: it has less than 5^n states. We have evaluated our construction against the semi-deterministic automata produced by Ultimate Büchi Automizer applied to programs of the Termination category of the software verification competition SV-COMP 2015. We complemented these automata by our algorithm and by four standard complementation constructions and compare the resulting automata. The evaluation confirms that our algorithm outperforms the known complementation techniques that work for general nondeterministic Büchi automata. The presentation is based on the identically titled paper published at TACAS 2016.

Authors

• Joint with Matthias Heizmann
• Sven Schewe University of Liverpool
• Jan Strejček
• Ming-Hsien Tsai.

Keywords

No keywords are indexed for this paper.