Logic for Computer Science/Logic for Computer Technology Chapter 11 Summary of the book Modelling Computing Systems written by Faron Moller and Georg Struth. Summary written in English. Using examples and pictures, the substance and theory are clarified. Given at Utrecht University.
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:
𝑎
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.
The benefits of buying summaries with Stuvia:
Guaranteed quality through customer reviews
Stuvia customers have reviewed more than 700,000 summaries. This how you know that you are buying the best documents.
Quick and easy check-out
You can quickly pay through credit card or Stuvia-credit for the summaries. There is no membership needed.
Focus on what matters
Your fellow students write the study notes themselves, which is why the documents are always reliable and up-to-date. This ensures you quickly get to the core!
Frequently asked questions
What do I get when I buy this document?
You get a PDF, available immediately after your purchase. The purchased document is accessible anytime, anywhere and indefinitely through your profile.
Satisfaction guarantee: how does it work?
Our satisfaction guarantee ensures that you always find a study document that suits you well. You fill out a form, and our customer service team takes care of the rest.
Who am I buying these notes from?
Stuvia is a marketplace, so you are not buying this document from us, but from seller luukvaa. Stuvia facilitates payment to the seller.
Will I be stuck with a subscription?
No, you only buy these notes for $3.21. You're not tied to anything after your purchase.
