Abstract
A well known problem when reasoning about concurrent systems is that of state explosion. One of the strategies that has been proposed to alleviate this problem is to make use of the symmetries which a concurrent system may exhibit to construct a symmetry-reduced model that reflects the behaviour of the system. The main contribution of this thesis is an investigation into the theoretical foundations of the method by considering symmetries in the context of category theory. It seems natural to do so since the morphisms that characterise each category may be thought of as a kind of simulation of behaviour. A new category of language systems is presented, together with several subcategories. Morphisms in this category are defined to preserve structure. The notion of a symmetry of a language system is defined and the quotient structure of the language system is given. The important question of behaviour preservation between the system and its symmetry-reduced model is generalised to the notion of morphism in the category. The conditions required on the morphism to ensure that it preserves behaviour are identified. These results are extended to the projection morphism that define the symmetry-reduced model by constructing a split morphism. Two specific behaviours, namely absence of deadlock and extensibility, are considered. The second contribution of this thesis is to establish a categorical relationship between the language system model and elementary nets. A vector language semantics for elementary nets is given. Functors between these categories are defined and the existence of an adjunction is proved.