nLab transition system

Contents

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,Tran)T = (S,i,L,Tran), 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.

Remark

The term labelled transition system can also refer to the data of a domain, a set of labels and a transition relation, without any distinguished initial or final sets.

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.

See also

References

Discussion in relation to bisimulations and open morphisms:

Last revised on May 15, 2024 at 10:14:33. See the history of this page for a list of all contributions to it.