Library Process

Require Import HahnBase.
Require Import List.
Require Import Morphisms.
Require Import Prelude.
Require Import Setoid.
Require Import Utf8.

Import ListNotations.

Process Algebra Theory


Module Type Processes(dom : Domains).
  Export dom.

Statics

Expressions


Inductive ProcExpr :=
  | PEconst(v : Val)
  | PEvar(x : ProcVar)
  | PEop(e1 e2 : ProcExpr).

Add Search Blacklist "ProcExpr_rect".
Add Search Blacklist "ProcExpr_ind".
Add Search Blacklist "ProcExpr_rec".
Add Search Blacklist "ProcExpr_sind".

Free variables


Fixpoint pexpr_fv (e : ProcExpr) : list ProcVar :=
  match e with
    | PEconst _ => []
    | PEvar x => [x]
    | PEop e1 e2 => pexpr_fv e1 ++ pexpr_fv e2
  end.

Conditions


Inductive ProcCond :=
  | PBconst(b : bool)
  | PBnot(b : ProcCond)
  | PBand(b1 b2 : ProcCond)
  | PBeq(e1 e2 : ProcExpr).

Add Search Blacklist "ProcCond_rect".
Add Search Blacklist "ProcCond_ind".
Add Search Blacklist "ProcCond_rec".
Add Search Blacklist "ProcCond_sind".

Free variables


Fixpoint pcond_fv (b : ProcCond) : list ProcVar :=
  match b with
    | PBconst _ => []
    | PBnot b' => pcond_fv b'
    | PBand b1 b2 => pcond_fv b1 ++ pcond_fv b2
    | PBeq e1 e2 => pexpr_fv e1 ++ pexpr_fv e2
  end.

Processes

All actions have an associated guard and effect. Rather than giving syntax for defining such guards and effects, we simply assume the following two functions:

Parameter guard : Act -> Val -> ProcCond.
Parameter effect : Act -> Val -> ProcCond.

Processs maintain the well-formedness condition that any action argument (in Pact) and condition (in Pcond) is closed (i.e., does not have any free variables). This condition is enforced already here, by letting action arguments be values and conditions be Booleans. Note that summations can be used in combination with these (Boolean) values, to make them useful.

Inductive Proc :=
  | Pepsilon
  | Pdelta
  | Pact(a : Act)(v : Val)
  | Passert(b : ProcCond)
  | Pseq(P1 P2 : Proc)
  | Palt(P1 P2 : Proc)
  | Ppar(P1 P2 : Proc)
  | Plmerge(P1 P2 : Proc)
  | Psum(f : Val -> Proc)
  | Pcond(b : bool)(P : Proc)
  | Piter(P : Proc).

Add Search Blacklist "Proc_rect".
Add Search Blacklist "Proc_ind".
Add Search Blacklist "Proc_rec".
Add Search Blacklist "Proc_sind".

Lemma proc_sum_ext :
  forall f f', f = f' -> Psum f = Psum f'.

Below is a shorthand tactic for doing induction on the inductive structure of processes.

Ltac proc_induction P :=
  induction P as [
    
    |
    
    |
    
    a E|
    
    B|
    
    P1 IH1 P2 IH2|
    
    P1 IH1 P2 IH2|
    
    P1 IH1 P2 IH2|
    
    P1 IH1 P2 IH2|
    
    f IH|
    
    B P' IH |
    
    P IH
  ].

Free variables

The set of free variables in processes is defined in terms of a predicate instead of a fixpoint. This is needed, since processes are coinductively defined.

Definition act_fv (a : Act)(v : Val) : list ProcVar :=
  pcond_fv (guard a v) ++ pcond_fv (effect a v).

Fixpoint proc_fv (P : Proc)(x : ProcVar) : Prop :=
  match P with
    | Pepsilon => False
    | Pdelta => False
    | Pact a v => In x (act_fv a v)
    | Passert b => In x (pcond_fv b)
    | Pseq Q R => proc_fv Q x \/ proc_fv R x
    | Palt Q R => proc_fv Q x \/ proc_fv R x
    | Ppar Q R => proc_fv Q x \/ proc_fv R x
    | Plmerge Q R => proc_fv Q x \/ proc_fv R x
    | Psum f => exists v, proc_fv (f v) x
    | Pcond _ Q => proc_fv Q x
    | Piter Q => proc_fv Q x
  end.

