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

PCTL formula to mu-calculus:

P := AF EG(a implies AX EX not a))

alpha = EX not a = <next> not a

beta = AX alpha = [next] alpha

gamma = a implies beta = not a or beta

delta = EG gamma = nu X. gamma and <next> X

epsilon = AF delta = mu X. delta or [next] X

| alpha | = | <next> not a | = PreE , | not a | = 0, 2, 3, 4

| beta | = | [next] alpha | = PreA , | alpha | = 1, 2, 3, 4

| gamma | = | not a or beta | = | not a | union | beta | = 0, 3, 4 union 1, 2, 3, 4 = 0, 1, 2, 3, 4

| delta | = | nu X. gamma and <next> X | = 0, 1, 2, 3, 4

Exam 21/12/2017 4

| X0 | = 0, 1, 2, 3, 4

| X1 | = | gamma and <next> X0 | = | gamma | inter PreE , | X0 | = 0, 1, 2, 3, 4 inter 0, 1, 2, 3, 4 = 0, 1, 2, 3, 4

| epsilon | = | mu X. delta or [next] X | = 0, 1, 2, 3, 4

| X0 | = {}

| X1 | = | delta or [next] X0 | = | delta | union PreA , | X0 | = 0, 1, 2, 3, 4 union {} = 0, 1, 2, 3, 4

Check if the initial state 0 is in 0, 1, 2, 3, 4 → Yes! T | P, so CTL formula property is true in the initial state of

TSExercise 4

I = (x ≥ 0 and y ≥ 0 and x + y = 23

P = {x = 23 and y = 0

g = (x>0)

delta = (x := x−1; y := y+1

Q = {y = 23

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

1 P implies I{x = 23 and y = 0 implies {x ≥ 0 and y ≥ 0 and x + y = 23 → true!

3 (not g and I implies Q{x ≤ 0 and x ≥ 0 and y ≥ 0 and x + y = 23 implies {y = 23{x = 0 and y ≥ 0 and x + y = 23 implies {y = 23 → true!

2 (g and I delta I

We have to compute the weakest precondition:

x := x−1

y := y+1

x ≥ 0 and y ≥ 0 and x + y = 23→ x−1 ≥ 0 and y+1 ≥ 0 and x - 1 + y + 1 = 23→ x ≥ 1 and y ≥ 1 and x + y = 23

So we want: (g and I implies wp{x > 0 and x ≥ 0 and y ≥ 0 and x + y = 23 implies {x ≥ 1 and y ≥ 1 and x + y = 23{x > 0 and y ≥ 0 and x + y = 23 implies {x ≥ 1 and y ≥ 1 and x + y = 23 → true!

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

Exercise 5

Exam 21/12/2017

Exercise 6

We want to model check that eventually always not a is true. We do this checking that the negated formula is false.

Negated formula: not (eventually always not a)

Generate the automa for the TS

Exam 21/12/2017 7

Check non emptiness by model checking this mu-calculus formula:

final = 1, ii), 2, ii)

nu X. (mu Y (final and <next>X or <next>Y| X0 | = { (init, i), 0, i), 1, i), 1, ii), 2, i), 2, ii) }

| X1 | = | mu Y (final and <next>X0 or <next>Y | = { (init, i), 0, i), 1, i), 1, ii), 2, i), 2, ii) }

| Y00 | = {}

| Y01 | = | (final and <next>X0 or <next>Y00 |= | final | inter PreE , | X0 | union PreE , | Y00 |= ({ 1, ii), 2, ii) } inter { (init, i), 0, i), 1, i), 1, ii), 2, i), 2, ii) }) union {}= { 1, ii), 2, ii) }

| Y02 | = | (final and <next>X0 or <next>Y01 |Exam 21/12/2017 8= | final | inter PreE , | X0 | union PreE , | Y01 |= ({ 1, ii), 2, ii) } inter { (init, i), 0, i), 1, i), 1, ii), 2, i), 2, ii) }) union 0, i), 1, i), 1, ii), 2, i),2,

