Skip to content

Rabin and Streett automata

16 fully proved

Rabin

StructureRabin automaton#✓fully proved

A Rabin automaton is a nondeterministic automaton together with a set of Rabin pairs \((E, F)\), each a pair of sets of states. A run is accepting when some pair is hit: the run visits \(E\) infinitely often and \(F\) only finitely often.

structure Rabin (State Symbol : Type*) extends NA State Symbol where
  /-- The Rabin pairs. -/
  accept : Set (Set State × Set State)
Used by 8
Used byRun-wise Rabin/Streett duality · Rabin-to-Muller conversion preserves the language · Parity-to-Muller conversion preserves the language · Parity-to-Rabin conversion preserves the language · Membership in the language of a Rabin automaton · Muller presentation of a Rabin automaton · Rabin presentation of a parity automaton · Streett automaton with the pairs of a Rabin automaton

TheoremMembership in the language of a Rabin automaton#✓fully proved

An infinite word \(x\) is accepted by a Rabin automaton \(r\) if and only if there is a run \(s\) of \(r\) on \(x\) and a Rabin pair \((E, F)\) of \(r\) such that \(s\) visits \(E\) infinitely often and visits \(F\) only finitely often.

theorem mem_language_iff {r : Rabin State Symbol} {xs : ωSequence Symbol} :
    xs ∈ language r ↔
      ∃ ss, r.Run xs ss ∧ ∃ p ∈ r.accept, (∃ᶠ k in atTop, ss k ∈ p.1) ∧
        (∀ᶠ k in atTop, ss k ∉ p.2)
Uses 1 · Used by 2
Statement usesRabin automaton
Used byRabin-to-Muller conversion preserves the language · Parity-to-Rabin conversion preserves the language

DefinitionMuller presentation of a Rabin automaton#✓fully proved

Given a Rabin automaton with set of Rabin pairs \(\mathcal{R}\), this is the Muller automaton with the same states, initial states and transitions whose accepting family consists of the sets \(S\) of states for which some pair \((E, F) \in \mathcal{R}\) satisfies \(S \cap E \neq \emptyset\) and \(S \cap F = \emptyset\). A Muller automaton accepts a run when the set of states that the run visits infinitely often belongs to its accepting family.

def toMuller (r : Rabin State Symbol) : Muller State Symbol where
  toNA := r.toNA
  accept := {S | ∃ p ∈ r.accept, (S ∩ p.1).Nonempty ∧ Disjoint S p.2}
Uses 1 · Used by 3
Statement usesRabin automaton
Used byRabin-to-Muller conversion preserves the language · Parity-to-Muller conversion preserves the language · Muller presentation of a parity automaton

TheoremRabin-to-Muller conversion preserves the language#✓fully proved

If the state space is finite, then a Rabin automaton \(r\) accepts the same language as its Muller presentation: the Muller automaton with the same transitions and initial states as \(r\) whose acceptance sets are the sets \(S\) of states such that, for some Rabin pair \((E, F)\) of \(r\), \(S\) meets \(E\) and is disjoint from \(F\).

theorem language_toMuller [Finite State] (r : Rabin State Symbol) :
    language r.toMuller = language r
Uses 3 · Used by 1
Statement usesRabin automaton · Muller presentation of a Rabin automaton
Proof usesMembership in the language of a Rabin automaton
Used byParity-to-Muller conversion preserves the language

Streett

StructureStreett automaton#✓fully proved

A Streett automaton is a nondeterministic automaton together with a set of Streett pairs \((E, F)\), each a pair of sets of states. A run is accepting when every pair is respected: if the run visits \(E\) infinitely often then it also visits \(F\) infinitely often.

structure Streett (State Symbol : Type*) extends NA State Symbol where
  /-- The Streett pairs. -/
  accept : Set (Set State × Set State)
Used by 7
Used byRun-wise Rabin/Streett duality · Streett-to-Muller conversion preserves the language · Parity-to-Streett conversion preserves the language · Membership in the language of a Streett automaton · Muller presentation of a Streett automaton · Streett presentation of a parity automaton · Streett automaton with the pairs of a Rabin automaton

TheoremMembership in the language of a Streett automaton#✓fully proved

An infinite word \(x\) is accepted by a Streett automaton \(r\) if and only if there is a run \(s\) of \(r\) on \(x\) such that for every Streett pair \((E, F)\) of \(r\), if \(s\) visits \(E\) infinitely often then \(s\) visits \(F\) infinitely often.

