Defining Partial Orders on Graphical Models of Concurrent Systems

Our interest is in models of concurrency, and their theoretical axiomatisation and analysis. We build on a rich thread of research [BSZ14, FSR16, BSZ17a] interpreting models such as Petri nets as so-called string diagrams, a notation for morphisms of symmetric monoidal categories. From there, we can use structure-preserving mappings between the model and a semantic domain. The main contribution of the thesis is the definition of a symmetric monoidal inequality theory, which extends the standard tool used in this field to handle inequalities. Armed with this, we answer more questions about systems than just whether they have the same behaviours, such as describing specifications which leave open ambiguity or choices for implementors, proofs that systems satisfy such a specification (or not), and demonstrations that one system exhibits some (but not necessarily all) behaviours of another