### Abstract

This entry provides a verified implementation of rank-based Büchi Complementation. The verification is done in three steps:

1. Definition of odd rankings and proof that an automaton rejects a word iff there exists an odd ranking for it.
2. Definition of the complement automaton and proof that it accepts exactly those words for which there is an odd ranking.
3. Verified implementation of the complement automaton using the Isabelle Collections Framework.

### License

BSD License

### Topics

- Computer science/Automata and formal languages

### Session Buchi_Complementation

- Alternate
- Graph
- Ranking
- Complementation
- Complementation_Implement
- Formula
- Complementation_Final
- Complementation_Build

### Depends on

- Transition Systems and Automata

### Auto-related entries

- Gale-Shapley Algorithm
- Factorization of Polynomials with Algebraic Coefficients
- Signature-Based Gröbner Basis Algorithms
- Weight-Balanced Trees
- Formalizing the Edmonds-Karp Algorithm

## Cite

×

Buchi_Complementation-AFP

    @article{Buchi_Complementation-AFP,
      author  = {Julian Brunner},
      title   = {Büchi Complementation},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Buchi_Complementation.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 27, 2017 : Isabelle2017