Proposition 8.1 (iv), p. 219 — a projection preserves nonblocking, nonrejecting and proper

Proved

RamadgeWonham.Quotient.prop_8_1_iv

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

discrete-event-systemsp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1supervisory-control

Let $\mathcal G$ be a trim generator over a finite alphabet $\Sigma$ with controllable events $\Sigma_c$ . Let $\mathcal S$ and $\hat{\mathcal S}$ be supervisors with accessible automata, let $\mathcal S$ be complete with respect to $\mathcal G$ , and let $\pi : \mathcal S \to \hat{\mathcal S}$ be a projection. Then

$\mathcal S$ is nonblocking iff $\hat{\mathcal S}$ is nonblocking;
$\mathcal S$ is nonrejecting iff $\hat{\mathcal S}$ is nonrejecting;
$\mathcal S$ is proper iff $\hat{\mathcal S}$ is proper.

Formalization Note Standing assumptions as hypotheses: $\Sigma$ finite, $\mathcal G$ trim, both supervisor automata accessible.

Preamble

import Mathlib
import Definitions.Def_RamadgeWonham_Quotient_Projection

Formal statement

namespace RamadgeWonham.Quotient

open Shared.Generator

/-- Proposition 8.1 (iv) (p. 219): if `𝒮` is complete with respect to `𝒢` and `π : 𝒮 → 𝒮̂` is a
projection, then `𝒮` is nonblocking (respectively, nonrejecting, proper) iff `𝒮̂` is nonblocking
(respectively, nonrejecting, proper). -/
theorem prop_8_1_iv
    {α : Type} [Fintype α] {Ec : Set α} (𝒢 : Shared.Generator α) (h𝒢 : 𝒢.L = Shared.pre 𝒢.Lm)
    (𝒮 𝒮h : Shared.Supervisor α Ec) (h𝒮acc : 𝒮.S.Accessible) (h𝒮hacc : 𝒮h.S.Accessible)
    (h𝒮 : Shared.Complete 𝒢 𝒮)
    (π : 𝒮.S.Q → 𝒮h.S.Q) (hπ : IsProjection 𝒮 𝒮h π) :
    (Shared.Nonblocking 𝒢 𝒮 ↔ Shared.Nonblocking 𝒢 𝒮h) ∧ (Shared.Nonrejecting 𝒢 𝒮 ↔ Shared.Nonrejecting 𝒢 𝒮h) ∧
      (Shared.Proper 𝒢 𝒮 ↔ Shared.Proper 𝒢 𝒮h) := by sorry

end RamadgeWonham.Quotient

Source

Ramadge and Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. Control Optim. 25(1), 1987, p. 219, Proposition 8.1 (iv)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph