More proofs

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