View article

The comparison between Milner’s CCS and Petri nets leads to prove that CCS defines a subclass of the concurrent systems definable by means of net theory, i.e. the class of systems composed of interacting sequential automata. The proof is based on (the construction of) an isomorphism between Milner’s communicating systems class and a subclass of Petri nets.The paper fully presents the proof for a subclass of communicating systems (where neither value passing nor finite unlimited instances of agents are allowed) and a specific subclass of nets, the SA² _PT class (a restriction of the Superposed Automata nets class). Some hints how to extend the proof to the whole CCS conclude the paper. This result allows to transfer analytic concepts and techniques from a theory to the other, as for example the observation equivalence notion defined inside the CCS. The paper is fully self-consistent.