Parity automata

4 fully proved

Parity

StructureNondeterministic parity automaton#✓fully proved

A nondeterministic parity automaton with states in \(Q\) and symbols in \(\Sigma\) is a nondeterministic automaton (a transition relation labelled by symbols on \(Q\), together with a set of start states) with a priority \(p(q) \in \mathbb{N}\) assigned to each state \(q \in Q\).

structure Parity (State Symbol : Type*) extends NA State Symbol where
  /-- The priority of each state. -/
  priority : State → ℕ

Used by 9

Used byBüchi-to-parity conversion preserves the language · Every state sequence of a finite parity automaton has a parity winner · Büchi automata as parity automata · Parity-to-Muller conversion preserves the language · Parity-to-Rabin conversion preserves the language · Parity-to-Streett conversion preserves the language · Muller presentation of a parity automaton · Rabin presentation of a parity automaton · Streett presentation of a parity automaton

TheoremEvery state sequence of a finite parity automaton has a parity winner#✓fully proved

Let \(\mathcal{A}\) be a nondeterministic parity automaton with finitely many states and priority function \(p\). For every infinite sequence of states \(s_0, s_1, s_2, \dots\), the priority sequence \(p(s_0), p(s_1), p(s_2), \dots\) satisfies the even or the odd max-parity condition: the largest priority occurring infinitely often exists and is even, or it exists and is odd.

theorem run_parityEven_or_parityOdd [Finite State] (a : Parity State Symbol)
    (ss : ωSequence State) : ParityEven (ss.map a.priority) ∨ ParityOdd (ss.map a.priority)

Uses 5

Statement usesNondeterministic parity automaton · Even max-parity condition · Odd max-parity condition

Proof usesLargest infinitely occurring value · Bounded sequences have a largest infinitely occurring value

Buchi

DefinitionBüchi automata as parity automata#✓fully proved

A nondeterministic Büchi automaton is turned into the nondeterministic parity automaton with the same states, transitions and start states, in which every accepting state has priority \(2\) and every other state has priority \(1\).

def toParity (na : Buchi State Symbol) [DecidablePred (· ∈ na.accept)] : Parity State Symbol where
  toNA := na.toNA
  priority s := if s ∈ na.accept then 2 else 1

Uses 1 · Used by 1

Statement usesNondeterministic parity automaton

Used byBüchi-to-parity conversion preserves the language

TheoremBüchi-to-parity conversion preserves the language#✓fully proved

Every nondeterministic Büchi automaton accepts the same language of infinite words as its presentation as a parity automaton (priority \(2\) on accepting states, \(1\) elsewhere).

theorem language_toParity (na : Buchi State Symbol) [DecidablePred (· ∈ na.accept)] :
    language na.toParity = language na

Uses 4

Statement usesBüchi automata as parity automata · Nondeterministic parity automaton · Even max-parity condition

Proof usesMax-parity with priorities 1 and 2 is the Büchi condition

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.