Reachability via a subset of processes

This file develops a theory of reachability via a subset of processes, that is, what happens when only a subset of processes can receive messages and take steps. It culminates with two "diamond properties" of this more refined reachability relation.

References

• [Volzer2004] H. Völzer, A constructive proof for FLP. Information Processing Letters 92(2), (October 2004) 83–87.

def Cslib.FLP.Algorithm.CanReachVia {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (a : Algorithm P M S) (ps : Set P) (s1 s2 : State P M S) : Prop

a.CanReachVia ps s1 s2 means that state s2 is reachable from state s1 via a finite execution of algorithm a in which all messages received have destinations in ps.

Equations

• a.CanReachVia ps s1 s2 = Relation.ReflTransGen (fun (s t : Cslib.FLP.State P M S) => ∃ (x : Cslib.FLP.Action P M), Cslib.FLP.DestIn ps x ∧ a.lts.Tr s x t) s1 s2

theorem Cslib.FLP.CanReachVia.iff_exists_mTr {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {ps : Set P} {s s' : State P M S} : a.CanReachVia ps s s' ↔ ∃ (xs : List (Action P M)), a.lts.MTr s xs s' ∧ List.Forall (DestIn ps) xs

Restricted reachability is witnessed by a finite trace whose destinations lie in ps.

theorem Cslib.FLP.CanReachVia.canReach {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {ps : Set P} {s s' : State P M S} (h : a.CanReachVia ps s s') : a.lts.CanReach s s'

a.CanReachVia ps s s' implies a.lts.CanReach s s' for any ps.

theorem Cslib.FLP.CanReachVia.refl {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} (ps : Set P) (s : State P M S) : a.CanReachVia ps s s

a.CanReachVia ps s s is true for any ps.

theorem Cslib.FLP.CanReachVia.stepL {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {ps : Set P} {x : Action P M} {s1 s2 s3 : State P M S} (hx : DestIn ps x) (h1 : a.lts.Tr s1 x s2) (h2 : a.CanReachVia ps s2 s3) : a.CanReachVia ps s1 s3

Extending CanReachVia on the left by one step.

theorem Cslib.FLP.CanReachVia.diamond {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {ps : Set P} {s s1 s2 : State P M S} (h1 : a.CanReachVia ps s s1) (h2 : a.CanReachVia psᶜ s s2) : ∃ (s' : State P M S), a.CanReachVia psᶜ s1 s' ∧ a.CanReachVia ps s2 s'

A diamond property for CanReachVia. This theorem formalizes Proposition 1 of [Volzer2004].

theorem Cslib.FLP.CanReachVia.subset_inp {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] {ps : Set P} {inp1 inp2 : P → Bool} {s1 : State P M S} (he : Set.EqOn inp1 inp2 ps) (hr : a.CanReachVia ps (a.start inp1) s1) : ∃ (s2 : State P M S), a.CanReachVia ps (a.start inp2) s2 ∧ s2.proc = s1.proc

If inputs inp1 and inp2 agree on all processes in ps and state s is reachable from the initial state determined by inp1 by receiving messages with destinations in ps only, then there exists a state s2 that agrees with s on the states of all processes and is reachable from the initial state determined by inp2 by receiving messages with destinations in ps only. This theorem is implicitly used in the proof of Lemma 1 of [Volzer2004].