About Open Access
[PhD Thesis] Synthesis and Axiomatisation for Structural Equivalences in the Petri Box calculus
Lookup NU author(s)
Full text is not currently available for this publication.
The Petri Box Calculus (PBC) consists of an algebra of box expressions, and a corresponding algebra of boxes (a class of labelled Petri nets). A compositional semantics provides a translation from box expressions to boxes. The synthesis problem is to provide an algorithmic translation from boxes to box expressions. The aniomatisation problem is to provide a sound and complete axiomatisation for the fragment of the calculus under consideration, which captures a particular notion of equivalence for boxes. There are several alternative ways of defining an equivalence notion for boxes, the strongest one being net isomorphism. In this thesis, the synthesis and axiomatisation problems are investigated for net semantic isomorphism, and a slightly weaker notion of equivalence, called duplication equivalence, which can still be argued to capture a very close structural similarity of concurrent systems the boxes are supposed to represent. In this thesis, a structured approach to developing a synthesis algorithm is proposed, and it is shown how this may be used to provide a framework for the production of a sound and complete axiomatisation. This method is used for several different fragments of the Petri Box Calculus, and for generation axiomatisations for both isomorphism and duplication equivalence. In addition, the algorithmic problems of checking equivalence of boxes and box expressions, and generating proofs of equivalence are considered as extensions to the synthesis algorithm.
Department of Computing Science, University of Newcastle upon Tyne
Newcastle upon Tyne
British Lending Library DSC stock location number: DXN023004
Newcastle University Library, NE2 4HQ, United Kingdom. Tel: 0044 (191) 222 7657
©2014 Newcastle University Library