# HW 11

# 1

Translate : G(¬error or F heat)

The LTL formula is not satisfied becuase errors do not always imply that the heat will go up. This is because the paths on the Kripke structure do not take into account people just opening and closing the mircowave door.

Counter-example for the Kripke structure logically:
¬ G (¬error or heat) = F ¬(¬error v F heat) = F (error and ¬ F heat) = F (error and G ¬ heat)

Counter-example State : < 3,1,2,5,3,1,2,5,3,1,2,5,3,1,2,5, ...>

# 2

Original System: the property is True

Abstracted System : the property is False

The abstract Kripke Structure does not satisfy G !(r && d) as both r and d are true in the first state, rsd. As the abstraction fails the LTL property, the original structure may or may not fail the formula

##### Abstracted

# 3

By definition:

P is an interpolant of A and B if:

1) A implies P. A is within P
2) P && B is unsatisfiable
3) P have the common variables of A and B

To satisfy P as an interpolant:
$y = 4 - x$


# 4

For the Kripke structure, the tuple contains the variable (pc, freed, oEn):


Thus it satisfies the property G !(pc=2 && freed=true) as freed is never true before executing line of code 2.

# 5
### Original

locked = false , oEn = *, got_lock = *
1: if (*) {
2: 		do {
3: 			got_lock = 0;
4: 			if (*) {
5: 				locked = true;
6: 				got_lock > 0;
7: 			}
8: 			if (got_lock) {
9: 				locked = false;
10:			}
11:		} while (*) ;
12:	}
13: do {
14: 	locked = true;
15: 	oEn = true;
16: 	if (*) {
17: 		locked = false;
18: 		oEn = false;
19: 	}
20: } while (!oEn);
21: locked = false;

Thus to verify the property that lock() is not called twice, we have to test for the LTL logic: $𝑮(!(pc==5$ && $locked ==true)$ && $!(pc==5$ && $locked ==true))$


The program will not perform a double lock at all as seen in the state highlighted above in blue, where lock() is perform and it is not locked.