Büchi Complementation (Q7361932)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Buchi_Complementation
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Büchi Complementation |
AFP entry Buchi_Complementation |
Statements
19 October 2017
0 references
Julian Brunner
0 references
Büchi Complementation (English)
0 references
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.
0 references
