Second Edition Logic in Computer Science: Modelling and reasoning about systems Solutions to designated exercises MICHAEL HuTH and MARK RYAN ~ ) B 1 +a premioe v~ 3 on @® @ 4 q 1,3 “ YY) 5 1 7e4.2 6 sp aid-5 Q Ne s = alt]; 1 while (k != nti) { @) \ t= min(e+ale], afk]; & \ s = min(s,t); \ k= ke; ®) | |h @ \ \ \\ (ws) \ \ —\\\ o10 Propositional logic A(y)- We prove the validity of (pq) V (p Ar) k pA (qv) by 1 (ADV (PAr) premise a PAG ‘assumption 3 p Ae 2 4 q Aen 2 5 avr Vind 6 PA(@Vr) A353 7 pAr ‘assumption 8 P Aer T 9 r Nep7 10 qvr Vin 9 uw PA(@Vr) Ai8,10 2 pA(@QVr) Ve 1,2—6,7—11 2(a). We prove the validity of sp + -qt q+ p by ~p+-q_ premise q ‘assumption qi? ~p MY 1,3 P red q>p 2-5Propositional logic 19 a pag ma (Pha) PY (79> (AQ) p> (pv (m9 (PAg))). Note that ~g and ~-y are two different subformulas. 3(a). An example of a parse tree of a propositional logic formula which is ‘a negation of an implication: ©) 3(c)- An example of a parse tree of a formula which is a conjunction of conjunctions is28 Propositional logic = [n+ tien = tye uu) guarantees that our claim holds for n +1. Note that the first step of this computation also uses that multiplication with a positive number is monotone: x > y implies 2-2 > 2+ y. 8. The Fibonacci numbers are defined by it it Fut Fao foralln > 2 (15) We use mathematical induction to prove that Fj, is even for all nel 1. Base Case: For n = 1, we compute Fy = Fy = Fa + Fi by (1.5), but the latter is just 1+ 1 = 2 which is even. 2. Inductive Step: Our induction hypothesis assumes that Fn be even. We noed to show that Fy(q.11) is even as well ‘This is a bit tricky as we have to decide on where to apply the inductive definition of (1.5): Print) = Fans Fona}t = Fina + Feanaz-1 by (1.5) Fonsiist + Pint = (Fine + Fin) + Fanti unfolding Figy.+1)41 with (1.5) = 2 Pong t Fine Since Fj, is assumed to be even and since 2+ Fjn,41 clearly is even, we conclude that 2: Fsn41-+ Fin, and therefore F41)+ is even as well. Note that it was erucial not to unfold Fin41 as well; otherwise, wwe would obtain four summands but no inductive argument. (Why?) 10. Consider the assertion “The number n? + 5n +1 is even for all n > 1" (a) We prove the inductive step of that assertion as follows: wePredicate logic (v) x; again, we can't nest predicates (B, $ are predicates) (wi) ¥ (vii) ¥ (vill) %; again, we can't nest predicates. A(a). ‘The parsetres is a746 Predicate logic 12. We prove the validity of $ > Vr Q(c) t Vz ($ > Q(2)) by S-+¥eQ(e) prem zo Ss ve Qle) Qx0) $+ Qo) 7 Va(S + Q(x)) Vai2-6 13(a). We show the validity of Ve Plo), Vey Ye (Pla.142) + P(f(0),¥ fe) + PCfl@),4, flo) by 1 Ve Pla,.2) prem 2 Wa Wy Wz (Pl2,y,2) + PU (2) uJ(2))) prem 3 Plane) Vee1 4 Wy V2 (Pla, y,2) > P(f(a),y,f(2))) Vee? 5 V2 (Pla,a,2) + PUs(a),a, f(2))) wed 6 P(a,a,e) ++ P(F(a),a, F(a) Ve05 7 P(f(a).4, f(a) ~106,3 13(b). We show the validity of VaP(a,x,2), Vay V2 (P(x, 9,2) > PU), yf (2))) + 32 PUF(@), 2 F(F(@)) by 1 veP(a,2,2) prem 2 Va Vy V2 (P(2,y,2) + P(f(#).¥sf(2))) prem 3 Pla, f(a), f(a)) Vane 1 4 Wy ¥2 (P(a,y.2) > PUF(@),9, F(2))) Vee2 5 v2 (P(a, f(a),z) + P(f(a), f(a), f(2))) Wye 4 6 Pa, f(a), F(a) > P(F(@), fla), f(F(@))) Vee 7 P(F(@), f(a), FUF(@)) 90 6,3 8 Sz P(f(a),2,f(f(a))) Bei?Predicate logic 55 fun Commutes (6: Group) { all a,b: [Link] | a.(b.([Link])) = b.(a.([Link])) } run Conmutes for 3 but 1 Group assert Conmutative { all G: Group | Commutes(G) } check Commutative for § but 1 Group ii, Analyzing the assertion above we find no solution. ‘The small- scope hypothesis therefore suggests that all finite groups are com- mutative. 'This time, the small-scope hypothesis got it wrong! ‘There are finite groups that are not commutative. iii, In fact, increasing the scope from 5 to 6 reveals a violation to our goal. Please run this analysis yourself and inspect the navigable tree to determine where and how commutativity is broken. 6(e) Yes, the assertions are formulas that make a claim about all groups. Soa counter-example exists iff it exists for a single group. We already achieved the restriction to one group with the but 1 Group in the check and run directives64 Verification by model checking end case end function ‘You can now prove, by mathematical induction on the height of ¢'s parse tree, that the call TRANSLATE ¢ terminates and that the re- sulting formula has connectives only from theset {, >, A, AF EU, EX } EXBROISES 3.5 (p.250) 1(a). The process of translating informal requir tions is subject to various pitfalls. One of them is simply ambiguity, For example, it is unclear whether “after some finite steps” means “at least one, but finitely many steps”, or whether zero steps are al- lowed as well. Tt may also be debatable what “then” exactly means in“... then the system enters ...”, We chose to solve this problem for the case when zero steps are not admissible, mostly since “fol- lowed by” suggests a real state transition to take place. The CTL formula we came up with is AG (p 3 AX AG (-gv 4 which in LTL may be expressed as GQ XG(-qV -r UA). rents into formal speeifiea- or Ut) Tt says: At any state, if p is true, then at any state which one can reach with at least one state transition from here, either qis false, or r is false until t becomes true (for all continuations of the computation path). ‘his is evidently the property we intent to model. Variaous other “equivalent” solutions can be given. 1(f). The informal specification is ambiguous. Assuming that we mean & particular path we have to say that there exists some path on which pis true every second state (this is the global part). We assume that the informal description meant to set this off such that p is true at the first (current), third etc. state. The CTL* formula thus reads E[G(p A XX p)]- Note that this is indeed a CTL* formula and you can check that it insists on a path so > 81 ~ sy > -.. where 59,82, 84,--- all satisfy P.Verification by model checking B # The function Hy is not montone: e.g. {2} © {2,5}, but Hy({2}), which is {5,9}, is not a subset of Hp({2,5}), which is {9}. * The fumetion Hy is monotone since union and intersection are monotone and the composition of monotone operations is again monotone. 1(b). We compute the least and greatest fixed-point of Hs with just one iteration each: it is {2,4} in each of these cases. So why can we say that this is the only fixed-point of Hy? 2(a) Let X CX’ and s € F(X). Then s € AN F(X) implies s € A and 5 € F(X). So in order to show s € Fi(X") = AN F(X) it sulfices to show s € F(X"). But this follows from s € F(X) as XC X" and since F is monotone. XX" and consider s € F(X) o Ifs€A, then s€ AU(BA F(X’) = F(X’) follows. «Is ¢ A, then s € F(X) = AU(BNF(X)) implies s € BN F(X), but we already saw in item (a) that this implies s € BO F(X’) and so s € AU (BN F(X’) = Fa(X") does it. 5. © Let X CX" and # € H(X) = [6] {40 € S| sy + s1 implies #1 € X}. Then s € [@] is clear. If se S with s > s', then s © H(X) implies #” € X. Since X C X', we infer from that s! € X’. But this shows # € [g] M {sp € 5 | so + s1 implies sy € X"} = H(X') © We compute 2b) I H(IAG d]) = [4] {80 € S| 50 + 81 implies s; € [AG ¢]} = [A] NIAXAG 4] [acd]. © We have already seen that [AG 6] is a fixed point of H. To show that it is the greatest fixed point, it suffices to show here that any set X with H(X) = X has to be contained in [AG g]. So let so be an element of such a fixed point X. We need to show that so is in [AG g] as well. For that we use the fact that so € X = H(X) = [¢] {8 € S| s+ 1 implies «1 € X} to infer that s; € X for all s; with so —+ 5). But, since 5; is in X, we may apply that same argument tos; € X = H(X) = [0] 0 {s € S| ss implies sy € X} and we get 52 € X for all sz with s, —+ s2. By mathematical induction, we can therefore. show that s, € X, where sy is any state that is reachable from s Since all states in X satisfy 4, this means that # is in [AG g].92 Program verification (r20) (G-(@) = a) (20) Implied anx; (Q-@) =a) A@20)} Assignment yrt ((y- (a!) = 2!) N(a@ 2 O)} Assignment while @>0 { ((u- @!) =a!) A(a>0)A(a>0)) Invariant Hyp. A guard ((y- (a= 1)!-a) = 21) A(a~1>0)) Implied (((y-@)- ((a—1)!) = at) A(a—120)) Implied yrytas ((y- ((a—1))) =a!) A(a-1>0)) Assignment asa-1 {(y- (a) = 2!) A (a= 0)} Assignment t ((y- (a!) = 2!) A (a 20) A~(a > 0)) =a) Note that we had to strenghten our invariant hypothesis by adding conjunct (a > 0). ‘This was needed since =(a > 0) does not in itself imply the desired (a = 0) to secure that our invariant implies the postcondition 21(a). We simulate the code for each of these arrays in a table which listsModal logics and agents a1 P : 4 ‘The world b satisfies p 00g, since ¢ f p. For the worlds a and 6, we have alk p and ¢ Ik p, so we need to secure a Ik 0g and ct 00g. But this can be done, since all three worlds, 2, of this model have an immediate successor state, 2’, such that a! Ik q. (Why does this imply what we require, and what choices of 2! for © would you make?) © We seek 2 model in which p + 00q is not true. By definition, we seek & model in which not every world satisfies p > 30g. The model in Figure 5.5 of the textbook qualifies, for a f p + 104. (Why?) 5(d). The relation z Ik O(p Aq) means that there is a world y with R(r,y) and y lt p Ag. On the other hand, x Ik Op A Oq means that there are worlds ¥/ and y/" with R(2,y!) and y! kp R(x,y") and y" te @. With that in mind, it is relatively easy to find a model which distin- sguishes these two formulas: Note that af O(p Aq), whereas a it Op A Og.100 Modal logics and agents We make use of the second part. of Theorem 5.26. ‘Thus, if y is, any world which is G-reachable from « within I steps, we have to argue that y It Cq@, ie. y Ik BE¢ for all k > 1. Fix any k > 1. If 2 is G-reachable from y within k steps, we are done if 2 IF g. But since y is G-reachable from # within I steps, we conclude that 2 is G-reachable from z within I+ & steps. But then our assumption that z It Cod implies x Ik Eff*¢ which renders z + 6. ‘Thus, Jag -+ CaCo@ is valid im KTS, © To show that -Ced + Ca-Cag¢ is valid in KT45, it suffices to consider an arbitrary world x in an arbitrary model of KTS such that x Ik ~Caq. We then only have to show that x It Cg~Cad follows. We make crucial use of the second part of Theorem 5.26, and apply proof by contradiction: Assume that x If Og—Ca¢. By Theorem 5.26, there exists a world y which is G-reachable by such that y ¥ “Cad, ie. y Ik Cad. Since G is non-empty (what does =Cod + Ca~Cod mean if G is empty, and why it is then valid?), we know that the relation Ur (5.1) 10 is an equivalence relation (see the discussion in the textbook after ‘Theorem 5.26). But then « and y are related via this equivalence relation and one satisfies Ca, whereas the other one does not. This is a contradiction. (Why?) 10(c). Again, we prove this via showing two separate implications. (i) We prove Cp ++ KiC, by Cp ass cep cat ECp CE2 KiCp EK 3 Cp> Kp il-4 This follows simply by the rule K’ 10(e). The formula scheme =9 + Ky>K.d means “If @ is false, then agent knows that he does not know ¢.”