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 → Option (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 : Constant → Option (Process Name Constant)} {μ : Act Name} {p : Process Name Constant} : Tr (Process.pre μ p) μ p
• parL {Name : Type u} {Constant : Type v} {defs : Constant → Option (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 : Constant → Option (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 : Constant → Option (Process Name Constant)} {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 → Option (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 : Constant → Option (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 : Constant → Option (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 : Constant → Option (Process Name Constant)} {k : Constant} {p : Process Name Constant} {μ : Act Name} {p' : Process Name Constant} : defs k = some 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 → Option (Process Name Constant)} : LTS (Process Name Constant) (Act Name)

Equations

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

@[instance_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)

theorem Cslib.CCS.not_tr_of_terminated {Name : Type u} {Constant : Type v} {defs : Constant → Option (Process Name Constant)} {p : Process Name Constant} {μ : Act Name} {p' : Process Name Constant} (h : Terminated p) : ¬lts.Tr p μ p'

A terminated process has no outgoing transitions.

theorem Cslib.CCS.pre_tr {Name : Type u} {Constant : Type v} {defs : Constant → Option (Process Name Constant)} {μ : Act Name} {p : Process Name Constant} {μ' : Act Name} {p' : Process Name Constant} (h : lts.Tr (Process.pre μ p) μ' p') : μ = μ' ∧ p = p'

Inversion lemma for prefix transitions.

theorem Cslib.CCS.const_tr {Name : Type u} {Constant : Type v} {defs : Constant → Option (Process Name Constant)} {k : Constant} {μ : Act Name} {p' : Process Name Constant} (h : lts.Tr (Process.const k) μ p') : ∃ (p : Process Name Constant), defs k = some p ∧ lts.Tr p μ p'

Inversion lemma for constant transitions.

theorem Cslib.CCS.pre_deterministicState {Name : Type u} {Constant : Type v} {defs : Constant → Option (Process Name Constant)} {μ : Act Name} {p : Process Name Constant} : lts.DeterministicState (Process.pre μ p)

Prefixes are deterministic.

theorem Cslib.CCS.const_deterministicStateLabel {Name : Type u} {Constant : Type v} {defs : Constant → Option (Process Name Constant)} {k : Constant} {p : Process Name Constant} {μ : Act Name} (hdef : defs k = some p) (h : lts.DeterministicStateLabel p μ) : lts.DeterministicStateLabel (Process.const k) μ

Constants are deterministic if their definition is deterministic.

theorem Cslib.CCS.res_deterministicStateLabel {Name : Type u} {Constant : Type v} {defs : Constant → Option (Process Name Constant)} {p : Process Name Constant} {μ : Act Name} {μ' : Name} (h : lts.DeterministicStateLabel p μ) : lts.DeterministicStateLabel (Process.res μ' p) μ

Restriction is deterministic if its subterm is deterministic.