Deducing causal relationships in CCS

Abstract

We introduce purely parallel processes, a class of finite CCS processes defined by a restricted syntax which allows synchronization but forbids choice. Such processes are deterministic in the sense of Milner [7]. We define a function which associates to each purely parallel process a labelled partially ordered set which is also deterministic but in the sense of Vaandrager, [10]. Our main result is that this induces a bijection from equivalence classes of purely parallel processes, under weak bisimulation, to finite deterministic pomsets. The motivation for this work comes from practical problems in verification and we give two applications of our results.