Safety-liveness decomposition

We prove that every linear-time property decomposes as the intersection of a safety property and a liveness property, following Alpern and Schneider.

@[reducible, inline]

abbrev SafetyLivenessDecomposition.InfWord (T : Sort u_1) : Sort u_1

An infinite word over the alphabet T, modelled as a function from positions to letters.

Equations

• SafetyLivenessDecomposition.InfWord T = (ℕ → T)

@[reducible, inline]

abbrev SafetyLivenessDecomposition.FinWord (T : Type u_1) : Type u_1

A finite word over the alphabet T, modelled as a list of letters.

Equations

• SafetyLivenessDecomposition.FinWord T = List T

def SafetyLivenessDecomposition.FinWord.append {T : Type u_1} (a : FinWord T) (b : InfWord T) : InfWord T

Concatenate a finite word a in front of an infinite word b.

Equations

• a.append b i = if x : i < List.length a then a[i] else b (i - List.length a)

def SafetyLivenessDecomposition.InfWord.slice {T : Type u_1} (w : InfWord T) (k : ℕ) : FinWord T

The length-k prefix of an infinite word w, as a finite word.

Equations

• w.slice k = List.ofFn fun (i : Fin k) => w ↑i

@[reducible, inline]

abbrev SafetyLivenessDecomposition.Property (T : Type u_1) : Type u_1

A linear-time property: a set of infinite words.

Equations

• SafetyLivenessDecomposition.Property T = Set (SafetyLivenessDecomposition.InfWord T)

def SafetyLivenessDecomposition.SafetyProp {T : Type u_1} (P : Property T) : Prop

A property is a safety property when every word outside it has a finite bad prefix: no extension of that prefix lies in the property.

Equations

• SafetyLivenessDecomposition.SafetyProp P = ∀ (σ : SafetyLivenessDecomposition.InfWord T), ¬σ ∈ P → ∃ (i : ℕ), ∀ (β : SafetyLivenessDecomposition.InfWord T), ¬(σ.slice i).append β ∈ P

def SafetyLivenessDecomposition.LivenessProp {T : Type u_1} (P : Property T) : Prop

A property is a liveness property when every finite word can be extended to an infinite word lying in the property.

Equations

• SafetyLivenessDecomposition.LivenessProp P = ∀ (α : SafetyLivenessDecomposition.FinWord T), ∃ (β : SafetyLivenessDecomposition.InfWord T), α.append β ∈ P

@[simp]

theorem SafetyLivenessDecomposition.slice_length {T : Type u} (σ : InfWord T) (n : ℕ) : List.length (σ.slice n) = n

@[simp]

theorem SafetyLivenessDecomposition.slice_get {T : Type u} (σ : InfWord T) (n k : ℕ) (hk : k < List.length (σ.slice n)) : (σ.slice n)[k] = σ k

theorem SafetyLivenessDecomposition.slice_append {T : Type u} (α : FinWord T) (β : InfWord T) : (α.append β).slice (List.length α) = α

theorem SafetyLivenessDecomposition.append_slice_eq_self {T : Type u} (σ : InfWord T) (n : ℕ) : ((σ.slice n).append fun (k : ℕ) => σ (k + n)) = σ

theorem SafetyLivenessDecomposition.safety_liveness_decomposition {T : Type u_1} [t_nonempty : Nonempty T] (P : Property T) : ∃ (A : Property T), ∃ (B : Property T), SafetyProp A ∧ LivenessProp B ∧ A ∩ B = P