Synthesis of Box Expressions from Petri Boxes

摘要

The Petri Box Calculus consists of an algebra of Box expressions, and acorresponding algebra of Petri Boxes, which are classes of isomorphic labelled nets. A compositional semantic provides a translation from Box expressions to Petri Boxes. The paper describes an algorithm for synthesizing 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 axiomatization of the fragment of the calculs under consideration. (Copyright (c) 1996 University of Newcastle upon Tyne.)