Semantics of CCS

Main definitions

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

inductive Cslib.CCS.Tr {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} : Process Name Constant → Act Name → Process Name Constant → Prop

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

• pre {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} {μ : Act Name} {p : Process Name Constant} : Tr (Process.pre μ p) μ p
• parL {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} {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 : Constant → Process Name Constant → Prop} {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 : Constant → Process Name Constant → Prop} {p : Process Name Constant} {μ : Act Name} {p' q : Process Name Constant} {μ' : Act Name} {q' : Process Name Constant} : μ.Co μ' → Tr p μ p' → Tr q μ' q' → Tr (p.par q) Act.τ (p'.par q')
• choiceL {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} {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 : Constant → Process Name Constant → Prop} {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 : Constant → Process Name Constant → Prop} {μ : 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 : Constant → Process Name Constant → Prop} {k : Constant} {p : Process Name Constant} {μ : Act Name} {p' : Process Name Constant} : defs k p → Tr p μ p' → Tr (Process.const k) μ p'

def Cslib.CCS.«term_[_]⭢_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cslib.CCS.«term_[_]↠_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

abbrev Cslib.CCS.lts {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} : LTS (Process Name Constant) (Act Name)

Equations

• Cslib.CCS.lts = { Tr := Cslib.CCS.Tr }

@[implicit_reducible]

instance Cslib.CCS.instHasTauAct {Name : Type u} : HasTau (Act Name)

Equations

• Cslib.CCS.instHasTauAct = { τ := Cslib.CCS.Act.τ }

inductive Cslib.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)