ALL 10 CHAPTERS COVERED
,Appendix B
Solutions to Selected Exercises
This document contains solutions to selected exercises in the book Principles of Model Checking,
first edition, by Christel Baier (TU Dresden, Germany) and Joost-Pieter Katoen (RWTH Aachen
University, Germany & University of Twente, the Netherlands). This booklet is intended for
lecturers and instructors for courses that are based on this book.
Most of the solutions in this booklet are adapted from solution sets handed out to students in
classes we taught in the last couple of years. We thank our instructors for these classes for their
contributions, in particular, Tobias Blechmann, Frank Ciesinski, Markus Grösser, Tingting Han,
Joachim Klein, Sascha Klüppelholz, Miriam Nasfi, Martin Neuhäusser, and Ivan S. Zapreev for
their contributions.
This is a draft version. Solutions are provided without any guarantee of correctness. We welcome
suggestions for improvements to the solutions, as well as elegant solutions to exercises of the book
that are not covered in this booklet.
c 2008 Christel Baier and Joost-Pieter Katoen. All rights reserved.
Permission is granted to college and university instructors to make a reasonable number of copies,
free of charge, as needed to plan and run their courses. Instructors are expected to take reasonable
precautions against further, unauthorized copies, whether on paper, electronic, or other media.
Permission is also granted to MIT Press editorial, marketing, and sales staff to provide copies free
of charge to instructors and prospective instructors, and to make copies for their own use.
Other copies, whether paper, electronic, or other media, are prohibited without prior written
consent of the authors.
3
,4 Solutions to Selected Exercises
List of Covered Exercises
1. System Verification
2. Modelling Concurrent Systems 6
2.3 ...... 6 2.9 ...... 8 2.12 ...... 12
2.7 ...... 7 2.11 ...... 10
3. Linear-Time Properties 13
3.1 ...... 13 3.9 ...... 16 3.14 ...... 19
3.2 ...... 13 3.10 ...... 16 3.15 ...... 19
3.3 ...... 14 3.11 ...... 17 3.17 ...... 20
3.5 ...... 14 3.12 ...... 17 3.18 ...... 20
3.8 ...... 15 3.13 ...... 18 3.19 ...... 21
4. Regular Properties 22
4.1 ...... 22 4.11 ...... 26 4.24 ...... 28
4.2 ...... 23 4.12 ...... 26 4.25 ...... 29
4.5 ...... 23 4.13 ...... 27 4.26 ...... 30
4.6 ...... 24 4.22 ...... 27 4.27 ...... 30
4.7 ...... 25
5. Linear Temporal Logic 35
5.2 ...... 35 5.8 ...... 37 5.20 ...... 41
5.4 ...... 35 5.11 ...... 38 5.25 ...... 43
5.5 ...... 35 5.13 ...... 39 5.26 ...... 48
5.6 ...... 36 5.17 ...... 40 5.27 ...... 51
6. Computation Tree Logic 57
6.2 ...... 57 6.15 ...... 60 6.24 ...... 68
6.3 ...... 58 6.16 ...... 62 6.29 ...... 70
6.8 ...... 59 6.18 ...... 64 6.31 ...... 70
6.9 ...... 59 6.19 ...... 65 6.32 ...... 74
6.12 ...... 60 6.21 ...... 67
,Solutions to Selected Exercises 5
7. Equivalences and Abstraction 77
7.1 ...... 77 7.18 ...... 78 7.24 ...... 83
7.5 ...... 77 7.19 ...... 81 7.25 ...... 83
7.7 ...... 77 7.20 ...... 81 7.30 ...... 84
7.8 ...... 78 7.22 ...... 83
8. Partial Order Reduction 87
8.1 ...... 87 8.7 ...... 89 8.10 ...... 92
8.6 ...... 87 8.9 ...... 92 8.14 ...... 93
9. Timed Automata 96
9.1 ...... 96 9.3 ...... 98 9.5 ...... 101
9.2 ...... 97 9.4 ...... 100
10. Probabilistic Systems 103
10.1 ...... 103 10.6 ...... 106 10.29 ...... 106
10.2 ...... 105 10.16 ...... 106
,6 Solutions to Selected Exercises
Exercises of Chapter 2
Answer to Exercise 2.3
S
(a) Let Act = 0<i65 { ri , oi , gi , yi }. Labeling the transition system Ai yields:
ri oi
Ai : red
yellow red/yellow
green gi
yi
(b) The controller has to synchronize with the traffic lights. Note that the actions defined in part
(a) uniquely identify the i-th transition system. This is exploited by the controller in the
following way. The controller synchronizes with the traffic lights using pairwise handshaking.
C: r1 r2 r3
o1 o2 o3
ry1 ry2 ry3
g1 r1 g2 r2 g3
g1 g2 g3
y1 y2 y3
r3
y1 y2 y3
(c) Let TS1 k · · · kTSn denote the parallel composition of TS1 through TSn where TSi and TSj
(0 < i < j 6 n) synchronize over the set of actions Hi,j = Acti ∩Actj such that Hi,j ∩Actk =
∅ for k 6∈ { i, j }. The inference rules for the transition relation are:
S
– if α ∈ Acti \ 0<j6n,i6=j Hi,j and 0 < i 6 n:
si −−→ i s′i
α
hs1 , . . . , si , . . . , sn i −−→ hs1 , . . . , s′i , . . . , sn i
α
– if α ∈ Hi,j and 0 < i < j 6 n:
→ i s′i
α
si −− → j s′j
α
sj −−
→ s1 , . . . , s′i , . . . , s′j , . . . , sn
α
hs1 , . . . , si , . . . , sj , . . . , sn i −−
By applying these inference rules, the transition system A1 kA2 kA3 kC becomes:
,Solutions to Selected Exercises 7
hr, r, r, r1i
o1
hry, r, r, ry1i hr, r, r, r2i
g1 o2
r1
hg, r, r, g1i hr, ry, r, ry2i hr, r, r, r3i
y1 g2 o3
r2
hy, r, r, y1i hr, g, r, g2i hr, r, ry, ry3i
r3
y2 g3
hr, y, r, y2i hr, r, g, g3i
y3
hr, r, y, y3i
Answer to Exercise 2.7
(a) The program graph PGi for process i is given as:
1
true : p[i] := 0 V
true : ji := 1 y[ji ] 6= i ∨ p[k] < ji : ji := ji + 1
k6=i
2
ji < n : p[i] := ji
ji = n : enter true : y[ji ] := i
5 3 4
Note that we consider i as a constant here and that the variables ji are private to process i.
(b) The cardinality of the set of states of TS(PG1 ||| · · · |||PGn ) can be deduced as follows. Let
PGi = (Loci , Acti , Effecti , ֒→i , Loc0 , g0 ) be the formal representation of the program graph
from part (a) where:
– Loci = { 1, 2, 3, 4, 5 }
– Acti = { ji := 1, p[i] := ji , y[ji ] := i, ji := ji +1, enter, p[i] := 0 | i ∈ {1, . . . , n} }
According to the algorithm, we have:
dom(y[k]) = { 1, . . . , n } for all k ∈ {0, . . . , n − 1}
dom(ji ) = dom(p[k]) = { 0, . . . , n − 1 } for all k, i ∈ {1, . . . , n}
,8 Solutions to Selected Exercises
Therefore it follows |dom(y[k])| = |dom(ji )| = |dom(p[k])| = n. The arrays y and p have
capacity n. The state space of the transition system is:
S = Loc1 × · · · × Locn × Eval ({p[k], y[l], ji | i, k ∈ {1, . . . , n} and l ∈ {0, . . . , n − 1}}) .
Therefore we obtain |S| = 5n · n3n .
(c) We prove a stronger statement that implies mutual exclusion:
At level j ∈ { 0, . . . , n−1 }, at most n−j processes are at level > j
By definition, process Pi is at level j iff p[i] = j. We proceed by induction over j:
– basis (j = 0): The statement trivially holds, as n−j = n−0 = n and there are at most
n processes in the system.
– induction step (j j + 1): The induction hypothesis implies that there are at most
n−j processes at level > j. We show that there is at least one process that cannot move
from level j to level j+1. By contradiction, assume there also were n − j processes at
levels > j+1 (i.e., no process is stuck at level j). Let i be the last process that writes
to y[j]. Therefore, the old value of y[j] that corresponds to the previous process k at
level j is overwritten and we have y[j] = i. Hence the condition y[j] 6= i cannot be
true. According to the algorithm,
∗ process k writes p[k] before it writes y[j] and
∗ process i reads p[k] only after it wrote to y[j].
Therefore every time process i reads p[k], process k already set p[k] = j and for process
i, the second condition p[k] < j is not fulfilled either.
We assumed that process i enters level j + 1. This yields a contradiction since it cannot
leave the wait–loop.
According to the idea of the algorithm, a process enters the critical section when it leaves
the wait–loop at level n−1. As we proved, at level n−1, there may only be n−(n−1) = 1
processes at level > (n−1). Therefore, the mutual exclusion property holds.
Answer to Exercise 2.9
(a) The program graphs of the two processes can be depicted as follows:
true : y1 := y2 + 1 y2 = 0 ∨ y1 6 y2 : enter1
PG1 : 1 2 3
true : y1 := 0
true : y2 := y1 + 1 y1 = 0 ∨ y2 < y1 : enter2
PG2 : 1′ 2′ 3′
true : y2 := 0
(b) First, we provide the program graph PG1 kPG2 :
,Solutions to Selected Exercises 9
1, 1′
true : y1 := y2 + 1 true : y2 := y1 + 1
true : y1 := 0 true : y2 := 0
2, 1′ 1, 2′
y1 = 0 ∨ y2 < y1 : enter2
true : y2 := y1 + 1 true : y1 := y2 + 1
y2 = 0 ∨ y1 6 y2 : enter1
true : y1 := 0
true : y2 := 0
3, 1′ 2, 2′ 1, 3′
y2 = 0 ∨ y1 6 y2 : enter1 y1 = 0 ∨ y2 < y1 : enter2
y1 := y2 + 1
true : y2 := y1 + 1
3, 2′ 2, 3′
true : y2 = 0
y1 = 0 ∨ y2 < y1 : enter2 y2 = 0 ∨ y1 6 y2 : enter1 true : y1 := 0
3, 3′
The transition system TS(PG1 |||PG2 ) for y1 6 2 and y2 6 2 becomes:
,10 Solutions to Selected Exercises
(1, 1′ ), y1 = y2 = 0
y2 := y1 + 1
y2 := 0
y2 := 0
y1 := 0 y1 := y2 + 1
y1 := 0
(2, 1′ ), y 1 = 1, y2 = 0 (1, 2′ ), y 1 = 0, y2 = 1
y2 := y1 + 1 y1 := y2 + 1
enter2
enter1 (2, 2′ ), y1 = 1, y2 = 2 (2, 2′ ), y1 = 2, y2 = 1
enter1 enter2
y2 := y1 + 1
(3, 1′ ), y1 = 1, y2 = 0 (3, 2′ ), y1 = 1, y2 = 2 (2, 3′ ), y1 = 2, y2 = 1 (1, 3′ ), y1 = 0, y2 = 1
y1 := y2 + 1
y1 := 0 y2 := 0
(1, 2′ ), y1 = 0, y2 = 2 (2, 1′ ), y1 = 2, y2 = 0
enter1
y1 := y2 + 1 y2 := y1 + 1
enter2
(1, 3′ ), y 1 = 0, y2 = 2 (2, 2′ ), y1 = 3, y2 = 2 (2, 2′ ), y1 = 2, y2 = 3 (3, 1′ ), y1 = 2, y2 = 0
y1 := y2 + 1 y2 := y1 + 1
(2, 3), y1 = 3, y2 = 2 (3, 2′ ), y1 = 2, y2 = 3
(c) To show that the complete transition system is infinite, we consider the infinite execution:
y1 :=y2 +1
h1, 1′ , y1 = y2 = 0i −− −−−−−→ h2, 1′ , y1 = 1, y2 = 0i
y2 :=y1 +1
−−−−−−−→ h2, 2′ , y1 = 1, y2 = 2i
enter1
−− −−−→ h3, 2′ , y1 = 1, y2 = 2i
y1 :=0
−−−−→ h1, 2′ , y1 = 0, y2 = 2i
y1 :=y2 +1
−− −−−−−→ h2, 2′ , y1 = 3, y2 = 2i
enter2
−− −−−→ h2, 3′ , y1 = 3, y2 = 2i
y2 :=0
−−−−→ h2, 1′ , y1 = 3, y2 = 0i
y2 :=y1 +1
−− −−−−−→ h2, 2′ , y1 = 3, y2 = 4i
enter1
−−−−−→ h3, 2′ , y1 = 3, y2 = 4i
···
Answer to Exercise 2.11
(a) The output and the circuit control functions for C1 are as follows:
λy = r1 ∧ r2
δr 1 = (x ∧ ¬r1 ) ∨ (¬x ∧ r1 ) = x ⊕ r1
δr 2 = (¬x ∧ r2 ) ∨ (x ∧ r1 )
The transition system is given by TS(C1 ) = TS1 = (Eval({x, r1 , r2 }), Act, →, I, AP, L) where
, Solutions to Selected Exercises 11
– I = { (x, r1 , r2 ) | x, r1 , r2 ∈ B } = Eval({ x, r1 , r2 })
– AP = { x, r1 , r2 , y }
– L : S → 2AP as given in the figure below where evaluations are represented as triples
(x, r1 , r2 ).
{r2 } {x, r1 }
0, 1, 1 0, 0, 1 1, 1, 0
{r1 , r2 , y}
1, 0, 0 0, 0, 0
{x} ∅
1, 1, 1 1, 0, 1 0, 1, 0
{x, r1 , r2 , y} {x, r2 } {r1 }
(b) The transition system representation TS2 of the circuit C2 is given by:
∅ {r, y}
0 1
The synchronous composition of TS1 and TS2 is defined as the transition system
TS1 ⊗ TS2 = (S1 × S2 , Act, →, I1 × I2 , AP1 ⊎ AP2 , L)
It is given by the diagram below. Note that the set of initial states in this case equals the set
of states S1 × S2 , i.e., every state can serve as an initial state. Therefore we do not indicate
the initial states. We also omit the atomic propositions. These can be defined analogously
to part (a) by renaming the variables of C2 to r1′ and y ′ , respectively.
(0, 1, 1), 0 (1, 1, 1), 1 (1, 0, 1), 0
(0, 0, 1), 0 (1, 1, 0), 1
(0, 1, 1), 1
(1, 0, 0), 0 (0, 0, 0), 1
(0, 0, 1), 1
(0, 1, 0), 1
(1, 1, 1), 0
(1, 1, 0), 0 (1, 0, 0), 1 (0, 0, 0), 0
(1, 0, 1), 1 (0, 1, 0), 0
,Appendix B
Solutions to Selected Exercises
This document contains solutions to selected exercises in the book Principles of Model Checking,
first edition, by Christel Baier (TU Dresden, Germany) and Joost-Pieter Katoen (RWTH Aachen
University, Germany & University of Twente, the Netherlands). This booklet is intended for
lecturers and instructors for courses that are based on this book.
Most of the solutions in this booklet are adapted from solution sets handed out to students in
classes we taught in the last couple of years. We thank our instructors for these classes for their
contributions, in particular, Tobias Blechmann, Frank Ciesinski, Markus Grösser, Tingting Han,
Joachim Klein, Sascha Klüppelholz, Miriam Nasfi, Martin Neuhäusser, and Ivan S. Zapreev for
their contributions.
This is a draft version. Solutions are provided without any guarantee of correctness. We welcome
suggestions for improvements to the solutions, as well as elegant solutions to exercises of the book
that are not covered in this booklet.
c 2008 Christel Baier and Joost-Pieter Katoen. All rights reserved.
Permission is granted to college and university instructors to make a reasonable number of copies,
free of charge, as needed to plan and run their courses. Instructors are expected to take reasonable
precautions against further, unauthorized copies, whether on paper, electronic, or other media.
Permission is also granted to MIT Press editorial, marketing, and sales staff to provide copies free
of charge to instructors and prospective instructors, and to make copies for their own use.
Other copies, whether paper, electronic, or other media, are prohibited without prior written
consent of the authors.
3
,4 Solutions to Selected Exercises
List of Covered Exercises
1. System Verification
2. Modelling Concurrent Systems 6
2.3 ...... 6 2.9 ...... 8 2.12 ...... 12
2.7 ...... 7 2.11 ...... 10
3. Linear-Time Properties 13
3.1 ...... 13 3.9 ...... 16 3.14 ...... 19
3.2 ...... 13 3.10 ...... 16 3.15 ...... 19
3.3 ...... 14 3.11 ...... 17 3.17 ...... 20
3.5 ...... 14 3.12 ...... 17 3.18 ...... 20
3.8 ...... 15 3.13 ...... 18 3.19 ...... 21
4. Regular Properties 22
4.1 ...... 22 4.11 ...... 26 4.24 ...... 28
4.2 ...... 23 4.12 ...... 26 4.25 ...... 29
4.5 ...... 23 4.13 ...... 27 4.26 ...... 30
4.6 ...... 24 4.22 ...... 27 4.27 ...... 30
4.7 ...... 25
5. Linear Temporal Logic 35
5.2 ...... 35 5.8 ...... 37 5.20 ...... 41
5.4 ...... 35 5.11 ...... 38 5.25 ...... 43
5.5 ...... 35 5.13 ...... 39 5.26 ...... 48
5.6 ...... 36 5.17 ...... 40 5.27 ...... 51
6. Computation Tree Logic 57
6.2 ...... 57 6.15 ...... 60 6.24 ...... 68
6.3 ...... 58 6.16 ...... 62 6.29 ...... 70
6.8 ...... 59 6.18 ...... 64 6.31 ...... 70
6.9 ...... 59 6.19 ...... 65 6.32 ...... 74
6.12 ...... 60 6.21 ...... 67
,Solutions to Selected Exercises 5
7. Equivalences and Abstraction 77
7.1 ...... 77 7.18 ...... 78 7.24 ...... 83
7.5 ...... 77 7.19 ...... 81 7.25 ...... 83
7.7 ...... 77 7.20 ...... 81 7.30 ...... 84
7.8 ...... 78 7.22 ...... 83
8. Partial Order Reduction 87
8.1 ...... 87 8.7 ...... 89 8.10 ...... 92
8.6 ...... 87 8.9 ...... 92 8.14 ...... 93
9. Timed Automata 96
9.1 ...... 96 9.3 ...... 98 9.5 ...... 101
9.2 ...... 97 9.4 ...... 100
10. Probabilistic Systems 103
10.1 ...... 103 10.6 ...... 106 10.29 ...... 106
10.2 ...... 105 10.16 ...... 106
,6 Solutions to Selected Exercises
Exercises of Chapter 2
Answer to Exercise 2.3
S
(a) Let Act = 0<i65 { ri , oi , gi , yi }. Labeling the transition system Ai yields:
ri oi
Ai : red
yellow red/yellow
green gi
yi
(b) The controller has to synchronize with the traffic lights. Note that the actions defined in part
(a) uniquely identify the i-th transition system. This is exploited by the controller in the
following way. The controller synchronizes with the traffic lights using pairwise handshaking.
C: r1 r2 r3
o1 o2 o3
ry1 ry2 ry3
g1 r1 g2 r2 g3
g1 g2 g3
y1 y2 y3
r3
y1 y2 y3
(c) Let TS1 k · · · kTSn denote the parallel composition of TS1 through TSn where TSi and TSj
(0 < i < j 6 n) synchronize over the set of actions Hi,j = Acti ∩Actj such that Hi,j ∩Actk =
∅ for k 6∈ { i, j }. The inference rules for the transition relation are:
S
– if α ∈ Acti \ 0<j6n,i6=j Hi,j and 0 < i 6 n:
si −−→ i s′i
α
hs1 , . . . , si , . . . , sn i −−→ hs1 , . . . , s′i , . . . , sn i
α
– if α ∈ Hi,j and 0 < i < j 6 n:
→ i s′i
α
si −− → j s′j
α
sj −−
→ s1 , . . . , s′i , . . . , s′j , . . . , sn
α
hs1 , . . . , si , . . . , sj , . . . , sn i −−
By applying these inference rules, the transition system A1 kA2 kA3 kC becomes:
,Solutions to Selected Exercises 7
hr, r, r, r1i
o1
hry, r, r, ry1i hr, r, r, r2i
g1 o2
r1
hg, r, r, g1i hr, ry, r, ry2i hr, r, r, r3i
y1 g2 o3
r2
hy, r, r, y1i hr, g, r, g2i hr, r, ry, ry3i
r3
y2 g3
hr, y, r, y2i hr, r, g, g3i
y3
hr, r, y, y3i
Answer to Exercise 2.7
(a) The program graph PGi for process i is given as:
1
true : p[i] := 0 V
true : ji := 1 y[ji ] 6= i ∨ p[k] < ji : ji := ji + 1
k6=i
2
ji < n : p[i] := ji
ji = n : enter true : y[ji ] := i
5 3 4
Note that we consider i as a constant here and that the variables ji are private to process i.
(b) The cardinality of the set of states of TS(PG1 ||| · · · |||PGn ) can be deduced as follows. Let
PGi = (Loci , Acti , Effecti , ֒→i , Loc0 , g0 ) be the formal representation of the program graph
from part (a) where:
– Loci = { 1, 2, 3, 4, 5 }
– Acti = { ji := 1, p[i] := ji , y[ji ] := i, ji := ji +1, enter, p[i] := 0 | i ∈ {1, . . . , n} }
According to the algorithm, we have:
dom(y[k]) = { 1, . . . , n } for all k ∈ {0, . . . , n − 1}
dom(ji ) = dom(p[k]) = { 0, . . . , n − 1 } for all k, i ∈ {1, . . . , n}
,8 Solutions to Selected Exercises
Therefore it follows |dom(y[k])| = |dom(ji )| = |dom(p[k])| = n. The arrays y and p have
capacity n. The state space of the transition system is:
S = Loc1 × · · · × Locn × Eval ({p[k], y[l], ji | i, k ∈ {1, . . . , n} and l ∈ {0, . . . , n − 1}}) .
Therefore we obtain |S| = 5n · n3n .
(c) We prove a stronger statement that implies mutual exclusion:
At level j ∈ { 0, . . . , n−1 }, at most n−j processes are at level > j
By definition, process Pi is at level j iff p[i] = j. We proceed by induction over j:
– basis (j = 0): The statement trivially holds, as n−j = n−0 = n and there are at most
n processes in the system.
– induction step (j j + 1): The induction hypothesis implies that there are at most
n−j processes at level > j. We show that there is at least one process that cannot move
from level j to level j+1. By contradiction, assume there also were n − j processes at
levels > j+1 (i.e., no process is stuck at level j). Let i be the last process that writes
to y[j]. Therefore, the old value of y[j] that corresponds to the previous process k at
level j is overwritten and we have y[j] = i. Hence the condition y[j] 6= i cannot be
true. According to the algorithm,
∗ process k writes p[k] before it writes y[j] and
∗ process i reads p[k] only after it wrote to y[j].
Therefore every time process i reads p[k], process k already set p[k] = j and for process
i, the second condition p[k] < j is not fulfilled either.
We assumed that process i enters level j + 1. This yields a contradiction since it cannot
leave the wait–loop.
According to the idea of the algorithm, a process enters the critical section when it leaves
the wait–loop at level n−1. As we proved, at level n−1, there may only be n−(n−1) = 1
processes at level > (n−1). Therefore, the mutual exclusion property holds.
Answer to Exercise 2.9
(a) The program graphs of the two processes can be depicted as follows:
true : y1 := y2 + 1 y2 = 0 ∨ y1 6 y2 : enter1
PG1 : 1 2 3
true : y1 := 0
true : y2 := y1 + 1 y1 = 0 ∨ y2 < y1 : enter2
PG2 : 1′ 2′ 3′
true : y2 := 0
(b) First, we provide the program graph PG1 kPG2 :
,Solutions to Selected Exercises 9
1, 1′
true : y1 := y2 + 1 true : y2 := y1 + 1
true : y1 := 0 true : y2 := 0
2, 1′ 1, 2′
y1 = 0 ∨ y2 < y1 : enter2
true : y2 := y1 + 1 true : y1 := y2 + 1
y2 = 0 ∨ y1 6 y2 : enter1
true : y1 := 0
true : y2 := 0
3, 1′ 2, 2′ 1, 3′
y2 = 0 ∨ y1 6 y2 : enter1 y1 = 0 ∨ y2 < y1 : enter2
y1 := y2 + 1
true : y2 := y1 + 1
3, 2′ 2, 3′
true : y2 = 0
y1 = 0 ∨ y2 < y1 : enter2 y2 = 0 ∨ y1 6 y2 : enter1 true : y1 := 0
3, 3′
The transition system TS(PG1 |||PG2 ) for y1 6 2 and y2 6 2 becomes:
,10 Solutions to Selected Exercises
(1, 1′ ), y1 = y2 = 0
y2 := y1 + 1
y2 := 0
y2 := 0
y1 := 0 y1 := y2 + 1
y1 := 0
(2, 1′ ), y 1 = 1, y2 = 0 (1, 2′ ), y 1 = 0, y2 = 1
y2 := y1 + 1 y1 := y2 + 1
enter2
enter1 (2, 2′ ), y1 = 1, y2 = 2 (2, 2′ ), y1 = 2, y2 = 1
enter1 enter2
y2 := y1 + 1
(3, 1′ ), y1 = 1, y2 = 0 (3, 2′ ), y1 = 1, y2 = 2 (2, 3′ ), y1 = 2, y2 = 1 (1, 3′ ), y1 = 0, y2 = 1
y1 := y2 + 1
y1 := 0 y2 := 0
(1, 2′ ), y1 = 0, y2 = 2 (2, 1′ ), y1 = 2, y2 = 0
enter1
y1 := y2 + 1 y2 := y1 + 1
enter2
(1, 3′ ), y 1 = 0, y2 = 2 (2, 2′ ), y1 = 3, y2 = 2 (2, 2′ ), y1 = 2, y2 = 3 (3, 1′ ), y1 = 2, y2 = 0
y1 := y2 + 1 y2 := y1 + 1
(2, 3), y1 = 3, y2 = 2 (3, 2′ ), y1 = 2, y2 = 3
(c) To show that the complete transition system is infinite, we consider the infinite execution:
y1 :=y2 +1
h1, 1′ , y1 = y2 = 0i −− −−−−−→ h2, 1′ , y1 = 1, y2 = 0i
y2 :=y1 +1
−−−−−−−→ h2, 2′ , y1 = 1, y2 = 2i
enter1
−− −−−→ h3, 2′ , y1 = 1, y2 = 2i
y1 :=0
−−−−→ h1, 2′ , y1 = 0, y2 = 2i
y1 :=y2 +1
−− −−−−−→ h2, 2′ , y1 = 3, y2 = 2i
enter2
−− −−−→ h2, 3′ , y1 = 3, y2 = 2i
y2 :=0
−−−−→ h2, 1′ , y1 = 3, y2 = 0i
y2 :=y1 +1
−− −−−−−→ h2, 2′ , y1 = 3, y2 = 4i
enter1
−−−−−→ h3, 2′ , y1 = 3, y2 = 4i
···
Answer to Exercise 2.11
(a) The output and the circuit control functions for C1 are as follows:
λy = r1 ∧ r2
δr 1 = (x ∧ ¬r1 ) ∨ (¬x ∧ r1 ) = x ⊕ r1
δr 2 = (¬x ∧ r2 ) ∨ (x ∧ r1 )
The transition system is given by TS(C1 ) = TS1 = (Eval({x, r1 , r2 }), Act, →, I, AP, L) where
, Solutions to Selected Exercises 11
– I = { (x, r1 , r2 ) | x, r1 , r2 ∈ B } = Eval({ x, r1 , r2 })
– AP = { x, r1 , r2 , y }
– L : S → 2AP as given in the figure below where evaluations are represented as triples
(x, r1 , r2 ).
{r2 } {x, r1 }
0, 1, 1 0, 0, 1 1, 1, 0
{r1 , r2 , y}
1, 0, 0 0, 0, 0
{x} ∅
1, 1, 1 1, 0, 1 0, 1, 0
{x, r1 , r2 , y} {x, r2 } {r1 }
(b) The transition system representation TS2 of the circuit C2 is given by:
∅ {r, y}
0 1
The synchronous composition of TS1 and TS2 is defined as the transition system
TS1 ⊗ TS2 = (S1 × S2 , Act, →, I1 × I2 , AP1 ⊎ AP2 , L)
It is given by the diagram below. Note that the set of initial states in this case equals the set
of states S1 × S2 , i.e., every state can serve as an initial state. Therefore we do not indicate
the initial states. We also omit the atomic propositions. These can be defined analogously
to part (a) by renaming the variables of C2 to r1′ and y ′ , respectively.
(0, 1, 1), 0 (1, 1, 1), 1 (1, 0, 1), 0
(0, 0, 1), 0 (1, 1, 0), 1
(0, 1, 1), 1
(1, 0, 0), 0 (0, 0, 0), 1
(0, 0, 1), 1
(0, 1, 0), 1
(1, 1, 1), 0
(1, 1, 0), 0 (1, 0, 0), 1 (0, 0, 0), 0
(1, 0, 1), 1 (0, 1, 0), 0
