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. semantics.pGCL.wp: The weakest preexpectation transformer of a pGCL program.pGCL.wp_eq_op: Theorem stating that the optimal expected cost is equal the weakest preexpectation.pGCL.iInf_iSup_EC_eq_wp: Theorem stating that the⨆⨅formulation of the optimal expected cost is equal to the weakest preexpectation.
theorem
pGCL.iSup_iSup_EC_eq_wp
{𝒱 : Type u_1}
{Γ✝ : 𝒱 → Type u_2}
{X : State Γ✝ → ENNReal}
{C : pGCL Γ✝}
{σ : State Γ✝}
[DecidableEq 𝒱]
:
⨆ (𝒮 : 𝔖[SmallStepSemantics.mdp]),
⨆ (n : ℕ), SmallStepSemantics.mdp.EC (SmallStepSemantics.cost X) 𝒮 n (Conf.prog C σ) = wp[Optimization.Angelic]⟦@C⟧ X σ
theorem
pGCL.iInf_iSup_EC_eq_wp
{𝒱 : Type u_1}
{Γ✝ : 𝒱 → Type u_2}
{X : State Γ✝ → ENNReal}
{C : pGCL Γ✝}
{σ : State Γ✝}
[DecidableEq 𝒱]
:
⨅ (𝒮 : 𝔖[SmallStepSemantics.mdp]),
⨆ (n : ℕ), SmallStepSemantics.mdp.EC (SmallStepSemantics.cost X) 𝒮 n (Conf.prog C σ) = wp[Optimization.Demonic]⟦@C⟧ X σ
theorem
pGCL.iSup_iSup_EC_eq_wfp
{𝒱 : Type u_1}
{Γ✝ : 𝒱 → Type u_2}
{X : State Γ✝ → ENNReal}
{C : pGCL Γ✝}
{σ : State Γ✝}
[DecidableEq 𝒱]
:
⨆ (𝒮 : 𝔖[SmallStepSemantics.mdp]),
⨆ (n : ℕ), SmallStepSemantics.mdp.EC (SmallStepSemantics.cost X) 𝒮 n (Conf.prog C σ) = wfp[Optimization.Angelic]⟦@C⟧ X σ
theorem
pGCL.iInf_iSup_EC_eq_wfp
{𝒱 : Type u_1}
{Γ✝ : 𝒱 → Type u_2}
{X : State Γ✝ → ENNReal}
{C : pGCL Γ✝}
{σ : State Γ✝}
[DecidableEq 𝒱]
:
⨅ (𝒮 : 𝔖[SmallStepSemantics.mdp]),
⨆ (n : ℕ), SmallStepSemantics.mdp.EC (SmallStepSemantics.cost X) 𝒮 n (Conf.prog C σ) = wfp[Optimization.Demonic]⟦@C⟧ X σ