on June 19, 2006
- Consider the following problem:
Six soldiers who are heavily injured,
try to flee to their home land. The enemy is chasing them and in
the middle of the night they arrive at a bridge that spans a river
which is the border between the two countries at war. The bridge
has been damaged and can only carry two soldiers at a time.
Furthermore, several land-mines have been placed on the bridge and a
torch is needed to sidestep all the mines. The enemy is on their
trail, so the soldiers know that they have only 2 hours to cross the
bridge. The soldiers only have a single torch and they are not
equally injured. The following table lists the crossing times
(one-way!) for each of the soldiers:
soldier S0 5 minutes
soldier S1 10 minutes
soldier S2 20 minutes
soldier S3 25 minutes
soldier S4 30 minutes
soldier S5 35 minutes
Does a schedule exist which gets all six soldiers to the safe side
within 120 minutes?
(Ruys & Brinksma 1998)
In essence, this is a scheduling/planning problem, and we can take
advantage of the fact that a model-checker explores all possible orders
of interleavings. Thus, we can easily have the model-checker construct
all the different orderings for moving soldiers across the bridge.
We would like to get SPIN to generate a trace for us that illustrates a
schedule where the soldiers can get from the unsafe to the safe side in
120 minutes or less. SPIN generates counter-example or
property-violation traces. Therefore, we need to ask SPIN to try
to prove that a schedule does not exist. If it finds a
counterexample, it will illustrate a schedule that is a solution to the
Using Linear Temporal Logic, we can formalize the desired property
directly. One can also get SPIN to generate an appropriate trace using
You have to build a Promela model
to solve this problem and generate a trace illustrating some "good"
- Consider two transition systems:
that true that
- the systems are trace equivalent?
- T1 <= T2?
- T2 <= T1?
- T1 is bisimilar to T2?
why yes or why not.
- Read chapter 11 (pp. 109-123) in B. Berard et al. "Systems and
- Abstract the timer at the
sender side in your Promela model of PAR, check how the abstract
version of the protocol works for several timer settings.
- Use the model you built for
problem 4 and redefine the environment by using data independence;
formulate the correctness property first in the textual form, then
formalise it; check the property with Spin for several "good" timer
settings. Interpret the results in a natural language.
- In this exercise we consider a
list abstraction that can be
for the verification of protocols that sends packages of messages that
we model as lists of natural numbers.We use data independence and
abstract natural numbers p1, p2 into e1, e2 respectively, while all the
other naturals are non-distinguishable and they are abstracted into an
abstract element ne. Now we
want to abstract lists of non-repeating naturals numbers. An arbitrary
list of naturals is represented by
- its abstracted head
abstract representation of the whole list, which is of the form epsl, e1l, e2l, e1e2l, e2e1l, error, and, furthermore,
information whether it is an empty or a one-element list.
is an abstraction for an
"incorrect" list, i.e. a list with duplicated elements (the assumption
is that only lists of non-repeating naturals are sent, but one need to
assure that no repetition takes place at the receiver side as well); epsl represents correct lists
where no e1 and no e2 occur, e1l , e2l are representations of
correct lists where only e1 (e2 resp.) occurs; e1e2l, e2e1l represent lists where both e1 and e2 occur, in the corresponding
list abp1cdp2 will be
abstracted to (ne, e1e2l, long-list);
list p1 will be abstracted
to (e1, e1l, one-el); list aba will be abstracted to (ne, error, long-list).
Define a data type for
abstract lists in Promela and the abstract version of the removing of the head element from the
May 29 - June
- Prove that the Petri net
given in Fig. 5.1 (the upper net), p.90 of [Desel, Esparza] is live and
bounded by applying reduction techniques preserving liveness,
boundedness and safeness.
- Prove that definition 1 and
definition 3 of the free-choice nets
are equivalent (see the definitions at the slides).
- a) Exercise 4.3 from
b) Find for every net from
Exercise 4.3 the set of all markings M such that (N,M) is live.
- Consider the following two
WF-nets. Find out whether they have redundant or persistent places. Can
you make any conclusion about the soundness of these nets based on the
presence or absence of redundant
and persistent places?