CCS formalisation

Stream: general

[Bashar Hamade]

Has there been already work done for formalizing Calculus of Communicating Systems in Lean?
Particularly I would be interested in formalising the following:
-Definition of Labelled transitions systems (LTS) and successor states
-Reachability in LTS
-Nondeterminsm (internal and external)
-Syntax,Semantics and inference rules in CCS
-Equivalence Relations(Strong and weak bisimulation,observation congruence,trace equivalence...)

Mainly focusing on the last point

[Yaël Dillies]

I would like to formalise Chandra-Furst-Lipton (I am interested in additive combinatorics), but I don't I will need much CCS machinery at all.

[Marcus Rossel]

I have a repo for CCS (which I abandoned along the way) here: https://github.com/marcusrossel/lean-ccs It should at least cover the syntax and semantics of CCS. However, I tried and failed to define a reduction from a CCS expression to an equivalent LTS.