In: 92: University of Newcastle upon Tyne, Technical Report No. 384, 6. 1992.
Abstract: 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.