Successful termination

An explicit notion pterm P of termination of process P is defined to define the reduction rules for sequential composition Pseq.
Intuitively proc_term P means that P has the choice to have no further behaviour and behave like Pepsilon. In other words, proc_term P means that P is bisimilar to Palt P Pepsilon (which we prove later, after defining bisimilarity).

Inductive pterm : Proc -> Prop :=
  
  | pterm_epsilon : pterm Pepsilon
  
  | pterm_seq P Q : pterm P -> pterm Q -> pterm (Pseq P Q)
  
  | pterm_alt_l P Q : pterm P -> pterm (Palt P Q)
  | pterm_alt_r P Q : pterm Q -> pterm (Palt P Q)
  
  | pterm_par P Q : pterm P -> pterm Q -> pterm (Ppar P Q)
  
  | pterm_lmerge P Q : pterm P -> pterm Q -> pterm (Plmerge P Q)
  
  | pterm_sum f v : pterm (f v) -> pterm (Psum f)
  
  | pterm_cond P : pterm P -> pterm (Pcond true P)
  
  | pterm_iter P : pterm (Piter P).

Add Search Blacklist "pterm_ind".
Add Search Blacklist "pterm_sind".

Dynamics

Process stores

Process stores are used on the denotational and operational semantics of processes to give an interpretation to process-algebraic variables.

Definition ProcStore := ProcVar -> Val.

The following definition captures two stores agreeing on a given predicate phi over process variables.

Definition pstore_agree (phi : ProcVar -> Prop)(s1 s2 : ProcStore) : Prop :=
  forall x, phi x -> s1 x = s2 x.

Global Instance pstore_agree_symm :
  forall phi, Symmetric (pstore_agree phi).

Lemma pstore_agree_split :
  forall phi1 phi2 s1 s2,
  pstore_agree (fun x => phi1 x \/ phi2 x) s1 s2 <->
  pstore_agree phi1 s1 s2 /\ pstore_agree phi2 s1 s2.

Lemma pstore_agree_app :
  forall xs1 xs2 s1 s2,
  pstore_agree (fun x => In x (xs1 ++ xs2)) s1 s2 <->
  pstore_agree (fun x => In x xs1) s1 s2 /\
  pstore_agree (fun x => In x xs2) s1 s2.

Lemma pstore_agree_weaken :
  forall (phi1 phi2 : ProcVar -> Prop)(s1 s2 : ProcStore),
    (forall x, phi1 x -> phi2 x) ->
  pstore_agree phi2 s1 s2 ->
  pstore_agree phi1 s1 s2.

Expressions

The denotational semantics pexpr_eval e s of expressions e with respect to a process store s is defined in the standard way.

Fixpoint pexpr_eval (e : ProcExpr)(s : ProcStore) : Val :=
  match e with
    | PEconst v => v
    | PEvar x => s x
    | PEop e1 e2 => val_op (pexpr_eval e1 s) (pexpr_eval e2 s)
  end.

The evaluation of process-algebraic expressions e only depends on the variables occuring freely in e.

Lemma pexpr_agree :
  forall e s1 s2,
  pstore_agree (fun x => In x (pexpr_fv e)) s1 s2 ->
  pexpr_eval e s1 = pexpr_eval e s2.

Standard property relating expression evaluation to store updates.

Lemma pexpr_eval_upd :
  forall e s x v,
  ~ In x (pexpr_fv e) ->
  pexpr_eval e (update procvar_eq_dec s x v) = pexpr_eval e s.

Conditions

The denotational semantics pcond_eval b s of conditions b with respect to a process store s is defined in the standard way.

Fixpoint pcond_eval (b : ProcCond)(s : ProcStore) : bool :=
  match b with
    | PBconst b' => b'
    | PBnot b' => negb (pcond_eval b' s)
    | PBand b1 b2 => pcond_eval b1 s && pcond_eval b2 s
    | PBeq e1 e2 => if val_eq_dec (pexpr_eval e1 s) (pexpr_eval e2 s) then true else false
  end.

