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 compo- sitional semantics provides a translation from box expressions to boxes. The synthesis problem is to provide an algorithmic translation from boxes to box expressions. The axiomatisation 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 con- current 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 gener- ating 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.

The main theme of this thesis is to study the isometric algebra isomorphisms and the bipositive algebra isomorphisms between various Banach algebras associated with locally compact groups. Let $LUC(G)$ denote the $C^*$-algebra of left uniformly continuous functions with the uniform norm and let $C_0(G)^{\perp}$ denote the annihilator of $C_0(G)$ in $LUC(G)^*$. In Chapter 2 of this thesis, among other results, we show that if $G$ is a locally compact group and $H$ is a discrete group then whenever there exists a weak-star continuous isometric isomorphism between $C_0(G)^{\perp}$ and $C_0(H)^{\perp}$, $G$ is isomorphic to $H$ as a topological group. In particular, when $H$ is discrete $C_0(H)^{\perp}$ determines $H$ within the class of locally compact topological groups. In Chapter 3 of this thesis, we show that if $M(G,\omega_1)$ (the weighted measure algebra on $G$) is isometrically algebra isomorphic to $M(H,\omega_2)$, then the underlying weighted groups are isomorphic, i.e. there exists an isomorphism of topological groups $\phi:G\to H$ such that $\small{\displaystyle{\frac{\omega_1}{\omega_2\circ\phi}}}$ is multiplicative. Similarly, we show that any weighted locally compact group $(G,\omega)$ is completely determined by its Beurling group algebra $L^1(G,\omega)$, $LUC(G,\omega^{-1})^*$ and $L^1(G,\omega)^{**}$, when the two last algebras are equipped with an Arens product. Here, $LUC(G,\omega^{-1})$ is the weighted analogue of $LUC(G)$, for weighted locally compact groups. In Chapter 4 of this thesis, we show that the order structure combined with the algebra structure of each of the Banach algebras $L^1(G,\omega)$, $M(G,\omega)$, $LUC(G,\omega^{-1})^*$ and $L^1(G,\omega)^{**}$ completely determines the underlying topological group structure together with a constraint on the weight. In particular, we obtain new proofs for a previously known result of Kawada and results of Farhadi as special cases of our results. Finally, we provide an example of a bipositive algebra isomorphism between Beurling measure algebras that is not an isometry. We conclude this thesis with a selective list of open problems. / February 2016