Safety and Liveness properties of ω-sequences

This file formalizes the main results of [AlpernSchneider1985]. Namely, given an appropriate topology on ω-sequences:

• Safety properties can be identified with closed sets.
• Liveness properties can be identified with dense sets.
• Every property is the intersection of a safety property and a liveness property.

References

• [Alpern, Bowen; Schneider, Fred B. (1985). "Defining liveness". Information Processing Letters. 21 (4): 181–185.][AlpernSchneider1985]

@[reducible, inline]

abbrev Cslib.ωLanguage.IsSafety {α : Type u_1} (p : ωLanguage α) : Prop

Safety properties are identified with closed sets.

Equations

• p.IsSafety = IsClosed p.toSet

theorem Cslib.ωLanguage.isSafety_iff {α : Type u_1} (p : ωLanguage α) : p.IsSafety ↔ ∀ xs ∉ p, ∃ (n : ℕ), ∀ (ys : ωSequence α), ωSequence.take n xs ++ω ys ∉ p

An alternative characterization of IsSafety that justifies its definition: if an ω-sequence violates a safety property, then it has a finite prefix all of whose infinite extensions also violate the property.

@[reducible, inline]

abbrev Cslib.ωLanguage.IsLiveness {α : Type u_1} (p : ωLanguage α) : Prop

Liveness properties are identified with dense sets.

Equations

• p.IsLiveness = Dense p.toSet

theorem Cslib.ωLanguage.isLiveness_iff {α : Type u_1} (p : ωLanguage α) : p.IsLiveness ↔ ∀ (xs : ωSequence α) (n : ℕ), ∃ (ys : ωSequence α), ωSequence.take n xs ++ω ys ∈ p

An alternative characterization of IsLiveness that justifies its definition: any finite sequence can be extended to an infinite sequence satisfying a liveness property.

theorem Cslib.ωLanguage.isSafety_closure {α : Type u_1} (p : ωLanguage α) : p.closure.IsSafety

p.closure is always a safety property for any ω-language p.

theorem Cslib.ωLanguage.isLiveness_sup_compl_closure {α : Type u_1} (p : ωLanguage α) : (p ⊔ p.closureᶜ).IsLiveness

p ⊔ p.closureᶜ is always a liveness property for any ω-language p.

theorem Cslib.ωLanguage.exists_safetyLivenessDecomposition {α : Type u_1} (p : ωLanguage α) : ∃ (q : ωLanguage α) (r : ωLanguage α), q.IsSafety ∧ r.IsLiveness ∧ p = q ⊓ r

Every property p is the intersection of a safety property (namely, p.closure) and a liveness property (namely, p ⊔ p.closureᶜ).