Exam exercises Formal Methods - Esercizi d'esame svolti Formal methods

Exam exercises FM - De Giacomo

Exam 22/01/2014

Exercise 5

x = 100

x := y + 50 {y = 50

if (y > 0) then x := y + 100 → {y + 100 + y = 100 → {y = 0

else x := y + 200; → {y + 200 + y = 100 → {y = 50

{(y > 0 and y = 0) or (y ≤ 0 and y = 50) = {y = 50

x := x + y {x + y = 100

So, the wp is {y = 50

Exam 18/02/2014

Exercise 5

x := y + 1; {(y > 0 and y + 1 + y = 0) or y = 100 = {(y > 0 and y = 0.5) or y = 100 = {false or y = 100

if (y > 0) then x := x + y {x + y = 0

else x := y + 100; {y = 100

{(y > 0 and x + y = 0) or (y ≤ 0 and y = 100) = {(y > 0 and x + y = 0) or y = 100

x := x + y; {x = 0

So the wp is {false or y = 100

Exam 11/06/2015

Exercise 1

Alphabet: E(x), W(x), Dir(x), TD(x), Dep(x), Pa(x), Pr(x), R(x), worksin(x, y), directs(x, y), pd(x, y), pp(x, y), pr(x, y)

UML class diagram axioms:

• forall x. TD(x) implies W(x)
• forall x. TD(x) implies D(x)
• forall x. Dir(x) implies E(x)
• forall x. W(x) implies E(x)
• forall x, y. worksin(x, y) implies E(x) and Dep(y)
• forall x. E(x) implies 1 ≤ #{y | worksin(x, y)} ≤ 1
• forall x, y. directs(x, y) implies Dir(x) and Dep(y)
• forall x. Dir(x) implies #{y | directs(x, y)} ≤ 1
• forall y. Dep(y) implies 1 ≤ #{x | directs(x, y)} ≤ 1
• forall x, y directs(x, y) implies worksin(x, y)
• forall x, y. pd(x, y) implies Pa(x) and Dep(y)
• forall x. Pa(y) implies 1 ≤ #{y | pd(x, y)} ≤ 1
• forall x, y. pp(x, y) implies Pa(x) and Pr(y)
• forall x. Pa(y) implies 1 ≤ #{y | pp(x, y)} ≤ 1
• forall x, y. pr(x, y) implies Pa(x) and R(y)
• forall x. Pa(y) implies 1 ≤ #{y | pr(x, y)} ≤ 1

forall x, x', y, z. pd(x, y) and pd(x', y) and pp(x, z) and pp(x', z) implies x = x'

Exercise 2

1)

• E = John, Mary, Joe, Jim, Rick, Ann
• W = John, Mary, Joe, Ann
• Dir = Jim, Rick, Ann
• TD = Ann
• Dep = ICT, HR, Management
• worksin = John, ICT; Mary, ICT; Joe, HR; Ann, ICT; Jim, HR; Rick, Management
• directs = Ann, ICT; Jim, HR; Rick, Management

Check:

• worksin = John, Mary, Joe, Jim, Rick, Ann are employee → Ok
• ICT, HR, Management are department → Ok
• Every employee has exactly one department → Ok
• directs = Ann, Jim, Rick are director → Ok
• ICT, HR, Management are department → Ok
• Every department has exactly one director → Ok
• Every director has at most 1 department → Ok

So the above completed instantiation is correct!

2)(a)

Return the directors that direct a department with at least one worker. Dir(x) and exists w, d. directs(x, d) and worksin(w, d) → Jim, Ann

(b)

Return the departments whose employees are all directors. Dep(y) and (forall x. Dir(x) implies worksin(x, y)) → Management

Exercise 4

I i ≤ 10. P {i=0} g: (i<10) delta: (i:= i+1) Q {i=10}

In order to check if this triple is correct, it must satisfy 3 conditions:

1. P implies I {i=0 implies {i ≤ 10 → True!
2. (not g and I implies Q {i ≥ 10 and i ≤ 10 implies {i = 10 {i = 10 implies {i = 10 → True!
3. {g and I delta I

We have to compute weakest precondition of (delta, I i ≤ 10 i := i + 1 i + 1 ≤ 10 i ≤ 9

So we calculate:

(g and I implies wp {i < 10 and i ≤ 10 implies {i ≤ 9 {i ≤ 9} implies {i ≤ 9 → True!

The 3 conditions are satisfied, so the Hoare triple is correct!

Exercise 5

q1 := edge(r, b), edge(b, g), edge(g, r). q2 := edge(x, y), edge(y, z), edge(z, x), edge(z, v), edge(v, w), edge(w, z).

We want to check q1 ⊆ q2. They are boolean so we don't need to freeze them with fresh constant. Now we build the database for q1 → DBq1 domain = {r, b, g} edges e = {(r, b), (b, g), (g, r)}

Now I need to find a satisfying assignment in order to DBq1 | q2

• alpha(x) = r
• alpha(y) = b
• alpha(z) = g
• alpha(v) = r
• alpha(w) = b

This is a satisfying assignment. So we write the database q2 → DBq2 domain = {x, y, z, v, w} edges e = {(x, y), (y, z), (z, x), (z, v), (v, w), (w, z)}

An homomorphism is a mapping between 2 interpretation so we have to map the object in the domain of q2 into the domain of q1

• h(x) = alpha(x) = r
• h(y) = alpha(y) = b
• h(z) = alpha(z) = g
• h(v) = alpha(v) = r
• h(w) = alpha(w) = b

This is an homomorphism for the Chandra Merlin theorem.

Now we check if is an homomorphism:

• (x, y) in e in DBq2 → (h(x), h(y)) in e in DBq1 = (r, b) in e in DBq1 → Ok
• (y, z) in e in DBq2 → (h(y), h(z)) in e in DBq1 = (b, g) in e in DBq1 → Ok
• (z, x) in e in DBq2 → (h(z), h(x)) in e in DBq1 = (g, r) in e in DBq1 → Ok
• (z, v) in e in DBq2 → (h(z), h(v)) in e in DBq1 = (g, r) in e in DBq1 → Ok
• (v, w) in e in DBq2 → (h(v), h(w)) in e in DBq1 = (r, b) in e in DBq1 → Ok
• (w, z) in e in DBq2 → (h(w), h(z)) in e in DBq1 = (b, g) in e in DBq1 → Ok

The check is ok, so we found the homomorphism!

Exam 11/09/2015

Exercise 1

Alphabet: S(x), C(x), B(x), T(x), L(x), Sea(x), O(x), onboard(x, y), incommand(x, y), tb(x, y), ts(x, y), tl(x, y)

UML class diagram axioms:

• forall x. C(x) implies S(x)
• forall x, y. onboard(x, y) implies S(x) and B(y)
• forall x. S(x) implies #{y | onboard(x, y)} ≤ 1
• forall y. B(y) implies 1 ≤ #{x | onboard(x, y)}
• forall x, y. incommand(x, y) implies C(x) and B(y)
• forall x. C(x) implies #{y | incommand(x, y)} ≤ 1
• forall y. B(y) implies 1 ≤ #{x | incommand(x, y)} ≤ 1
• forall x, y. incommand(x, y) implies onboard(x, y)
• forall x. O(x) implies Sea(x)
• forall x, y. tb(x, y) implies T(x) and B(y)
• forall x. T(x) implies 1 ≤ #{y | tb(x, y)} ≤ 1
• forall x, y. ts(x, y) implies T(x) and Sea(y)
• forall x. T(x) implies 1 ≤ #{y | ts(x, y)} ≤ 1
• forall x, y. tl(x, y) implies T(x) and L(y)
• forall x. T(x) implies 1 ≤ #{y | tl(x, y)} ≤ 1
• forall x, x', y. tb(x, y) and tb(x', y) implies x = x'

Exercise 2

1)

• S = Dustin, Lubber, Rusty, Alice, Beth
• C = Alice, Beth
• B = Constitution, Enterprise
• onboard = Dustin, Constitution; Lubber, Constitution; Rusty, Constitution; Alice, Constitution; Beth, Enterprise
• incommand = Alice, Constitution; Beth, Enterprise
• Sea = Mediterranean, Atlantic
• O = Atlantic

Check:

• onboard = Dustin, Lubber, Rusty, Alice, Beth are sailors → Ok
• Constitution, Enterprise are boats → Ok
• Every sailor has at most 1 boat → Ok
• Every boat has at least 1 sailor → Ok
• incommand = Alice, Beth are commanders → Ok
• Constitution, Enterprise are boats → Ok
• Every commander has at most 1 boat → Ok
• Every boat has exactly 1 commander → Ok

So the above completed instantiation is correct!

2)(a)

Return the commanders that command a boat with at least a sailor who is not a commander. C(x) and exists y, w. incommand(x, y) and onboard(w, y) and not C(w) → Alice

(b)

Return the boats that have on board only commanders. B(y) and forall x. onboard(x, y) implies C(x) → Enterprise

(c)

Return the boats that have on board all the sailors who are not commanders. B(y) and (forall x. (S(x) and not C(x)) implies onboard(x, y)) → {}

Exercise 3

Mu-Calculus formula:

P := nu X. mu Y. ((a and <next>X) or (not b and <next>Y))

| X0 | = 1, 2, 3, 4

| X1 | = | mu Y. ((a and <next>X0) or (not b and <next>Y)) | = 1, 2, 4

| Y00 | = {}

| Y01 | = | ((a and <next>X0) or (not b and <next>Y00)) | = (( | a | inter PreE , | X0 | ) union ( | not b | inter PreE , | Y00 | )) = 2, 4 inter 1, 2, 3, 4 union 1, 2 inter {}) = 2, 4 union {} = 2, 4

| Y02 | = | ((a and <next>X0) or (not b and <next>Y01)) | = (( | a | inter PreE , | X0 | ) union ( | not b | inter PreE , | Y01 | )) = 2, 4 inter 1, 2, 3, 4 union 1, 2 inter 1, 3, 4 = 2, 4 union 1 = 1, 2, 4

| Y03 | = | ((a and <next>X0) or (not b and <next>Y02)) | = (( | a | inter PreE , | X0 | ) union ( | not b | inter PreE , | Y02 | )) = 2, 4 inter 1, 2, 3, 4 union 1, 2 inter 1, 3, 4 = 2, 4 union 1 = 1, 2, 4

| X2 | = | mu Y. ((a and <next>X1) or (not b and <next>Y)) | = 1, 2, 4 = 4

| Y10 | = {}

| Y11 | = | ((a and <next>X1) or (not b and <next>Y10)) |= (( | a | inter PreE , | X1 | ) union ( | not b | inter PreE , | Y10 | )) = 2, 4 inter 1, 3, 4 union 1, 2 inter {}) = 4 union {} = 4

| Y12 | = | ((a and <next>X1) or (not b and <next>Y11)) |= (( | a | inter PreE , | X1 | ) union ( | not b | inter PreE , | Y11 | )) = 2, 4 inter 1, 3, 4 union 1, 2 inter 3, 4 = 4 union {} = 4

| X3 | = | mu Y. ((a and <next>X2) or (not b and <next>Y)) | = 1, 2, 4 = 4

| Y20 | = {}

| Y21 | = | ((a and <next>X2) or (not b and <next>Y20)) |= (( | a | inter PreE , | X2 | ) union ( | not b | inter PreE , | Y20 | )) = 2, 4 inter 3, 4 union 1, 2 inter {}) = 4 union {} = 4

| Y22 | = | ((a and <next>X2) or (not b and <next>Y21)) |= (( | a | inter PreE , | X2 | ) union ( | not b | inter PreE , | Y21 | )) = 2, 4 inter 3, 4 union 1, 2 inter 3, 4 = 4 union {} = 4

| X3 | = | X2 | = 4 → fixpoint

I found the fixpoint 4. Check if initial state 1 is in 4 → No, so mu-calculus is not correct. → Tnot | P.

CTL formula to mu-calculus:

P := EF(a and EX AG b)

alpha = AG b = nu X. b and [next]X

beta = EX alpha = <next> alpha

gamma = a and beta

delta = EF gamma = mu X. gamma or <next>X

| alpha | = | nu X. b and [next]X | = 4

| X0 | = 1, 2, 3, 4

| X1 | = | b and [next]X0 | = | b | inter PreA , | X0 |= 3, 4 inter 1, 2, 3, 4 = 3, 4

| X2 | = | b and [next]X1 |= | b | inter PreA , | X1 |= 3, 4 inter 2, 4 = 4

| X3 | = | b and [next]X2 |= | b | inter PreA , | X2 |= 3, 4 inter 4 = 4

| beta | = | <next> alpha | = 3, 4 = PreE , | alpha | 3, 4

| gamma| = | a and beta | = 4 = | a | inter | beta |= 2, 4 inter 3, 4 = 4

| delta | = | mu X. gamma or <next>X | = 1, 2, 3, 4

| X0 | = {}

| X1 | = | gamma or <next>X0 |= | gamma | union PreE , | X0 |= 4 union {} = 4

| X2 | = | gamma or <next>X1 |= | gamma | union PreE , | X1 |= 4 union 3, 4 = 3, 4

| X3 | = | gamma or <next>X2 |= | gamma | union PreE , | X2 |= 4 union 2, 3, 4 = 2, 3, 4

| X4 | = | gamma or <next>X3 |= | gamma | union PreE , | X3 |= 4 union 1, 2, 3, 4 = 1, 2, 3, 4

| X5 | = | gamma or <next>X4 |= | gamma | union PreE , | X4 |= 4 union 1, 2, 3, 4 = 1, 2, 3, 4

Check if the initial state is in delta → Yes. T | P, so CTL formula property is true in the initial state of TS.

Exercise 4

I (i + j ≤ 10 P {i=0 and j=10 g: (i<10) delta: {j:=j-1; i:= i+1 Q {j=0}

In order to check if the Hoare triple is correct, it must satisfy 3 conditions:

1. P implies I {i=0 and j=10 implies {i + j ≤ 10 → true!
2. (not g and I implies Q {i ≥ 10 and i + j ≤ 10 implies {j=0} → true
3. (g and I delta I

We have to compute the weakest precondition wp of (delta, I i := i + 1 j := j - 1 i + j ≤ 10 → wp: i + 1 + j - 1 ≤ 10 → wp: i + j ≤ 10

Now we check if (g and I implies wp: {i < 10 and i + j ≤ 10 implies {i + j ≤ 10 → True

The 3 conditions are satisfied, so the Hoare triple is correct!

Exercise 5

q1 :- edge(r, b), edge(b, g), edge(g, r)

q2 :- edge(i, f), edge(f, v), edge(v, i), edge(i, a), edge(a, v), edge(a, s), edge(s, i)

We want to check q1 ⊆ q2. The queries are boolean, so we don't need to freeze them with fresh constant. Now we build the database for q1 → DBq1 domain = {r, b, g} edges e = {(r, b), (b, g), (g, r)}

Now I need to find a satisfying assignment in order to DBq1 | q2

• alpha(i) = r
• alpha(f) = b
• alpha(v) = g
• alpha(a) = b
• alpha(s) = g

This is a satisfying assignment. So we write the database for q2 → DBq2 domain = {i, f, v, a, s} edges e = {(i, f), (f, v), (v, i), (i, a), (a, v), (a, s), (s, i)}

An homomorphism is a mapping between 2 interpretation, so we have to map the object in the domain of q2 into the domain of q1

• h(i) = alpha(i) = r
• h(f) = alpha(f) = b
• h(v) = alpha(v) = g
• h(a) = alpha(a) = b
• h(s) = alpha(s) = g

This is an homomorphism for Chandra Merlin Theorem.

Now we check if is an homomorphism:

• (i, f) in e in DBq2 → (h(i), h(f)) in e in DBq1 = (r, b) in e in DBq1 → Ok
• (f, v) in e in DBq2 → (h(f), h(v)) in e in DBq1 = (b, g) in e in DBq1 → Ok
• (v, i) in e in DBq2 → (h(v), h(i)) in e in DBq1 = (g, r) in e in DBq1 → Ok
• (i, a) in e in DBq2 → (h(i), h(a)) in e in DBq1 = (r, b) in e in DBq1 → Ok
• (a, v) in e in DBq2 → (h(a), h(v)) in e in DBq1 = (b, g) in e in DBq1 → Ok
• (a, s) in e in DBq2 → (h(a), h(s)) in e in DBq1 = (b, g) in e in DBq1 → Ok
• (s, i) in e in DBq2 → (h(s), h(i)) in e in DBq1 = (g, r) in e in DBq1 → Ok

The check is ok, so we found the homomorphism!

Exam 17/06/2016

Exercise 4

Definition:

A state s0 of transition system S is bisimilar, or simply equivalent, to a state t0 of transition system T iff there exists a bisimulation between the initial states s0 and t0.

A binary relation R is a bisimulation iff:

• (s, t) in R implies that:
• s is final if t is final
• for all action a: if s → [a]s' then exists t'. t →[a] t' and (s',t') in R
• if t →[a]t' then exists s'. s →[a] s' and (s',t') in R

R0 = {(t1, s1), (t1, s2), (t1, s3), (t2, s1), (t2, s2), (t2, s3)} → Cartesian product

R1 = {(t1, s1), (t2, s2), (t2, s3)} → remove the pair of states that are final in one state and not in the other

R2 = {(t1, s1), (t2, s2)} → remove tuple where s can do an action and t cannot and viceversa

R3 = {(t2, s2)} → remove tuples (t, s) that can reach (t', s') but (t', s') is not in R

R4 = {}

R5 = {}

R4 = R5 = {} → greatest fixpoint

S and T are not bisimilar since (s1, t1 don't belong to GFP.

Exam 25/07/2016

Exercise 1

Alphabet: A(x), G(x), P(x), S(x), member(x, y), recorded(x, y), guest(x, y)

UML Class Diagram Axioms:

• forall x, y. recorded(x, y) implies A(x) and S(y)
• forall y. S(y) implies 1 ≤ #{x | recorded(x, y)} ≤ 1
• forall x, y. guest(x, y) implies P(x) and S(y)
• forall x, y. member(x, y) implies G(x) and P(y)
• forall x. G(x) implies 2 ≤ #{y | member(x, y)}
• forall x. G(x) implies A(x)
• forall x. P(x) implies A(x)
• forall x. G(x) implies not P(x)
• forall x. A(x) implies G(x) or P(x)

Exercise 2

1)

• G = Be, RS
• P = John, Paul, George, Ringo, Mick, Keith
• A = Be, RS, John, Paul, George, Ringo, Mick, Keith
• member = { John, Be), Paul, Be), George, Be), Ringo, Be), Mick, RS, Keith, RS }
• S = { original, cover }
• recorded = { RS, original), Be, cover }
• guest = { John, original), Paul, original)}

Check:

• member = John, Paul, George, Ringo, Mick, Keith are all person → OK
• Be, RS are all group → OK
• Every group are at least 2 member → OK
• recorded = Be, RS are all group → OK
• {original, cover} are all song → OK
• Every song is recorded by 1 and only 1 artist → OK
• guest = John, Paul, George, Ringo, Mick, Keith are all person → OK
• {original, cover} are all song → OK

So the above completed instantiation is correct!

2)(a)

Return groups with more than 3 members (at least 4). exists y1, y2, y3, y4. G(x) and member(x, y1) and member(x, y2) and member(x, y3) and member(x, y4) and y1 ≠ y2 and y1 ≠ y3 and y1 ≠ y4