Open AccessA Compositional Proof System on a Category of Labelled Transition Systems
Author(s) -
Glynn Winskel
Publication year - 1989
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v18i294.6688
Subject(s) - categorical variable , category theory , transition (genetics) , computation , computer science , exploit , theoretical computer science , transition system , mathematics , proof theory , algorithm , pure mathematics , machine learning , mathematical proof , chemistry , biochemistry , geometry , computer security , gene
This 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 presenting a category of labelled transition systems, 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 forrning the proof system.