TU Wien:Formale Methoden der Informatik VU (Egly)/Ausarbeitung Prüfung 2023-06-20 (fmi234)

Prüfungsangabe (fmi234.pdf)

Block 1

Block 1.a) Reduction co-HALTING to BITFLIP-HALTING

Proposed solution (2023-10-30)

To prove the correctness of the reduction we have to show that both directions of the equivalence are valid.

Proving =>

Assume that (Pi, I) is a positive instance of co-Halting, i.e: Pi does not halt on input I. We have to show that Pi1 does halt on either I1 or its inverse, or the other way around.

We know that Pi1 returns and therefore halts on the inverse of I; therefore, by construction of g((Pi, I)) Pi1 halts on I1.

Pi1 therefore needs to not halt on flip(I1) = I for g((Pi, I)) to be a positive instance of Bitflip-Halting. Because we know that Pi halts on I (and the conditional in Pi1 does not matter on input I), we know that Pi1 halts on flip(I1) = I; if it didn't it would contradict our assumption.

Therefore, we know that g((Pi, I)) = (Pi1, I1) halts on I1 = flip(I), but not on the bit-flipped string flip(I1) = I: g((Pi, I)) is a yes-instance of Bitflip-Halting if (Pi, I) is a yes-instance of co-Halting.

Proving <=

Assume that g((Pi, I)) is a positive instance of Bitflip-Halting, i.e.: Pi1 halts on I', but not flip(I').

There are two return-statements in Pi1, therefore two possible paths that can have resulted in this positive instance. We look at both of them separately:

• First return statement was reached: Due to the conditional we know that this return-statement is only reached if the input string is identical to it's flipped string (Note: intuitively, this is impossible for all strings of at least one symbol of the given alphabet). Therefore, Pi1(I) = Pi1(flip(I)) = yes, which contradicts our assumption that Pi1 halts on I but not on the bit-flipped string flip(I).
• The second return statement is reached only after Pi has been executed on S = I1 = flip(I). From the definition of Bitflip-Halting we know that a yes-instance of the problem halts on some I', but not on its bit-flipped string. Because we have seen that Pi1 halts on I1 = flip(I), we know that Pi1 therefore does not halt on flip(flip(I)) = I. The only way this can happen is if the call to Pi(S) = Pi(I) does not halt, which matches the problem description of co-Halting, q.e.d.

Block 1.b) Multiple Choice

Proposed solution (2023-10-30)

• The correctness of the reduction in (a) proves undecidability of Bitflip-Halting. True: The reduction shows that co-Halting, which is undecidable, is not harder than Bitflip-Halting. If Bitflip-Halting is at least as hard as co-Halting, it is undecidable.
• If the reduction in (a) is correct, we know that Bitflip-Halting must be semi-decidable. False: co-Halting is not semi-decidable. Furthermore, even a reduction from a semi-decidable cannot prove semi-decidability of the target problem.
• If the reduction in (a) is correct, we know that Bitflip-Halting cannot be semi-decidable. True: If Bitflip-Halting were semi-decidable, co-Halting would be semi-decidable by reducing it to Bitflip-Halting. Semi-decidability of co-Halting and the known semi-decidability of its co-Problem Halting would result in decidability of Halting, which we know is not the case.
• If the reduction in (a) is correct, we know that Bitflip-Halting cannot be decidable. True: If Bitflip-Halting were decidable, co-Halting would be decidable by way of reduction. Decidability of co-Halting implicates decidability of its co-Problem, Halting, which we know not to be the case.
• If the reduction in (a) is correct, we know that the complement of Bitflip-Halting must be semi-decidable. False: We can't know this from the reduction.
• If the reduction in (a) is correct, we know that Bitflip-Halting cannot be in NP. True: All problems in NP are decidable, but Bitflip-Halting is undecidable.

Block 3

Block 3.a) Invariant and variant generation

Let p be the following IMP program loop, containing the integer-valued program variables x, y, z:

x := n; y := 0; z := 0;
while z < n do
  x := x + 5*z;
  y := y - 5*z;
  z := z + 1;
od

Give an inductive invariant and a variant for while loop in p and prove the validity of the total correctness triple [n >= 1] p [x + y = n]

Proposed solution (2023-10-30)

Rewrite the loop body using index notation (with counter i) to find possible invariants:

x[i+1] := x[i] + 5*z[i];
y[i+1] := y[i] - 5*z[i];
z[i+1] := z[i] + 1;
z[i] := i;
x[i] := x[0] + 5*(i-1);
y[i] := y[0] - 5*(i-1);

Rewriting to sum notation yields $x=n+5*\sum _{i=0}^{z-1}i=n+5*{\frac {(z-1)*z}{2}}$ and $y=-5*\sum _{i=0}^{z-1}I=-5*{\frac {(z-1)*z}{2}}$. We additionally encode n = x + y, as seen in the postcondition, to express a relationship between all variables in the invariant: $I=(x=n+5*{\frac {(z-1)*z}{2}})\land (y=-5*{\frac {(z-1)*z}{2}})\land (n=x+y)$

To prove termination required by total correctness, we further need a loop variant that is positive before each iteration, and strictly decreasing with each iteration. Because z is used as a loop index counter and n indicates the maximum number of iterations, we chose $t=n-z,t_{0}=n$

We now need to show that $VC(p,B)\land (A\Rightarrow wp(p,B))$ holds for A: n >= 1, B: x + y = n.