Lemma pcond_eval_excl :
  forall b s, pcond_eval b s = true \/ pcond_eval b s = false.

The evaluation of process-algebraic conditions b only depends on the variables occuring freely in b.

Lemma pcond_agree :
  forall b s1 s2,
  pstore_agree (fun x => In x (pcond_fv b)) s1 s2 ->
  pcond_eval b s1 = pcond_eval b s2.

Lemma pcond_eval_upd :
  forall b s x v,
  ~ In x (pcond_fv b) ->
  pcond_eval b (update procvar_eq_dec s x v) = pcond_eval b s.

Processes

The labelled small-step reduction rules of processes are defined below, as pstep.

Inductive ProcLabel :=
  | PLact(a : Act)(v : Val)
  | PLassert.

Add Search Blacklist "ProcLabel_rect".
Add Search Blacklist "ProcLabel_ind".
Add Search Blacklist "ProcLabel_rec".
Add Search Blacklist "ProcLabel_sind".

Inductive pstep : Proc -> ProcStore -> ProcLabel -> Proc -> ProcStore -> Prop :=
  
  | pstep_act s a v s' :
    pcond_eval (guard a v) s = true ->
    pcond_eval (effect a v) s' = true ->
    pstep (Pact a v) s (PLact a v) Pepsilon s'
  
  | pstep_assert b s :
    pcond_eval b s -> pstep (Passert b) s PLassert Pepsilon s
  
  | pstep_seq_l P Q l s P' s' :
    pstep P s l P' s' ->
    pstep (Pseq P Q) s l (Pseq P' Q) s'
  | pstep_seq_r P Q l s Q' s' :
    pterm P -> pstep Q s l Q' s' -> pstep (Pseq P Q) s l Q' s'
  
  | pstep_alt_l P Q l s P' s' :
    pstep P s l P' s' -> pstep (Palt P Q) s l P' s'
  | pstep_alt_r P Q l s Q' s' :
    pstep Q s l Q' s' -> pstep (Palt P Q) s l Q' s'
  
  | pstep_par_l P Q l s P' s' :
    pstep P s l P' s' ->
    pstep (Ppar P Q) s l (Ppar P' Q) s'
  | pstep_par_r P Q l s Q' s' :
    pstep Q s l Q' s' ->
    pstep (Ppar P Q) s l (Ppar P Q') s'
  
  | pstep_lmerge P Q l s P' s' :
    pstep P s l P' s' ->
    pstep (Plmerge P Q) s l (Ppar P' Q) s'
  
  | pstep_sum f l v P s s' :
    pstep (f v) s l P s' -> pstep (Psum f) s l P s'
  
  | pstep_cond P l s P' s' :
    pstep P s l P' s' -> pstep (Pcond true P) s l P' s'
  
  | pstep_iter P s a P' s' :
    pstep P s a P' s' -> pstep (Piter P) s a (Pseq P' (Piter P)) s'.

Add Search Blacklist "pstep_ind".
Add Search Blacklist "pstep_ind".

Standard properties of the reduction rules.

Lemma pstep_par_frame_l :
  forall P s l P' s' Q,
  pstep P s l P' s' ->
  pstep (Ppar P Q) s l (Ppar P' Q) s'.
Lemma pstep_par_frame_r :
  forall P s l P' s' Q,
  pstep P s l P' s' ->
  pstep (Ppar Q P) s l (Ppar Q P') s'.

Lemma pstep_act_agree :
  forall P s a v Q s1 s2,
  pstore_agree (fun x => In x (act_fv a v)) s1 s2 ->
  pstep P s (PLact a v) Q s1 ->
  pstep P s (PLact a v) Q s2.

Lemma pstep_assert_store :
  forall P s P' s',
  pstep P s PLassert P' s' -> s = s'.

Lemma pstep_assert_agree :
  forall P s1 s2 P',
  pstore_agree (proc_fv P) s1 s2 ->
  pstep P s1 PLassert P' s1 ->
  pstep P s2 PLassert P' s2.

Fault semantics

A process P exhibits a fault with respect to a store s, written pfault P s, if P can violate an assertional process Passn in a single reduction step, from the configuration (P, s).

Inductive pfault : Proc -> ProcStore -> Prop :=
  
  | pfault_assert b s : pcond_eval b s = false -> pfault (Passert b) s
  
  | pfault_seq_l P Q s : pfault P s -> pfault (Pseq P Q) s
  | pfault_seq_r P Q s : pterm P -> pfault Q s -> pfault (Pseq P Q) s
  
  | pfault_alt_l P Q s : pfault P s -> pfault (Palt P Q) s
  | pfault_alt_r P Q s : pfault Q s -> pfault (Palt P Q) s
  
  | pfault_par_l P Q s : pfault P s -> pfault (Ppar P Q) s
  | pfault_par_r P Q s : pfault Q s -> pfault (Ppar P Q) s
  
  | pfault_lmerge P Q s : pfault P s -> pfault (Plmerge P Q) s
  
  | pfault_sum f v s : pfault (f v) s -> pfault (Psum f) s
  
  | pfault_cond P s : pfault P s -> pfault (Pcond true P) s
  
  | pfault_iter P s : pfault P s -> pfault (Piter P) s.

Add Search Blacklist "pfault_ind".
Add Search Blacklist "pfault_ind".

Standard properties of process faults.

Lemma passn_nfault :
  forall b s, ~ pfault (Passert b) s -> pcond_eval b s = true.

Lemma pfault_agree :
  forall P s1 s2,
  pstore_agree (proc_fv P) s1 s2 -> pfault P s1 -> pfault P s2.

Bisimulation

Bisimilarity is defined in the standard way.

CoInductive bisim : relation Proc :=
  | bisim_proc P Q :
      
      (pterm P <-> pterm Q) /\
      
      (forall s, pfault P s <-> pfault Q s) /\
      
      (forall s l P' s', pstep P s l P' s' -> exists Q', pstep Q s l Q' s' /\ bisim P' Q') /\
      
      (forall s l Q' s', pstep Q s l Q' s' -> exists P', pstep P s l P' s' /\ bisim P' Q') ->
    bisim P Q.

Definition bisim_f : relation (Val -> Proc) :=
  pointwise_relation Val bisim.

Notation "P ≃ Q" := (bisim P Q) (only printing, at level 80).
Notation "f ≃ g" := (bisim_f f g) (only printing, at level 80).

Bisimilarity is an equivalence relation.

Global Instance bisim_refl : Reflexive bisim.
Global Instance bisim_symm : Symmetric bisim.
Global Instance bisim_trans : Transitive bisim.
Global Instance bisim_equiv : Equivalence bisim.

Hint Resolve bisim_refl : core.

Global Instance bisim_f_refl : Reflexive bisim_f.
Global Instance bisim_f_symm : Symmetric bisim_f.
Global Instance bisim_f_trans : Transitive bisim_f.
Global Instance bisim_f_equiv : Equivalence bisim_f.

Hint Resolve bisim_f_refl : core.

Terminating processes can always be replaced by bisimilar ones.

Lemma bisim_term :
  forall P Q, bisim P Q -> pterm P -> pterm Q.
Add Parametric Morphism : pterm
  with signature bisim ==> iff as pterm_mor.

Faulting processes can always be replaced by bisimilar ones.

Lemma bisim_fault :
  forall P Q s, bisim P Q -> pfault P s -> pfault Q s.
Add Parametric Morphism : pfault
  with signature bisim ==> eq ==> iff as pfault_mor.

The following theorem makes explicit the intuitive meaning of successful termination.

Theorem bisim_term_intuit :
  forall P, pterm P -> bisim P (Palt Pepsilon P).

Congruence

Bisimilarity is a congruence for all connectives.

Add Parametric Morphism : Pseq
  with signature bisim ==> bisim ==> bisim
    as bisim_seq.

Add Parametric Morphism : Palt
  with signature bisim ==> bisim ==> bisim
    as bisim_alt.

Add Parametric Morphism : Ppar
  with signature bisim ==> bisim ==> bisim
    as bisim_par.

Add Parametric Morphism : Plmerge
  with signature bisim ==> bisim ==> bisim
    as bisim_lmerge.

Add Parametric Morphism : Psum
  with signature bisim_f ==> bisim
    as bisim_sum.

Add Parametric Morphism : Pcond
  with signature eq ==> bisim ==> bisim
    as bisim_cond.

Lemma bisim_iter_seq_cong :
  forall P1 P2 Q1 Q2,
  bisim P1 P2 ->
  bisim Q1 Q2 ->
  bisim (Pseq P1 (Piter Q1)) (Pseq P2 (Piter Q2)).

Add Parametric Morphism : Piter
  with signature bisim ==> bisim as bisim_iter.

Axiomatisation

Below are several bisimulation equivalences for the above language of processes.
Usually these equation are given or presented as an axiomatisation that is proven sound (and sometimes complete) with respect to bisimilarity. However, here they are given directly as bisimulation equivalences.

Theorem bisim_seq_epsilon_l :
  forall P, bisim (Pseq P Pepsilon) P.

Theorem bisim_seq_epsilon_r :
  forall P, bisim (Pseq Pepsilon P) P.

Theorem bisim_seq_delta :
  forall P, bisim (Pseq Pdelta P) Pdelta.

Theorem bisim_seq_assoc :
  forall P Q R, bisim (Pseq P (Pseq Q R)) (Pseq (Pseq P Q) R).

Theorem bisim_alt_comm :
  forall P Q, bisim (Palt P Q) (Palt Q P).

Theorem bisim_alt_assoc :
  forall P Q R, bisim (Palt P (Palt Q R)) (Palt (Palt P Q) R).

Theorem bisim_alt_dupl :
  forall P, bisim (Palt P P) P.

Theorem bisim_alt_delta :
  forall P, bisim (Palt P Pdelta) P.

Theorem bisim_alt_distr :
  forall P Q R,
  bisim (Pseq (Palt P Q) R) (Palt (Pseq P R) (Pseq Q R)).

Theorem bisim_par_comm :
  forall P Q, bisim (Ppar P Q) (Ppar Q P).

Theorem bisim_par_assoc :
  forall P Q R, bisim (Ppar P (Ppar Q R)) (Ppar (Ppar P Q) R).

Theorem bisim_par_epsilon_l :
  forall P, bisim (Ppar Pepsilon P) P.

Theorem bisim_par_epsilon_r :
  forall P, bisim (Ppar P Pepsilon) P.

Theorem bisim_par_delta :
  forall P, bisim (Ppar P Pdelta) (Pseq P Pdelta).

Theorem bisim_lmerge_unfold :
  forall P Q, bisim (Ppar P Q) (Palt (Plmerge P Q) (Plmerge Q P)).

Theorem bisim_lmerge_delta :
  forall P, bisim (Plmerge Pdelta P) Pdelta.

Theorem bisim_lmerge_epsilon_delta :
  bisim (Plmerge Pepsilon Pdelta) Pdelta.

Theorem bisim_lmerge_epsilon_act :
  forall a v P, bisim (Plmerge Pepsilon (Pseq (Pact a v) P)) Pdelta.

Theorem bisim_lmerge_act :
  forall a v P, bisim (Plmerge (Pact a v) P) (Pseq (Pact a v) P).

Theorem bisim_lmerge_epsilon :
  bisim (Plmerge Pepsilon Pepsilon) Pepsilon.

Theorem bisim_lmerge_epsilon_alt :
  forall P Q,
  bisim (Plmerge Pepsilon (Palt P Q)) (Palt (Plmerge Pepsilon P) (Plmerge Pepsilon Q)).

Theorem bisim_lmerge_alt :
  forall P Q R,
  bisim (Plmerge (Palt P Q) R) (Palt (Plmerge P R) (Plmerge Q R)).

Theorem bisim_lmerge_assoc :
  forall P Q R,
  bisim (Plmerge (Plmerge P Q) R) (Plmerge P (Ppar Q R)).

Theorem bisim_lmerge_seq_delta :
  forall P, bisim (Plmerge P Pdelta) (Pseq P Pdelta).

Theorem bisim_lmerge_act_seq :
  forall a v P Q,
  bisim (Plmerge (Pseq (Pact a v) P) Q) (Pseq (Pact a v) (Ppar P Q)).

Theorem bisim_assert :
  forall b1 b2,
  pcond_eval b1 = pcond_eval b2 ->
  bisim (Passert b1) (Passert b2).

Theorem bisim_cond_true :
  forall P, bisim (Pcond true P) P.

Theorem bisim_cond_false :
  forall P, bisim (Pcond false P) Pdelta.

Theorem bisim_cond_conj :
  forall b1 b2 P, bisim (Pcond b1 (Pcond b2 P)) (Pcond (b1 && b2) P).

Theorem bisim_sum_alt :
  forall f v, bisim (Psum f) (Palt (f v) (Psum f)).

Theorem bisim_sum_alt_distr :
  forall f g,
  bisim (Psum (fun v => Palt (f v) (g v))) (Palt (Psum f) (Psum g)).

Theorem bisim_sum_seq :
  forall f P, bisim (Pseq (Psum f) P) (Psum (fun v => Pseq (f v) P)).

Theorem bisim_sum_indep :
  forall P, bisim (Psum (fun v => P)) P.

Theorem bisim_sum_cond :
  forall b (f: Val -> Proc),
  bisim (Psum (fun v => Pcond b (f v))) (Pcond b (Psum f)).

Theorem bisim_iter_unroll :
  forall P, bisim (Piter P) (Palt (Pseq P (Piter P)) Pepsilon).

Lemma bisim_iter_seq_helper :
  forall P Q R,
  bisim (Pseq P (Piter (Palt Q R))) (Pseq (Pseq P (Piter Q)) (Piter (Pseq R (Piter Q)))).

Theorem bisim_iter_seq :
  forall P Q,
  bisim (Piter (Palt P Q)) (Pseq (Piter P) (Piter (Pseq Q (Piter P)))).

Theorem bisim_iter_delta :
  bisim (Piter Pdelta) Pepsilon.

Theorem bisim_iter_epsilon :
  bisim (Piter Pepsilon) Pepsilon.

Process safety

Any process P is defined to be safe with respect to any process store s, written psafe P s, if no fault can ever be reached from that configuration.

CoInductive psafe : Proc -> ProcStore -> Prop :=
  | proc_safe P s :
      
      (~ pfault P s) /\
      
      (forall l P' s', pstep P s l P' s' -> psafe P' s') ->
    psafe P s.

Process safety is closed under bisimilarity.

Lemma psafe_bisim :
  forall P Q s, bisim P Q -> psafe P s -> psafe Q s.
Add Parametric Morphism : psafe
  with signature bisim ==> eq ==> iff
    as psafe_eq_mor.

Other properties of process safety.

Lemma psafe_seq_l :
  forall P1 P2 s, psafe (Pseq P1 P2) s -> psafe P1 s.
Lemma psafe_seq_r :
  forall P1 P2 s, pterm P1 -> psafe (Pseq P1 P2) s -> psafe P2 s.

Lemma psafe_alt :
  forall P1 P2 s, psafe P1 s -> psafe P2 s -> psafe (Palt P1 P2) s.

Lemma psafe_alt_rev :
  forall P1 P2 s, psafe (Palt P1 P2) s -> psafe P1 s /\ psafe P2 s.

Lemma psafe_alt_l :
  forall P Q s, psafe (Palt P Q) s -> psafe P s.
Lemma psafe_alt_r :
  forall P Q s, psafe (Palt P Q) s -> psafe Q s.

Lemma psafe_delta :
  forall s, psafe Pdelta s.

Lemma psafe_epsilon :
  forall s, psafe Pepsilon s.

Lemma psafe_par_l :
  forall P1 P2 s, psafe (Ppar P1 P2) s -> psafe P1 s.
Lemma psafe_par_r :
  forall P1 P2 s, psafe (Ppar P1 P2) s -> psafe P2 s.

Lemma psafe_sum :
  forall f s,
    (forall v, psafe (f v) s) <->
  psafe (Psum f) s.

Lemma psafe_cond :
  forall P s, psafe (Pcond true P) s <-> psafe P s.

End Processes.