Objectives:

• Master on-the-fly LTL model checking

Chapter 9 of the course text.

## Paper Pencil Problems

Consider the below solution to the dining philosopher for just two participants. Each active thread describes the state of the philosopher. Both start in the the first location, loc0. For example, in the first location of Philosopher1, when fork1 is available, then Philosopher1 sets fork1 to true and jumps to loc1 (goto loc1). The description details a transition system from which it is possible to derive a Kripke structure.

system TwoDiningPhilosophers {
boolean fork1 = false;
boolean fork2 = false;

loc loc0:  // take first fork
when !fork1 do  {
fork1 := true;
}
goto loc1;

loc loc1:  // take second fork
when !fork2 do {
fork2 := true;
}
goto loc2;

when fork2 do {
fork1 := false;
}
goto loc0;

loc loc2:  // drop second fork
when true do {
fork2 := false;
}
goto loc3;

loc loc3:  // drop first fork
when true do {
fork1 := false;
}
goto loc0;
}

loc loc0:  // take second fork
when !fork2 do {
fork2 := true;
}
goto loc1;

loc loc1:  // take first fork
when !fork1 do {
fork1 := true; }
goto loc2;

when fork1 do {
fork2 := false;
}
goto loc0;

loc loc2: // drop first fork
when true do {
fork1 := false;
}
goto loc3;

loc loc3:  // drop put second fork
when true do {
fork2 := false;
}
goto loc0;
}



Consider the following property description for the dining philosophers.

// Liveness Property:
//
//  If a philosopher picks up a fork, he will eventually release it
//  (this can be done for fork 1 or 2)
//
// LTL:
//
//    f = [] (fork1/2 --> <> !fork1/2)
1. (3 points) Write the complement of the property so it is expressed as a never-claim.
2. (5 points) Create the Buechi Automaton for the never-claim in the previous problem. Express the automaton in either a dotty format or the text format used to describe the dinning philosopher protocol above (i.e., locations with guarded or unguarded commands). Please label accept locations as locX:accept where X is a number. For example, loc1:accept.
3. (15 points) Perform on-the-fly model checking to see if our system satisfies the property (i.e., check the intersection of the model and the never claim). Please show the entire search graph as we did in class.When doing to the intersection, treat each location as as single atomic step.