On Synthesis of Box Expressions from Petri Boxes (1996)

Author(s): M Hesketh

Abstact: The Petri Box Calculus consists of an algebra of Box expressions, and a corresponding algebra of Petri Boxes, which are classes of isomorphic labelled nets. A compositional semantic provides a translation from Box expressions to Petri Boxes. This paper describes an algorithm for synthesising a Box expression from a net which is a member of the class of Petri Boxes, for a basic subset of the calculus. The related problems of checking isomorphism of members of the class of Petri Boxes, and equivalence of Box expressions are also investigated. An analysis of the synthesis algorithm provides a complete axiomatisation of the fragment of the calculus under consideration.