probabilistic Guarded Command Language (pGCL)

Main definitions

• pGCL: The definition of a variant of the pGCL language.
• pGCL.SmallStep: The small step operations semantics of pGCL.
• pGCL.𝒬: The induced operational Markov Decision Process (MDP) by the small step operational semantics.
• pGCL.wp: The weakest preexpectation transformer of a pGCL program.
• pGCL.op: The operational optimal expected cost transformer expressed as the optimal expected cost of pGCL.𝒬.
• pGCL.op_eq_wp: Theorem stating that the optimal expected cost is equal the weakest preexpectation.
• pGCL.iSup_iInf_EC_eq_wp: Theorem stating that the ⨅⨆ formulation of the optimal expected cost is equal to the weakest preexpectation.

theorem pGCL.iSup_iInf_EC_eq_wp {ϖ : Type u_1} {X : Exp ϖ} {C : pGCL ϖ} {σ : States ϖ} [DecidableEq ϖ] : ⨅ (𝒮 : 𝔖[𝒬]), ⨆ (n : ℕ), MDP.EC (𝒬.cost X) 𝒮 n (·⟨C,σ⟩) = C.wp X σ