ii)}= { 0, i), 1, i), 1, ii), 2, i), 2, ii) }| Y03 | = | (final and <next>X0 or <next>Y02 |= | final | inter PreE , | X0 | union PreE , | Y02 |= ({ 1, ii), 2, ii) } inter { (init, i), 0, i), 1, i), 1, ii), 2, i), 2, ii) }) union {(init, i), 0, i), 1, i), 1, ii),2, i), 2, ii)}= { (init, i), 0, i), 1, i), 1, ii), 2, i), 2, ii) }| Y04 | = | (final and <next>X0 or <next>Y03 |= | final | inter PreE , | X0 | union PreE , | Y03 |= ({ 1, ii), 2, ii) } inter { (init, i), 0, i), 1, i), 1, ii), 2, i), 2, ii) }) union {(init, i), 0, i), 1, i), 1, ii),2, i), 2, ii)}= { (init, i), 0, i), 1, i), 1, ii), 2, i), 2, ii) }{ (init, i), 0, i), 1, i), 1, ii), 2, i), 2, ii) } → fixpointCheck if (init, i) is in fixpoint → YES, so mu-calculus is correct for the negation of the originalformula T (eventually always not a)So, T not | eventually always not aExam 21/12/2017 9Exam 21/12/2017 BExercise 1Alphabet:C(x), BC(x), P(x), S(x), provides(x, y), contract(x, y, z), cost(x, y, z,

most 10 → Ok

Each service has at least 1 provider → Ok

contract/cost ={c1, b2 are customers → Ok

{s1, s2, s3 are services → Ok

{p1, p2 are providers → Ok

90.0, 80.0, 50.0, 170.0, 100.0 are real number

The above completed instantiation is correct!

2)Exam 21/12/2017 B 2(a) Check that, for every provider x and service y involved in a contract, provider x does provide service y.

forall x, y. (P(x) and S(y) and exists c. contract(c, y, x)) implies provides(x, y)→ {false}

(b) Return those customers that have contracts only for services provided by p2.

C(x) and forall y. (exists z. contract(x, y, z) implies provides("p2", y))→ {b2}

(c) Return those customers that have a contract for with all providers.

C(x) and forall z. P(z) implies exists y. contract(x, y, z)→ {}

Exercise 3

Mu-Calculus formula:

P := nu X. μY. ((b and [next]X) or (a and <next>Y ))

| X0 | = 0, 1, 2, 3, 4

| X1 | = | μY. ((b and [next]X0) or (a and <next>Y )) | = 3, 4

| Y00 | =

{}

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

| Y02 | = |((b and [next]X0) or (a and <next>Y01 |= | b | inter PreA , | X0 | union | a | inter PreE , | Y01 |= 3, 4 inter 0, 1, 2, ,3 ,4 union 1, 2 inter 0, 3, 4= 3, 4 union {} = 3, 4

| X2 | = | μY. ((b and [next]X1) or (a and <next>Y )) | = 3

| Y10 | = {}

| Y11 | = |((b and [next]X1) or (a and <next>Y10 |Exam 21/12/2017 B 3= | b | inter PreA , | X1 | union | a | inter PreE , | Y10 |= 3, 4 inter 3 union 1, 2 inter {})= 3 union {} = 3

| Y12 | = |((b and [next]X1) or (a and <next>Y11 |= | b | inter PreA , | X0 | union | a | inter PreE , | Y01 |= 3, 4 inter 3 union 1, 2 inter 0, 3= 3 union {} = 3

| X3 | = | μY. ((b and [next]X2) or (a and <next>Y )) | = {}

| Y20 | = {}

| Y21 | = |((b and [next]X2) or (a and <next>Y20 |= | b | inter PreA , | X2 | union | a | inter PreE ,

gamma and [next]X | = {}

X0 | = 0, 1, 2, 3, 4

X1 | = | gamma | inter PreA , | X0 |= 0, 3, 4 inter 0, 1, 2, 3, 4 = 0, 3, 4

X2 | = | gamma | inter PreA , | X1 |= 0, 3, 4 inter 3, 4 = 3, 4

X3 | = | gamma | inter PreA , | X2 |= 0, 3, 4 inter 3 = 3

X4 | = | gamma | inter PreA , | X3 |= 0, 3, 4 inter {} = {}

X5 | = | gamma | inter PreA , | X4 |= 0, 3, 4 inter {} = {}

epsilon | = | mu X. delta or <next>X | = {}

X0 | = {}

X1 | = | delta | union PreE , | X0 |= {} union {} = {}

Check if the initial state 0 is in {} → No, so CTL formula property is false in the initial state of TS.

Tnot | P.

Exercise 4

Exam 21/12/2017 B 5

I (x ≥ 0 y ≥ 0 x + y = 31

P {x = 31 y = 0

g: (x>0)

delta: (x := x−1; y := y+1

Q {y = 31

In order to check if this Hoare triple is correct, we have to satisfy 3 conditions:

1 P implies I{x = 31 and y = 0 implies {x ≥ 0 and y ≥ 0 and x + y = 31 → True

3 (not g and I implies Q{x ≤ 0 and x ≥ 0 and y ≥ 0 and x + y = 31 implies {y = 31{x =

0 and y ≥ 0 and x + y = 31 implies {y = 31 → True

2 (g and I delta IWe have to compute the weakest precondition of (delta, Ix := x − 1;y := y + 1;x ≥ 0 and y ≥ 0 and x + y = 31;→ wp = {x 1 ≥ 0 and y + 1 ≥ 0 and x 1 + y + 1 = 31 ={x ≥ 1 and y ≥ 1 and x + y = 31

So we need to verify if (g and I implies wp{x > 0 and x ≥ 0 and y ≥ 0 and x + y = 31 implies {x ≥ 1 and y ≥ 1 and x + y = 31

{x > 0 and y ≥ 0 and x + y = 31 implies {x ≥ 1 and y ≥ 1 and x + y = 31 → True

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

Exercise 5

Exam 21/12/2017 B 6

We want to prove that the formula is valid, so we check that the negation of the formula is UNSAT

The negation of the formula is UNSAT, so FOL formula is valid.

Exercise 6

We want to model check that eventually always not b is true. We do this checking that the negated formula is false.

Negated formula: not (eventually always not b)

Generate the automa for the TS

Exam 21/12/2017 B

Check non emptiness by model checking this mu-calculus formula:

final = 3, ii), 4, ii)}nu X. (mu Y. (final and <next>X or <next>Y| X0 | = { (init, i), 0, i), 3, i), 3, ii), 4, i), 4, ii) }| X1 | = | mu Y (final and <next>X0 or &l