Reference no: EM13935038

Exercise1(LTL) Question1 Assume a single atomic proposition pand the following LTL-path,which describes an alternating path of p and¬p. p // ¬p // p // ¬p // p // ¬p // ... Give an LTL formula that describes this path only. We assume two atomic propositions p and q. Question2 Decidewhetherthepathgivenontheright-handsidesatis?estheformula given on the left-hand side. pU(Xq) : p,q // p,¬q //¬p,¬q // p,q // ... pU(q ⇒¬Xq): p,¬q // p,¬q // ¬p,q // ¬p,q //¬p,¬q // ... X(¬(pUq)) : p,q // p,¬q // p,¬q // ¬p,q // ¬p,q // ... (In this question, "..." means that the last presented state is the same as all follow-up states.) 1 Question 3 Are the following LTL-formulas true for all paths (for atomic propositions p and q)?

Gp ⇒ (pUq)Up (pUq)∧(q Up) ⇔ p∧q Fp ⇔ F(Xp) X(Fp) ⇔ F(Xp) (pU(q ⇒¬Xq))∧(FGq) ⇔ pU(Gq)

Proofsare not necessary,but provide counter examplesifthe formula is in correct. However, if you provide proofs, you might get some bonus points.

Exercise2

(LocalAutomaton)

Question4 Compute the set cl(p Until¬p). Question5 Compute the set Sub(p Until¬p). Question6 Give the local automaton for p Until¬p. (Follow the de?nitions given in the lecture.) Exercise3(CTLModelChecking) 

q0 L(q0) = {a,b} q1 L(q1) = {b} q2 L(q2) = {a,c} q3 L(q3) = {a,b,c} q4 L(q4) = {a} q5 L(q5) = {c}

Figure 1: Automaton A Question7 Whichstatesofautomaton A (Fig.1)satisfythefollowingpropositional formulas:

1. b∨(a∧c). 2. (a∧¬c) =⇒ ¬b. 2 Question8 Let ? be the following CTL formula: AGb =⇒ AX¬E(a∨c) UNTIL b
.

1. Rewrite the formula ? into equivalent formula ?0 without AG, AX and =⇒ . We consider that the or operator,∨, is allowed in a CTL formula.

2. Give the parse tree of the rewritten formula ?0.

3. ManuallyruntheCTLexplicit-statealgorithmMarkofLecture7on?0i.e.,compute the result of Mark(B,?0), to determine whether A |= ?0 (and explain your answer).

Exercise4(SPIN)The of?cial webpage https://spinroot.com provides good overviews and manuals.

Below you ?nd a na¨ive implementation of a system with two water tanks (only the levels are modelled).There is a pump which tries to balance the levels. It succeeds if thewaterlevelsareequal. (Atext-?lecontainingthePromelaspecisavailableonline.) /* Level of the individual tanks */ int level[2]; /* Model of Pump */ activeproctype Pump() { do ::level[0]<level[1] -> level[1]--;skip;level[0]++; ::level[1]<level[0] -> level[0]--;skip;level[1]++; ::else -> break; od } /* set initial water levels */ init { level[0]=5; level[1]=49; }

Question9 Describe in English words what the processes Pump does. The ?nal goal is to have the same water levels in both tanks. In this case the pump can be switched off.

Question10 Use SPIN to check if the pump can always be switched off in the given scenario. Check if the pump can be switched off for all possible water levels.

Question 11 In case the Pump cannot be switched off, modify the system in a way that the water levels are equal at the end. Prove it. 3

Question 12 Add a process which, at some arbitrary point in time, adds non-deterministically the amount 42 to one of the tanks. Check for deadlocks.

Question13 Checkwhetheryoursystemalwaysbalancesoutthewaterlevels. Ifnot modify your system to achieve this. The pump should be switched off as soon as the water levels are equal. Use SPIN to prove it. Note: If you do experiments with SPIN, describe the procedure, provide the code and discuss SPIN's output. We want to see that you used SPIN and not a pen and paper analysis. Also note that some questions build on previous results.