From 5afecef00366cfc27ef280089cc3fcd2bd57e482 Mon Sep 17 00:00:00 2001 From: Traian-Florin Serbanuta Date: Tue, 29 Nov 2022 12:58:13 +0200 Subject: [PATCH] More proofs --- ...Corectness-All-Path-Reachability-Proofs.md | 209 ++++++++++++++++-- 1 file changed, 187 insertions(+), 22 deletions(-) diff --git a/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md index 01249d59910..728843e522e 100644 --- a/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md +++ b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md @@ -15,13 +15,193 @@ they are equisatisfiable (they denote the same set of configurations). ### All-path finally -Given a formula `φ`, let `AFφ` denote the formula “all-path finally” `φ`, -defined by: +Given a formula `φ`, let `AFφ` denote the formula “all-path finally” `φ`, whose +intended semantics is: "the set of configurations for which on all paths, +in a finite number of steps, `φ` holds". +Let us will first show that `AFφ` can be described by the formula ``` AFφ := μX.φ ∨ (○X ∧ •⊤) ``` +Let `Top` be the set of all configurations, and let `Prev` be the pointwise +extension of the function mapping a configuration to the set of all +configurations which can reach the given configuration in one step. +and `∁` be the complement operator on sets. + +The semantics of `μX.φ ∨ (○X ∧ •⊤)` is `LFP(G)` where +``` +G(X) := ⟦φ⟧ ∪ ( ∁(Prev(∁(X))) ∩ Prev(Top) ) +``` +Note that, since `X` is positively occuring in the scope of `μ`, `G` is +monotone, so the `LFP(G)` exists and can be defined according to the +Knaster-Tarski result, as the intersection of all pre-fixpoints of `G`, +that is, all `A` such that `G(A) ⊆ A`. + +Let us also note that `x ∈ G(A)` iff `φ` holds for `x` or `∅ ⊂ Prev⁻¹({x}) ⊆ A`, +i.e., iff `φ` holds for `x` or `x` is not stuck and all its transitions lead +into `A`. Indeed, +``` +x ∈ G(A) ⟺ × ∈ ⟦φ⟧ ∪ ( ∁(Prev(∁(A))) ∩ Prev(Top) +⟺ × ∈ ⟦φ⟧ or (x ∈ ∁(Prev(∁(A))) and x ∈ Prev(Top)) +⟺ × ∈ ⟦φ⟧ or (¬ x ∈ Prev(∁(A)) and ∅ ⊂ Prev⁻¹({x})) +⟺ × ∈ ⟦φ⟧ or (¬ (∃y y ∈ ∁(A) ∧ x ∈ Prev(y)) and ∅ ⊂ Prev⁻¹({x})) +⟺ × ∈ ⟦φ⟧ or (¬ (∃y ¬y ∈ A ∧ x ∈ Prev(y)) and ∅ ⊂ Prev⁻¹({x})) +⟺ × ∈ ⟦φ⟧ or ((∀y y ∈ A ∨ ¬ x ∈ Prev(y)) and ∅ ⊂ Prev⁻¹({x})) +⟺ × ∈ ⟦φ⟧ or ((∀y x ∈ Prev(y) ⟹ y ∈ A) and ∅ ⊂ Prev⁻¹({x})) +⟺ × ∈ ⟦φ⟧ or (Prev⁻¹({x}) ⊆ A and ∅ ⊂ Prev⁻¹({x})) +⟺ × ∈ ⟦φ⟧ or (∅ ⊂ Prev⁻¹({x}) ⊆ A) +``` + +Let `stuck x` be defined as `Prev⁻¹(x) = ∅` and let `x τ y` be defined +as `y ∈ Prev⁻¹({x})`. +We can also express `∅ ⊂ Prev⁻¹({x}) ⊆ A` in terms +of stuck and transitions, as `¬ stuck x ∧ ∀y x τ y → y ∈ A`. +Hence, `x ∈ G(A)` if either `x` matches `ϕ`, or `x` is not stuck and all +its transitions go into `A`. + +We can coinductively define (the possibly infinite) complete traces of the +transition system determined by `Prev⁻¹` starting in an element `a` as being: +either just `a`, if `stuck a`, or `a` followed by a trace starting in `b` for +some `b` such that `a τ b`. +Given this definition, the trace semantics for `AF ϕ` is +``` +⟦AF ϕ⟧ ::= { a | forall tr trace starting in a, exists b in tr such that b ∈ ⟦ϕ⟧ } +``` + +Let us first argue that `⟦AF ϕ⟧` is a pre-fixpoint of `G`, i.e., that +`G(⟦AF ϕ⟧) ⊆ ⟦AF ϕ⟧`. +Take `a ∈ G(⟦AF ϕ⟧)`. Then either `a ∈ ⟦ϕ⟧` or `¬ stuck a` and for all `b` +such that `a τ b`, `b ∈ ⟦AF ϕ⟧`. +Let `tr` be a complete trace starting in `a`. +If `a ∈ ⟦ϕ⟧`, then we can choose precisely `a` as the witness on that trace +for which `ϕ` holds. +Otherwise, `¬ stuck a` and for all `b` such that `a τ b`, `b ∈ ⟦AF ϕ⟧`. +Since `¬ stuck a` it must be that `tr` cannot be just `a` (it's complete), so +there must exist a `b` such that `a τ b` and `b` is the start of a trace `tr'` +such that `tr = a ⋅ tr'`. However, since `a τ b`, it follows that`b ∈ ⟦AF ϕ⟧`, +so `tr'` must contain a witness for which `ϕ` holds; that witness is also a +witness for `tr`. + +Let us now argue that `⟦AF ϕ⟧` is a post-fixpoint of `G`, i.e., that +`⟦AF ϕ⟧ ⊆ G(⟦AF ϕ⟧)`. +Take `a ∈ ⟦AF ϕ⟧`. We need to prove that either `a ∈ ⟦ϕ⟧` or `¬ stuck a` and +for all `b` such that `a τ b`, `b ∈ ⟦AF ϕ⟧`, +If `ϕ` holds for `a` then we're done. Assume `a ∉ ⟦ϕ⟧`. +Then it must be that `¬ stuck a`, since otherwise `a` would be a complete trace +starting in `a` with no witness for which `ϕ` holds. +Let now `b` be such `a τ b`. We need to show that `b ∈ ⟦AF ϕ⟧`. Let `tr` be a +complete trace starting in `b`. Then `a ⋅ tr` is a complete trace starting in `a`. +Since `a ∈ ⟦AF ϕ⟧`, there must be a witness in `a ⋅ tr` for which `ϕ` holds. +However, since `ϕ` doesn't hold for `a`, the witness must be part of `tr` +Since `tr` was chosen arbitrarily, it must be that `a ∈ ⟦AF ϕ⟧`. + +Therefore, `⟦AF ϕ⟧` is a fixpoint for `G`. To show that it is the LFP of `G` it +suffices to prove that it is included in any pre-fixpoint of `G`. +Let `A` be a pre-fixpoint of `G`, i.e., `G(A) ⊆ A`. That means that +(1) `A` contains all configurations matching `ϕ`; and +(2) `A` contains all configurations which are not stuck and transition on all + paths into `A` +Assume by contradiction that there exists `a ∈ ⟦AF ϕ⟧` such that `a ∉ A`. +We will coinductively construct a complete trace starting in `a` with no +witness in `A`. Since `A` contains all configurations for which `ϕ` holds, +this would contradict the fact that `a ∈ ⟦AF ϕ⟧`. +- if `stuck a` is stuck, then take the complete trace `a` +- if `¬ stuck a`, since `a ∉ A`, it means that (2) is false; hence it exists + a transition `a τ b` such that `b ∉ A`. Then take the complete trace + `a ⋅ tr` where `tr` is obtained by applying the above process for `b ∉ A`. + +Hence, `⟦AF ϕ⟧` is the LFP of `G`. Let us now study when this LFP can be +expressed according to Kleene's formula, i.e., when `LFP(G) = ⋃ₙGⁿ(∅)`. + +Given a complete trace `tr`, let `trₙ` be the `n`th element of the trace, if +it exists. + +Let us now argue that for any natural `n`, `Gⁿ⁺¹(∅)` denotes the set of +configurations for which in at most `n` steps, on all paths, `φ` holds, i.e., +``` +Gⁿ⁺¹(∅) = { a | forall tr trace starting in a, exists k ≤ n such that trₖ ∈ ⟦ϕ⟧ } +``` +We do that by induction on `n`: +- Base case: + ``` + G(∅) = ⟦φ⟧ ∪ ( ∁(Prev(∁(∅))) ∩ Prev(Top) ) + = ⟦φ⟧ ∪ ( ∁(Prev(Top)) ∩ Prev(Top) ) + = ⟦φ⟧ ∪ ∅ + = ⟦φ⟧ + = {a | a ∈ ⟦ϕ⟧} + = { a | forall tr trace starting in a, exists k ≤ 0 such that trₖ ∈ ⟦ϕ⟧} + ``` +- Induction case. + `a ∈ Gⁿ⁺²(∅) = G(Gⁿ⁺¹(∅))` iff `φ` holds for `a` or `¬ stuck a` and forall b + such that `a τ b`, `b ∈ Gⁿ⁺¹(∅)`. + Let `tr` be a complete trace starting in `a`. If the trace is just `a`, + then it must be that `a` is stuck, therefore `\phi` holds for `a` and since + `0 ≤ n+1` we are done. Otherwise assume `tr = a ⋅ tr'` such that `tr'` is a + complete trace starting in a configuration `b`. Then `a τ b`, hence `b ∈ Gⁿ⁺¹(∅)`. + By the induction hypothesis, there exists `k ≤ n` such that `tr'ₖ ∈ ⟦ϕ⟧`, hence + `trₖ₊₁ ∈ ⟦ϕ⟧`. + Conversely, let `a` be such that forall `tr` trace starting in a, there exists + `k ≤ 0` such that `trₖ ∈ ⟦ϕ⟧`. If `a ∈ ⟦ϕ⟧`, then `a ∈ G(Gⁿ⁺¹(∅))`. Suppose + `a ∉ ⟦ϕ⟧`. Then `¬ stuck a` (otherwise `a` would be a trace starting in `a` + for which the hypothesis would not hold). Let `b` be such `a τ b`. + +Since `G` is monotone, we can deduce that `Gⁿ(∅) ⊆ Gⁿ⁺¹(∅)` +(obviously `∅ ⊆ G(∅)` and then by applying monotone G `n` times). +Therefore, the limit `⋁ₙGⁿ(∅)` exists. + +By the characterization of `Gⁿ(∅)` presented above, it follows that `⋁ₙGⁿ(∅)` +denotes the set of configurations for which there exists `n` sucht that in at +most `n` steps, on all paths, `φ` holds. + +However, in order for it to be expressible as the ML formula `μX.φ ∨ (○X ∧ •⊤)` +it would have to be the `LFP(G)`, which would be true if `G(⋁ₙGⁿ(∅)) = ⋁ₙGⁿ(∅)`. + +First, for all `n`, `Gⁿ(∅) ⊆ ⋁ₙGⁿ(∅)` and since `G` is monotone, +`Gⁿ⁺¹(∅) ⊆ G(⋁ₙGⁿ(∅))`. Also, obviously `G⁰(∅) = ∅ ⊆ G(⋁ₙGⁿ(∅))`. +Therefore, `⋁ₙGⁿ(∅) ⊆ G(⋁ₙGⁿ(∅))`. + +Hence, to have equality, we would need that `G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) = ∅`. +We have that: +``` +x ∈ G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) +⟺ x ∈ G(⋁ₙGⁿ(∅)) and x ∉ ⋁ₙGⁿ(∅) +⟺ (x ∈ ⟦φ⟧ or ∅ ⊂ Prev⁻¹({x}) ⊆ ⋁ₙGⁿ(∅)) and x ∉ ⋁ₙGⁿ(∅) +⟺ ∅ ⊂ Prev⁻¹({x}) ⊆ ⋁ₙGⁿ(∅) and x ∉ ⋁ₙGⁿ(∅) (since ⟦φ⟧ ⊆ ⋁ₙGⁿ(∅)) +``` + +Given the above relation, we deduce that a sufficient condition ensuring that +`G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) = ∅` is that the transition system is finitely branching, +i.e., that `Prev⁻¹({x})` is finite for any `x`. Indeed, suppose +there exists `x ∈ G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅)`. Then, it must hold that +`∅ ⊂ Prev⁻¹({x}) ⊆ ⋁ₙGⁿ(∅)` and `x ∉ ⋁ₙGⁿ(∅)` +Let `k`, `y₁`, ..., `yₖ` be such that `Prev⁻¹({x}) = {y₁, ..., yₖ}`. +Since `∀y x ∈ Prev(y) ⟹ ∃n y ∈ Gⁿ(∅)`, it must be that there exist +`n₁`, ..., `nₖ` such that `yᵢ ∈ Gⁿⁱ(∅)` for any `1≤i≤k`. +Let `m = 𝐦𝐚𝐱 {n₁, ... , nₖ}`. Since `(Gⁿ(∅))ₙ` is an ascending chain, +it follows that `yᵢ ∈ Gᵐ(∅)` for any `1≤i≤k`, therefore `Prev⁻¹({x}) ⊆ Gᵐ(∅)`, +whence `x ∈ Gᵐ⁺¹(∅)`, contradiction with the fact that `x ∉ ⋁ₙGⁿ(∅)`. + +In what follows we will assume that the transition system generated by the +theory of interest is finitely branching. Nevertheless, before continuing, let +us give an example of a system and property for which the above construction is +not a fixpoint. + +#### CTL allways-finally `φ` vs. `μX.φ ∨ (○X ∧ •⊤)` + +Consider the following K theory + +``` +syntax KItem ::= "x" + +rule Y:Int => Y -Int 1 requires Y>0 +rule x => ?Y:Int ensures Y >= 0 +``` + +and the claim `x → AF 0` + +According to the CTL understanding of `AF`, the claim does not hold, as + #### Semantics of `AFφ` By the definition above, `AFφ` is semantically defined as `LFP(G)`, the @@ -38,26 +218,11 @@ possible transitions lead into `X`. Since `AFφ` is a fixed-point of `G`, the identity `G(AFφ) = AFφ` holds, whence `AFφ = φ ∨ (○AFφ ∧ •⊤)`. -Moreover, `G` is monotone (`X` occurs in a positive position) and we can show -that the conditions of Kleene's fixed-point theorem are satisfied: -`Gⁿ(⊥) ⊆ Gⁿ⁺¹(⊥)`, because `Gⁿ(⊥)` denotes the set of configurations for which -on all paths, in at most `n-1` steps, `φ` holds. - -Let us argue the above by induction on `n-1`. -- Base case: `G(⊥) = φ ∨ (○⊥ ∧ •⊤) = φ ∨ (¬•¬⊥ ∧ •⊤) = φ ∨ (¬•⊤ ∧ •⊤) = φ ∨ ⊥ = φ`, - so `G(⊥)` is the set of configurations for which `φ` holds. -- Induction case: Assuming `Gⁿ(⊥)` denotes the set of configurations for which - on all paths, in at most `n-1` steps, `φ` holds, `Gⁿ⁺¹(⊥) = G(Gⁿ(⊥))` will be - the union between the set of configurations for which `φ` holds and those - which are not stuck and whose all possible transitions lead into the set of - configurations for which on all paths, in at most `n-1` steps, `φ` holds, but - these are precisely the configurations for which on all paths, in at most `n` - steps, `φ` holds. - -From Kleene's theorem, `AFφ = ⋁ₙGⁿ(⊥)`, whence, a configuration is in `AFφ` iff -it is in `Gⁿ(⊥)` for some positive integer `n`. By the characterization of -`Gⁿ(⊥)` presented above, it follows that `AFφ` denotes the set of configurations -for which on all paths, in a finite number of steps, `φ` holds. +Moreover, since `⊥ ⊆ LFP(G)`, by iteratively applying monotone `G` and since +`LFP(G)` is a fixpoint, we get that for all `n`, `Gⁿ(⊥) ⊆ LFP(G)`, whence +`⋁ₙGⁿ(⊥) ⊆ LFP(G)`. + +For the formula ### Total corectness all-path reachability claims