Skip to content

Labelled Transition Systems

A labelled transition system is a triple \((S,A,\to)\) where

  • \(S\) is a set of STATES
  • \(A\) is a set of LABELS (actions, operations or events)
  • \(\to\subseteq S\times A\times S\). (\(\to:S\to 2^{A\times S}\)) transition relation/

We have \(s\stackrel{a}\longrightarrow s'\), where \(a\) is observable information about what happens during the transition particularly heading to model communication/concurrency/distribution.

Example

An FSA, \(M=(Q,\Sigma,q_0,\delta,F)\) is a LTS:

\(LTS_M=(S\cup\{\cdot\},\sigma\cup\{\checkmark\},\to)\) where \(s\stackrel{a}\longrightarrow s'\) is equivalent to

  1. \(a\in\Sigma\) and \(s'\in\delta(s,a)\)
  2. \(a=\checkmark\) and \(s'=\cdot\) and \(s\in F\)

\(\mathcal L_M=\{a_1,\cdots,a_n\in\Sigma^*\vert\exists q_1,\cdots,q_n\vert q_0\stackrel{a_1}\rightarrow\cdots\stackrel{a_n}\rightarrow q_n\stackrel{\checkmark}\rightarrow\cdot\}\).

Communication-based Concurrency

A robotics scenario: Some mobile robots need to manage their energy in order to accomplish tasks.

  • When batteries deplete, robots look for a recharge.
  • Recharges are offered by recharge stations or other robots.

We can model the behaviors using an LTS capturing the observable features we are interested in.

Transition System Specifications

Literals

Fix a term algebra \(Term_{\Sigma,V}\) and a set of labels \(A\). A transition system specification on \(A\) is a set of inference rules: \(H\over\alpha\), where \(H\) is the finite set of literals and \(\alpha\) is positive literals.

  • Positive literal: \(t\stackrel{\alpha}\rightarrow t'\) or \(t\in T\)

  • Negative literal: \(t\not\stackrel{\alpha}\rightarrow\) or \(t\not\in T\)

where \(\alpha\in A,t\in Term_{\Sigma,V},T\subseteq Term_{\Sigma,V}\).

Operational Semantics of Regular Expressions

Note that

  • \(x\&y\) range over the set of regular expression
  • these rules from a TSS
  • each operator has a set of rules including \(0\) which has \(\emptyset\).

Basic Process algebra with \(a\in A\cup\{r\}\)

Act:

\[ a\in A\over a\stackrel{a}\longrightarrow 1 \]

Tic:

\[ \over 1\stackrel{\epsilon}\longrightarrow 1 \]

Seq 1:

\[ x\stackrel{a}\longrightarrow x'\ (x'\neq 1)\over x\cdot y\stackrel{a}\longrightarrow x'\cdot y \]

Seq 2:

\[ x\stackrel{a}\longrightarrow 1\over x\cdot y\stackrel{a}\longrightarrow y \]

Cho 1:

\[ x\stackrel{a}\longrightarrow x'\ (x\neq 1)\over x+y\stackrel{a}\longrightarrow x' \]

Cho 2:

\[ x\stackrel{a}\longrightarrow 1\over x+y\stackrel{a}\longrightarrow 1 \]

Cho 3:

\[ y\stackrel{a}\longrightarrow y'\ (x\neq 1)\over x+y\stackrel{a}\longrightarrow y' \]

Cho 4:

\[ y\stackrel{a}\longrightarrow 1\over x+y\stackrel{a}\longrightarrow 1 \]

Star 1:

\[ \over x^*\stackrel{\epsilon}\longrightarrow 1 \]

Star 2:

\[ x\stackrel{a}\longrightarrow x'\over x^*\stackrel{a}\longrightarrow x'\cdot x^* \]

LTSs as proofs of TSSs

A proof in a TSS \(\mathcal T\) of a closed transition rule \(H\over\alpha\) is an upwardly finitely branching tree whose

  • nodes are labelled by literals with the root labelled by \(\alpha\)
  • the leaves of the tree are the literals in \(H\)
  • If \(K\) is the set of children of \(\beta\) then there is \({H'\over\alpha'}\in T\) and \(\sigma:V\to Term_{\Sigma,\emptyset}\) s.t. \(K=H'\sigma\) and \(\beta=\alpha'\sigma\).

\(H\) provable in \(\mathcal T\), written \(\mathcal T\vdash {H\over\alpha}\), if there is a proof of \(H\over\alpha\) in \(\mathcal T\).

Example

Fix the alphabet \(V=\{e,c,t,cl\}\)

\[ {{{e\in V\over e\stackrel{e}\longrightarrow 1}\over e\cdot c\stackrel{e}\longrightarrow c\ (c\neq 1)}\over e\cdot c+e\cdot t\stackrel{e}\longrightarrow c\ (c\neq 1)}\over(e\cdot c+e\cdot t)\cdot cl\stackrel{e}\longrightarrow c\cdot cl\text{ or } t\cdot cl\stackrel{c\text{ or }t}\longrightarrow cl\stackrel{cl}\longrightarrow 1 \]

Regular Expressions and Their Operational Semantics

We saw that we can define the language of an FSA \(M=(Q,\Sigma,q_0,S,F)\) as

\(\mathcal L_M=\{a_1,\cdots,a_n\in\Sigma^*\vert\exists q_1,\cdots,q_n\vert q_0\stackrel{a_1}\rightarrow\cdots\stackrel{a_n}\rightarrow q_n\stackrel{\checkmark}\rightarrow\cdot\}\)

where \(\to\) is the relation of the LTS corresponding to \(M\)

This can be generalized to any LTS.