The Modelling and Analysis of Security Protocols: the CSP Approach

4.2. Labelled Transition Systems

The classic operational representation of a CSP process is as a Labelled Transition System (LTS) [75]: a set of nodes representing the states of the process are connected by directed arcs, labelled with either a visible event or the internal action Τ, which describe how one state can evolve into another. There is a structured operational semantics for CSP [14] and more particularly for CSP_M [83], which allow these arcs to be deduced between nodes representing process terms – or rather closures, terms together with bindings for their free identifiers – and this operational semantics forms the basis of the compilation strategy for purely sequential or recursive terms. One of the components of the FDR tool is a ...