Other formats:
BibTeX
LaTeX
RIS
@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 and 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, p.~770-787. ISBN~978-3-662-49673-2. Available from: https://dx.doi.org/10.1007/978-3-662-49674-9\_{}49.
|