A compositional partial order semantics for petri net components

Abstract

In this paper we introduce the concept of a Petri net component and show how systems can be composed from components. A component communicates with its environment via distinguished input and output places, which formalizes communication by message passing; Then, we present a compositional semantics for components. The semantics is an extension of processes for place/transition systems (partial order semantics). We show that the semantics is fully abstract with respect to the behaviour of closed components (essentially, processes of place/transition systems). A main feature of the compositional semantics is that composition of components corresponds to conjunction. This feature makes the compositional semantics applicable in combination with a temporal logic, which then allows to reason about systems in a compositional way. This is demonstrated by help of a simple temporal logic.