A compositional proof system on a category of labelled transition systems (Q2640340)

This paper is a contribution to the effort to formulate both syntactical and semantical notions of concurrency in category-theoretic language in order to be able to compare different models of concurrency. A category of labelled transition systems is introduced, and various constructions, such as products, coproducts, are described. The notion of a fibration functor p: \(X\to B\) is shown to be a useful one, as it plays a central role in the considerations here. The full subcategory of synchronization trees is shown to be coreflective - i.e. the inclusion functor has a right adjoint. Associated with any fixed transition system is a language of modal assertions, including a least fixed point construct. The meaning of an assertion is the set of reachable states which satisfy it. A logical category, Prop, has as objects pairs U:T where U is a ``property'', a certain kind of subset of the reachable states of the transition system T; a morphism \(U:T\to U':T'\) is a morphism f: \(T\to T'\) such that the f image of each state in U belongs to U'. A system of terms that denote labelled transition systems is introduced. Each term denotes a particular transition system, which has an associated set of modal assertions. A rather long set of rules to derive valid assertions is introduced and shown to be sound and complete. As the author frankly admits, this study is not the final word on compositional proof systems. There is a noneffective element in the reduction of statements about a product to statements about the components; general recursion has not been included; the categorical status of restriction or hiding is not well understood. Nevertheless, this paper is an interesting contribution to the stated goal. There are several minor misprints and at least one major one: the definition of the morphisms of the category X at the top of page 34 should read: v: \(U\to F(f)(U')\), not v: \(U\to F(U')\).