A compositional proof system on a category of labelled transition systems

AbstractThis paper presents an attempt to cast labelled transition systems, and other models of parallel computation, in a category-theoretic framework. One aim is to use category theory to provide abstract characterisations of constructions like parallel composition valid throughout a range of different models and to provide formal means for translating between different models. Another aim is to exploit the framework of categorical logic to systematise specification languages and the derivation of proof systems for parallel processes. After a category of labelled transition systems is presented, its categorical constructions are used to establish a compositional proof system. A category of properties of transition systems indexed by the category of labelled transition systems is used in forming the proof system