nLab
transition system

Contents

Transition systems.

Transition systems are a well established semantic model for both sequential and concurrent systems.

Definition

A transition system is a structure T=(S,i,L,Trans)T = (S,i,L,Trans), where

  • SS is a set of states with initial state, ii;

  • LL is a set of labels, sometimes referred to also as events;

  • TranS×L×STran\subseteq S\times L\times S is the transition relation.

Let (S,i,L,Tran)(S, i, L, Tran ) be a transition system. We write

sass\stackrel{a}{\to} s'

to indicate that (s,a,s)Tran(s, a, s')\in Tran.

Definition

A morphism from one transition system, TT, to another TT' will be a pair (σ,λ)(\sigma, \lambda), in which

  • σ\sigma is a function from the states of TT to those of TT'

  • λ\lambda is a partial function from the labels of TT to those of TT' such that for any transition sass\stackrel{a}{\to} s' of TT if λ(a)\lambda(a) is defined, then σ(s)λ(a)σ(s)\sigma(s)\stackrel{\lambda(a)}{\to} \sigma(s') is a transition of TT'; otherwise, if λ(a)\lambda(a) is undefined, then σ(s)=σ(s)\sigma(s) = \sigma(s').

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 \bot to the codomain. (We will use the notation from partial function freely in what follows.) This is done here simply by introducing idle transitions (s,,s)(s,\bot,s) thought of as going from ss to itself, and working with L L_\bot as a set of labels instead of LL. (This is very neat here as it corresponds the label \bot to ‘do nothing’ to the states.) After completing everything in this way we get new transition systems T =(S,i,L ,Tran )T_\bot = (S,i,L_\bot, Tran_\bot), etc. and will work with these. (Of course, Tran =Tran{s,,s)sS}Tran_\bot = Tran \cup \{s,\bot,s)\mid s\in S\}.) Now a morphism ff is the same as given by a pair σ:SS\sigma: S\to S', as before, and λ:L L \lambda: L_\bot\to L'_\bot, satisfying the compatibility condition that if (s,a,s)Tran (s,a,s')\in Tran_\bot, then (σ(s),λ(a),σ(s))Tran (\sigma(s),\lambda(a),\sigma(s'))\in Tran'_\bot, (and that λ ()=\lambda_\bot(\bot) = \bot').

This way we get a category, TSTS, 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.

Labeled transition systems.

In the above, we have used the notation LL 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 LL by EE and refer to its elements as ‘events’ in what follows.

Definition

A labelled transition system consists of a transition system T=(S,i,E,Tran)T = (S, i, E, Tran) together with a set LL of labels, and a function l:ELl : E \to L. We denote it by (T,L,l)(T,L,l).

A morphism, (σ,τ,λ):(T 1,L 1,l 1)(T 2,L 2,l 2)(\sigma, \tau , \lambda) : (T_1 , L_1 , l_1) \to (T_2 , L_2 , l_2 ) between labeled transition systems consists of a morphism (σ,τ):T 1T 2(\sigma, \tau) : T_1 \to T_2 between the underlying transition systems together with a partial function λ:L 1L 2\lambda : L_1 \to L_2 such that l 2τ=λl 1l_2 \circ \tau = \lambda \circ l_1.

We write LTSLTS for the category of labeled transition systems.

TSs as relational structures

We can view a transition system as a relational structure. The set of states is the ‘set of worlds’ and for each event, eEe \in E we define a relation R eS×SR_e \subseteq S\times S by (s,s)R e(s,s')\in R_e if and only if, (s,e,s)Trans(s,e,s')\in Trans. We thus derive a relation for each event and, conversely, if we know the family {R eeE}\{R_e \mid e\in E\}, then we can rebuild TransTrans in the obvious way.

Higher dimensional analogues

There are tentative definitions of

higher dimensional transition system,

which take a more nPOV of this theory.

References

category: computer science

Revised on September 8, 2012 13:37:00 by Tim Porter (95.147.236.244)