Abstract:
The overall intention of this work is to investigate the ability to regard a finite computation as a single event, in dealing with the semantics of concurrency. We propose a calculus of concurrent processes that embodies this ability in two respects: the first one is that of execution, the second that of operation. As usual, we formalize the execution of a process as a labelled transition relation. But our point is that at each step the performed action is a compound one, namely a labelled poset, not just an atom. The action reflects the causal and concurrent structure of the process, and we claim that the bisimulation relative to such transition systems brings out a clear distinction between concurrency and sequential non-determinism. Next we introduce a second transition relation, formalizing the operation of a process on data. As in the usual semantics of sequential programs, a process operates on data by means of its terminated sequences of computations. Then we obtain atomic actions by abstracting the whole operation of a process as a single event. We show that this abstraction mechanism, together with the idea of compound actions, allows us to deal with a variety of synchronization and communication discipline.