theorem mem_language_iff {r : Streett State Symbol} {xs : ωSequence Symbol} :
    xs ∈ language r ↔
      ∃ ss, r.Run xs ss ∧
        ∀ p ∈ r.accept, (∃ᶠ k in atTop, ss k ∈ p.1) → (∃ᶠ k in atTop, ss k ∈ p.2)
Uses 1 · Used by 2
Statement usesStreett automaton
Used byStreett-to-Muller conversion preserves the language · Parity-to-Streett conversion preserves the language

DefinitionMuller presentation of a Streett automaton#✓fully proved

Given a Streett automaton with set of Streett pairs \(\mathcal{P}\), this is the Muller automaton with the same states, initial states and transitions whose accepting family consists of the sets \(S\) of states such that every pair \((E, F) \in \mathcal{P}\) with \(S \cap E \neq \emptyset\) also satisfies \(S \cap F \neq \emptyset\). A Muller automaton accepts a run when the set of states that the run visits infinitely often belongs to its accepting family.

def toMuller (r : Streett State Symbol) : Muller State Symbol where
  toNA := r.toNA
  accept := {S | ∀ p ∈ r.accept, (S ∩ p.1).Nonempty → (S ∩ p.2).Nonempty}
Uses 1 · Used by 1
Statement usesStreett automaton
Used byStreett-to-Muller conversion preserves the language

TheoremStreett-to-Muller conversion preserves the language#✓fully proved

If the state space is finite, then a Streett automaton \(r\) accepts the same language as its Muller presentation: the Muller automaton with the same transitions and initial states as \(r\) whose acceptance sets are the sets \(S\) of states such that, for every Streett pair \((E, F)\) of \(r\), if \(S\) meets \(E\) then \(S\) meets \(F\).

theorem language_toMuller [Finite State] (r : Streett State Symbol) :
    language r.toMuller = language r
Uses 3
Statement usesStreett automaton · Muller presentation of a Streett automaton
Proof usesMembership in the language of a Streett automaton

Parity

DefinitionRabin presentation of a parity automaton#✓fully proved

Given a parity automaton with priority function \(\Omega\) from states to natural numbers, this is the Rabin automaton with the same states, initial states and transitions whose Rabin pairs are the pairs \((E_i, F_i)\) for \(i \in \mathbb{N}\), where \(E_i = \{s : \Omega(s) = 2i\}\) and \(F_i = \{s : \Omega(s) > 2i\}\).

def toRabin (a : Parity State Symbol) : Rabin State Symbol where
  toNA := a.toNA
  accept := {p | ∃ i, p = ({s | a.priority s = 2 * i}, {s | a.priority s > 2 * i})}
Uses 2 · Used by 3
Statement usesNondeterministic parity automaton · Rabin automaton
Used byParity-to-Muller conversion preserves the language · Parity-to-Rabin conversion preserves the language · Muller presentation of a parity automaton

TheoremParity-to-Rabin conversion preserves the language#✓fully proved

If the state space is finite, then a parity automaton \(a\) accepts the same language as its Rabin presentation: the Rabin automaton with the same transitions and initial states as \(a\) whose Rabin pairs are the pairs \((E_i, F_i)\) for \(i \in \mathbb{N}\), where \(E_i\) is the set of states of priority \(2i\) and \(F_i\) the set of states of priority greater than \(2i\).

theorem language_toRabin [Finite State] (a : Parity State Symbol) :
    language a.toRabin = language a
Uses 7 · Used by 1
Statement usesNondeterministic parity automaton · Rabin presentation of a parity automaton · Rabin automaton · Even max-parity condition
Proof usesMembership in the language of a Rabin automaton · Largest infinitely occurring value · The tail of a bounded sequence is bounded by its largest infinitely occurring value
Used byParity-to-Muller conversion preserves the language

DefinitionStreett presentation of a parity automaton#✓fully proved

Given a parity automaton with priority function \(\Omega\) from states to natural numbers, this is the Streett automaton with the same states, initial states and transitions whose Streett pairs are the pairs \((E_i, F_i)\) for \(i \in \mathbb{N}\), where \(E_i = \{s : \Omega(s) = 2i + 1\}\) and \(F_i = \{s : \Omega(s) > 2i + 1\}\).

def toStreett (a : Parity State Symbol) : Streett State Symbol where
  toNA := a.toNA
  accept := {p | ∃ i, p = ({s | a.priority s = 2 * i + 1},
    {s | a.priority s > 2 * i + 1})}