${\begin{aligned}A\Rightarrow wp(p,B))&=A\Rightarrow wp(x:=n;y:=0;z:=0;while\dots ;,x+y=n)\\&=A\Rightarrow wp(x:=n;y:=0;z:=0;,I)\\&=A\Rightarrow wp(x:=n;y:=0;,(x=n)\land (y=0)\land (n=x+y))\\&=A\Rightarrow wp(x:=n;,(x=n)\land (0=0)\land (n=x))\\&=A\Rightarrow (n=n)\land (0=0)\land (n=n)\\&=n\geq 1\Rightarrow (n=n)\land (0=0)\land (n=n)\end{aligned}}$

${\begin{aligned}VC(while\dots ,B)&=(I\land \neg b)\Rightarrow B\\&\land (I\land b)\Rightarrow t\geq 0\\&\land (I\land b\land t=t_{0})\Rightarrow wp(p_{loop},I\land t<t_{0})\\&\land VC(p_{loop},I\land t<t_{0})\end{aligned}}$

${\begin{aligned}(I\land \neg b)\Rightarrow B&=(x=n+5{\frac {(z-1)*z}{2}})\land (y=-5{\frac {(z-1)*z}{2}})\land (n=x+y)\land z\geq n\Rightarrow n=x+y\\&=n=x+y\Rightarrow n=x+y\end{aligned}}$

${\begin{aligned}(I\land \neg b)\Rightarrow n-z\geq 0&=(x=n+5{\frac {(z-1)*z}{2}})\land (y=-5{\frac {(z-1)*z}{2}})\land (n=x+y)\land z<n\Rightarrow n-z\geq 0\\&=z<n\Rightarrow n-z\geq 0\end{aligned}}$

${\begin{aligned}VC(x:=x+5*z;y:=y-5*y;z:=z+1;,I\land t<t_{0})&=\top \end{aligned}}$

Thus, we have proven the total correctness triple.

Block 3.b) Weakness of assertions

Proposed solution (2023-10-30)

$A_{1}:wlp(\mathbf {abort} ,B)=true;A_{2}:wlp(\mathbf {skip} ,B)=B$

Definition of Weaker and Stronger Assertions:

• A is weaker ("more states satisfy it", "easier to satisfy") than B iff B => A.
• A is stronger ("less states satisfy it", "harder to satisfy") than B iff A => B.

B => true is valid, while true => B is harder to satisfy given that B is non-trivial. Therefore, A1 is weaker than A2.

Block 3.c) Find states for Hoare Triples

Proposed solution (2023-10-30)

Computing the wlp(p, x > y) can assist in coming up with possible states: $wlp(p,x>y)=(x\neq y\Rightarrow 3y>9y)\land (x=y\Rightarrow 4x>2x)$. Due to the given precondition we can ignore the second implication (and the else-path of the program). y > 3y intuitively holds for any y < 0.

a) $\sigma _{1}\models \{x<y\}p\{x>y\}:\sigma _{1}(x)=-3,\sigma _{1}(y)=-1$

b) $\sigma _{2}\not \models \{x<y\}p\{x>y\}:\sigma _{2}(x)=1,\sigma _{2}(y)=3$

Block 4

Block 4.a) Simulations between Kripke structures

Proposed solution (2023-10-30)

i) M2 simulates M1. Simulation relation: $H=\{(t_{0},s_{0}),(t_{4},s_{1}),(t_{5},s_{1}),(t_{1},s_{3}),(t_{2},s_{2}),(t_{6},s_{3}),(t_{3},s_{2})\}$

ii) M1 does not simulate M1:

The self-loop in s1 requires states in which b holds to have a successor in which b also holds, which is not the case for t3.

Formally: For s1, there is no t' in SM1 in such that (t3, t') is in RM1 and (s1, t') is in H for (s1, s1) in RM2.

Block 4.b) Multiple Choice: CTL* Formulas

1 $\mathbf {X} (\neg a\land c)$

	CTL
	LTL
	CTL*
	s0
	s1
	s2
	s3
	s4

2 $\mathbf {E} [(b\land c)\mathbf {U} (a)]$

	CTL
	LTL
	CTL*
	s0
	s1
	s2
	s3
	s4

3 $((b\land \neg c)\mathbf {U} (a))$

	CTL
	LTL
	CTL*
	s0
	s1
	s2
	s3
	s4

4 $\mathbf {EX} (\neg b\land c)$

	CTL
	LTL
	CTL*
	s0
	s1
	s2
	s3
	s4

5 $\mathbf {EG} c$

	CTL
	LTL
	CTL*
	s0
	s1
	s2
	s3
	s4

States verified using forsyte.at Kripke Builder

Block 4.c) LTL Tautologies

i) $\mathbf {G} ((\mathbf {F} b)\land \neg a)\rightarrow \mathbf {G} (\neg a\mathbf {U} b)$

Tautology.

Proof:

$\mathbf {G} ((\mathbf {F} b\land \neg a)$: For all states >= 0: There exists a k >= 0 such that state k on the path models b. The state models !a.

$\mathbf {G} (\neg a\mathbf {U} b)$: For all states >= 0: There exists a k >= 0 such that state k on the path models b, and for all 0 <= j < k state k models !a

The existence of a future state modelling b satisfies the definition of U regarding b. Because all states model !a, clearly all states before this future state also model !a.

ii) $\mathbf {G} (\neg a\mathbf {U} b)\rightarrow \mathbf {G} ((\mathbf {F} b)\land \neg a)$

Not a tautology: Counterexample: L(s0) = {}, L(s1) = {a, b}, R = {(s0, s1), (s1, s1)}