Semantics of CCS

Main definitions

• CCS.tr: transition relation for CCS.
• CCS.lts: the LTS of CCS.

inductive CCS.tr {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} : Process Name Constant → Act Name → Process Name Constant → Prop

The transition relation for CCS. This is a direct formalisation of the one found in [San].

• pre {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {μ : Act Name} {p : Process Name Constant} : tr (Process.pre μ p) μ p
• parL {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {p : Process Name Constant} {μ : Act Name} {p' q : Process Name Constant} : tr p μ p' → tr (p.par q) μ (p'.par q)
• parR {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {q : Process Name Constant} {μ : Act Name} {q' p : Process Name Constant} : tr q μ q' → tr (p.par q) μ (p.par q')
• com {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {p : Process Name Constant} {μ : Act Name} {p' q q' : Process Name Constant} : tr p μ p' → tr q (Act.co Name μ) q' → tr (p.par q) Act.τ (p'.par q')
• choiceL {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {p : Process Name Constant} {μ : Act Name} {p' q : Process Name Constant} : tr p μ p' → tr (p.choice q) μ p'
• choiceR {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {q : Process Name Constant} {μ : Act Name} {q' p : Process Name Constant} : tr q μ q' → tr (p.choice q) μ q'
• res {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {μ : Act Name} {a : Name} {p p' : Process Name Constant} : μ ≠ Act.name a → μ ≠ Act.coname a → tr p μ p' → tr (Process.res a p) μ (Process.res a p')
• const {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {k : Constant} {p : Process Name Constant} {μ : Act Name} {p' : Process Name Constant} : defs k p → tr p μ p' → tr (Process.const k) μ p'

def CCS.lts {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} : LTS (Process Name Constant) (Act Name)

The LTS of CCS.

Equations

• CCS.lts = { tr := CCS.tr }

inductive CCS.Terminated {Name : Type u} {Constant : Type v} : Process Name Constant → Prop

A process is (successfully) terminated if it is a composition of nils.

• nil {Name : Type u} {Constant : Type v} : Terminated Process.nil
• par {Name : Type u} {Constant : Type v} {p q : Process Name Constant} : Terminated p → Terminated q → Terminated (p.par q)
• choice {Name : Type u} {Constant : Type v} {p q : Process Name Constant} : Terminated p → Terminated q → Terminated (p.choice q)
• res {Name : Type u} {Constant : Type v} {p : Process Name Constant} {a : Name} : Terminated p → Terminated (Process.res a p)