Process algebras are mathematical languages for describing and analysing the behaviour of concurrent systems. The operational semantics of a process algebra is commonly represented as a labelled transition system (LTS). Unfortunately, labelled transition systems focus on immediate state changes and thus fail to cover the concurrency relation between transitions, which is crucial for the notion of justness, arguably the minimal fairness assumption required for the verification of liveness properties. A synchron represents a path in the parse tree of a process algebra expression. Each transition in the process algebra-stemmed LTS can be understood as the synchronisation of a number of synchrons. Under this interpretation, we can then derive the conventional relation between transitions from that between synchrons.

This talk will use the process algebra CCS as an example to introduce the concept of synchrons. We then demonstrate how to derive concurrency relation between transitions. If time permits, we will discuss an extension of the synchron framework exploring the relation between paths. This extension could be useful for justness-preserving alternatives of weak bisimulation, etc.