Transition systems are a well established semantic model for both sequential and concurrent systems.
A transition system is a structure , where
is a set of states with initial state, ;
is a set of labels, sometimes referred to also as events;
is the transition relation.
Let be a transition system. We write
to indicate that .
A morphism from one transition system, , to another will be a pair , in which
is a function from the states of to those of
is a partial function from the labels of to those of such that for any transition of if is defined, then is a transition of ; otherwise, if is undefined, then .
It is useful to rework this definition of morphism using a variant of the idea, discussed at partial function, that replaces a partial function by a total function using the neat trick of adding an additional element to the codomain. (We will use the notation from partial function freely in what follows.) This is done here simply by introducing idle transitions thought of as going from to itself, and working with as a set of labels instead of . (This is very neat here as it corresponds the label to ‘do nothing’ to the states.) After completing everything in this way we get new transition systems , etc. and will work with these. (Of course, .) Now a morphism is the same as given by a pair , as before, and , satisfying the compatibility condition that if , then , (and that ).
This way we get a category, , of transition systems.
The notions of transition system and of morphisms between them is clearly related to (low dimensional) cubical sets / labelled directed graphs/labelled transition systems, but we will need to consider labelled cubical sets.
In the above, we have used the notation to stand for the set of events and the set of labels for those events. It is sometimes useful to make a distinction between the events themselves and their labels and to explicitly give a labelling as a function. This is important, for instance, in treating ‘relabelling’ which leads to categorical fibrational situations (see the paper by Winskel and Nielsen, cited below.) In order to make the distinction clearer, we will replace by and refer to its elements as ‘events’ in what follows.
A labelled transition system consists of a transition system together with a set of labels, and a function . We denote it by .
A morphism, between labeled transition systems consists of a morphism between the underlying transition systems together with a partial function such that .
We write for the category of labeled transition systems.
We can view a transition system as a relational structure. The set of states is the ‘set of worlds’ and for each event, we define a relation by if and only if, . We thus derive a relation for each event and, conversely, if we know the family , then we can rebuild in the obvious way.
There are tentative definitions of
which take a more nPOV of this theory.
G. Winskel and M. Nielsen, Models for concurrency. vol. 3, Handbook of Logic in Computer Science, pages 100 - 200, Oxford Univ. Press, 1994. (see also online technical report).