Hoofdstuk 11:
11.1 Labelled Transition Systems
A light can be either on or off. There is a switch that can be used to turn the light on
(if it is off) and turn the light off (if it is on). We can visualise this as follows. The lights
has 2 possible states, either On or Off. Mostly capital letters are used for states, the
On or Off state. Non capital are used for actions, the on or off action that trigger an transition from
one state to another.
A little more complicated to model is a vending machine. A simple vending machine
can dispense coffee or tea for 1 euro. There are two possible states:
− 0, no coin inserted
− 1, a coin has been inserted a drink may be selected.
There can be more than one action between different states.
Each of these examples are instances of a labelled transition system, a simple way to model a
computational process that can be in different states and shift between these states. More formally,
a labelled transition system consists of:
− A set States – corresponding to all the possible states of the system (like On or 1);
− A set Actions – corresponding to the labels between states;
− A relation on States × Actions × States corresponding to the possible transitions from one
𝑎
state to the next. We usually write 𝑠1 → 𝑠2 when this relation includes (s1, a, s2), or put
differently we can transition from state s1 to s2 by performing the action a.
Labelled transition system of the vending machine:
− States: {0, 1}
− Actions: {coin, coffee, tea}
− Transitions: {(0, coin, 1),(1, coffee, 0),(1, tea, 0)}
𝑎
We will write 𝑠1 → 𝑠2 when we can transition from s1 to s2 by the action a. When we cannot
transition from s1 to s2 with the action a, we sometimes write:
When there are no actions that transition from s1 to s2, we will write:
When there are no transitions from s to any other state, we will write:
We can easily extend our transition relation to work over lists of actions, rather than a single action.
This is useful to model a sequence of transition steps, rather than a single step, usually written 𝑠
𝑤
→ 𝑠′ , where w ∈ Action∗:
, ε
− 𝑠 → 𝑠, if there are no further actions to be taken, we stay at the state s.
aw a w
− 𝑠 → 𝑡, if 𝑠 → 𝑠′, ′and 𝑠′ → 𝑡, for some state s ′ , if we can take a single step from s to s ′
along a, and continue from s ′ to t by the word w, we can transition from s to t by aw.
A man needs to cross a river with a wolf, a goat, and a cabbage. His boat is only large enough to
carry himself and one of his three possessions, so he must transport them one at a time. However, if
he leaves the wolf and the goat together unattended, then the wolf will eat the goat; similarly, if he
leaves the goat and the cabbage together unattended, the goat will eat the cabbage. How can the
man get across safely with his possessions? We can model this problem as a labelled transition
system.
We want to model where the man, wolf, goat and cabbage are. Each can be on one side of the river,
but not both at the same time. We can model this by taking P({M, W, G,
C}) as our set of states. At a given state S, the elements of S have
successfully crossed the river. Initially, no one has crossed the river –
hence we are at the state ∅.
There are four possible actions: {m, g, c, w} corresponding to crossing
the river with the an empty boat (m), the goat (g), the cabbage (c), or
the wolf (w). The transitions each move the man (and possibly one of his
g
possessions) to the other side of the river. For example, MGC ≀≀≀ W →C
≀≀≀ MWG Finally, some states are ‘dangerous’ – when the wolf and goat
are unattended on one side of the river or the goat and cabbage are
unattended on one side of the river. On the right is the is the LTS of the
whole story.
11.3 A language for describing processes
Drawing smaller processes is fine but we would never draw the labelled transition system for even
moderately-complex processes. We need a proper language for describing bigger and more
complicated systems. A formal description language can also be programmed and analysed on a
machine. In this language we will have variables, such as Off, On, and Broken. We will also have
events or actions, such as pull, break and reset.
The zero process has one state, but no actions or transitions. We typically write 0 to
denote this ‘empty’ process.
11.1 Labelled Transition Systems
A light can be either on or off. There is a switch that can be used to turn the light on
(if it is off) and turn the light off (if it is on). We can visualise this as follows. The lights
has 2 possible states, either On or Off. Mostly capital letters are used for states, the
On or Off state. Non capital are used for actions, the on or off action that trigger an transition from
one state to another.
A little more complicated to model is a vending machine. A simple vending machine
can dispense coffee or tea for 1 euro. There are two possible states:
− 0, no coin inserted
− 1, a coin has been inserted a drink may be selected.
There can be more than one action between different states.
Each of these examples are instances of a labelled transition system, a simple way to model a
computational process that can be in different states and shift between these states. More formally,
a labelled transition system consists of:
− A set States – corresponding to all the possible states of the system (like On or 1);
− A set Actions – corresponding to the labels between states;
− A relation on States × Actions × States corresponding to the possible transitions from one
𝑎
state to the next. We usually write 𝑠1 → 𝑠2 when this relation includes (s1, a, s2), or put
differently we can transition from state s1 to s2 by performing the action a.
Labelled transition system of the vending machine:
− States: {0, 1}
− Actions: {coin, coffee, tea}
− Transitions: {(0, coin, 1),(1, coffee, 0),(1, tea, 0)}
𝑎
We will write 𝑠1 → 𝑠2 when we can transition from s1 to s2 by the action a. When we cannot
transition from s1 to s2 with the action a, we sometimes write:
When there are no actions that transition from s1 to s2, we will write:
When there are no transitions from s to any other state, we will write:
We can easily extend our transition relation to work over lists of actions, rather than a single action.
This is useful to model a sequence of transition steps, rather than a single step, usually written 𝑠
𝑤
→ 𝑠′ , where w ∈ Action∗:
, ε
− 𝑠 → 𝑠, if there are no further actions to be taken, we stay at the state s.
aw a w
− 𝑠 → 𝑡, if 𝑠 → 𝑠′, ′and 𝑠′ → 𝑡, for some state s ′ , if we can take a single step from s to s ′
along a, and continue from s ′ to t by the word w, we can transition from s to t by aw.
A man needs to cross a river with a wolf, a goat, and a cabbage. His boat is only large enough to
carry himself and one of his three possessions, so he must transport them one at a time. However, if
he leaves the wolf and the goat together unattended, then the wolf will eat the goat; similarly, if he
leaves the goat and the cabbage together unattended, the goat will eat the cabbage. How can the
man get across safely with his possessions? We can model this problem as a labelled transition
system.
We want to model where the man, wolf, goat and cabbage are. Each can be on one side of the river,
but not both at the same time. We can model this by taking P({M, W, G,
C}) as our set of states. At a given state S, the elements of S have
successfully crossed the river. Initially, no one has crossed the river –
hence we are at the state ∅.
There are four possible actions: {m, g, c, w} corresponding to crossing
the river with the an empty boat (m), the goat (g), the cabbage (c), or
the wolf (w). The transitions each move the man (and possibly one of his
g
possessions) to the other side of the river. For example, MGC ≀≀≀ W →C
≀≀≀ MWG Finally, some states are ‘dangerous’ – when the wolf and goat
are unattended on one side of the river or the goat and cabbage are
unattended on one side of the river. On the right is the is the LTS of the
whole story.
11.3 A language for describing processes
Drawing smaller processes is fine but we would never draw the labelled transition system for even
moderately-complex processes. We need a proper language for describing bigger and more
complicated systems. A formal description language can also be programmed and analysed on a
machine. In this language we will have variables, such as Off, On, and Broken. We will also have
events or actions, such as pull, break and reset.
The zero process has one state, but no actions or transitions. We typically write 0 to
denote this ‘empty’ process.
