A monotone framework for CCS

The calculus of communicating systems, CCS, was introduced by Robin Milner as a calculus for modelling concurrent systems. Subsequently several techniques have been developed for analysing such models in order to get further insight into their dynamic behaviour. In this paper we present a static analysis for approximating the control structure embedded within the models. We formulate the analysis as an instance of a monotone framework and thus draw on techniques that often are associated with the efficient implementation of classical imperative programming languages. We show how to construct a finite automaton that faithfully captures the control structure of a CCS model. Each state in the automaton records a multiset of the enabled actions and appropriate transfer functions are developed for transforming one state into another. A classical worklist algorithm governs the overall construction of the automaton and its termination is ensured using techniques from abstract interpretation.