Büchi Complementation

Title:	Büchi Complementation
Author:	Julian Brunner
Submission date:	2017-10-19
Abstract:	This entry provides a verified implementation of rank-based Büchi Complementation. The verification is done in three steps: Definition of odd rankings and proof that an automaton rejects a word iff there exists an odd ranking for it. Definition of the complement automaton and proof that it accepts exactly those words for which there is an odd ranking. Verified implementation of the complement automaton using the Isabelle Collections Framework.
BibTeX:	@article{Buchi_Complementation-AFP, author = {Julian Brunner}, title = {Büchi Complementation}, journal = {Archive of Formal Proofs}, month = oct, year = 2017, note = {\url{http://isa-afp.org/entries/Buchi_Complementation.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Transition_Systems_and_Automata
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.