Uses 2 · Used by 1
Statement usesNondeterministic parity automaton · Streett automaton
Used byParity-to-Streett conversion preserves the language

TheoremParity-to-Streett conversion preserves the language#✓fully proved

If the state space is finite, then a parity automaton \(a\) accepts the same language as its Streett presentation: the Streett automaton with the same transitions and initial states as \(a\) whose Streett pairs are the pairs \((E_i, F_i)\) for \(i \in \mathbb{N}\), where \(E_i\) is the set of states of priority \(2i + 1\) and \(F_i\) the set of states of priority greater than \(2i + 1\).

theorem language_toStreett [Finite State] (a : Parity State Symbol) :
    language a.toStreett = language a
Uses 7
Statement usesNondeterministic parity automaton · Streett presentation of a parity automaton · Streett automaton · Even max-parity condition
Proof usesMembership in the language of a Streett automaton · Largest infinitely occurring value · Bounded sequences have a largest infinitely occurring value

DefinitionMuller presentation of a parity automaton#✓fully proved

The Muller automaton of a parity automaton is the Muller presentation of its Rabin presentation. It has the same states, initial states and transitions, and its accepting family consists of the sets \(S\) of states for which there is a natural number \(i\) such that \(S\) contains a state of priority \(2i\) and no state of priority greater than \(2i\). A Muller automaton accepts a run when the set of states that the run visits infinitely often belongs to its accepting family.

def toMuller (a : Parity State Symbol) : Muller State Symbol :=
  a.toRabin.toMuller
Uses 3 · Used by 1
Statement usesNondeterministic parity automaton · Rabin presentation of a parity automaton · Muller presentation of a Rabin automaton
Used byParity-to-Muller conversion preserves the language

TheoremParity-to-Muller conversion preserves the language#✓fully proved

If the state space is finite, then a parity automaton accepts the same language as its Muller presentation, the Muller automaton obtained by converting it to its Rabin presentation and that to a Muller automaton.

theorem language_toMuller [Finite State] (a : Parity State Symbol) :
    language a.toMuller = language a
Uses 8
Statement usesNondeterministic parity automaton · Muller presentation of a parity automaton · Even max-parity condition
Proof usesParity-to-Rabin conversion preserves the language · Rabin presentation of a parity automaton · Rabin automaton · Rabin-to-Muller conversion preserves the language · Muller presentation of a Rabin automaton

Rabin

DefinitionStreett automaton with the pairs of a Rabin automaton#✓fully proved

Given a Rabin automaton, this is the Streett automaton with the same states, initial states and transitions and the same set of pairs.

For a fixed run and a pair \((E, F)\), the Streett condition (if the run visits \(E\) infinitely often, then it visits \(F\) infinitely often) is the negation of the Rabin condition (the run visits \(E\) infinitely often and \(F\) only finitely often).

def toStreett (r : Rabin State Symbol) : Streett State Symbol where
  toNA := r.toNA
  accept := r.accept
Uses 2 · Used by 1
Statement usesRabin automaton · Streett automaton
Used byRun-wise Rabin/Streett duality

TheoremRun-wise Rabin/Streett duality#✓fully proved

Let \(r\) be a Rabin automaton and let \(s\) be an infinite sequence of states. Then \(s\) satisfies the Rabin condition of \(r\), that is, for some Rabin pair \((E, F)\) of \(r\) the sequence \(s\) visits \(E\) infinitely often and \(F\) only finitely often, if and only if \(s\) fails the Streett condition with the same pairs, that is, it is not the case that for every Rabin pair \((E, F)\) of \(r\), if \(s\) visits \(E\) infinitely often then \(s\) visits \(F\) infinitely often.

The sequence \(s\) need not be a run of \(r\). (For languages of nondeterministic automata there is no such complementation statement, since complementation also swaps the run quantifier.)

theorem acceptsRun_iff_not_streett {r : Rabin State Symbol} {ss : ωSequence State} :
    (∃ p ∈ r.accept, (∃ᶠ k in atTop, ss k ∈ p.1) ∧ (∀ᶠ k in atTop, ss k ∉ p.2)) ↔
      ¬ (∀ p ∈ r.toStreett.accept, (∃ᶠ k in atTop, ss k ∈ p.1) →
        (∃ᶠ k in atTop, ss k ∈ p.2))
Uses 3
Statement usesRabin automaton · Streett automaton with the pairs of a Rabin automaton · Streett automaton

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.