R.P. Hopkins
University of Newcastle upon Tyne. 1992
We define a class of modular Petri nets, referred to as Petri Boxes, together with some box composition operations, which have been specifically developed to give compositional Petri net semantics of a process algebra having synchronous communication between concurrent processes, prioritised choice and multi-action communication, i.e. a process being able to atomically engage in a (multi-)set of observable actions which can give a single synchronisation with a number of other concurrent processes. As a case study we define a "voter", for use in TMR systems; and some general properties of the composition operations are used to prove that if the voter is composed with three given processes of which two exhibit equivalent "correct" behaviour, then so does the overall construction. In this framework the construction accommodates a kind of non-determinism in the correct given processes which could not be accommodated without multi-action communication.