Model Checker in ML

Summary of Data and information for your program

Pnet for moderated meeting FSM model CTL formulae

Check your program against Clarke's original

Turn in your work via the Web. Make an area that I can read and put all the code and supporting documentation in it Make sure your directory has a "README.txt" file explaining what is there and how to use it.

You may use the assignment data area as an example.

Input parsing

You may use "" to parse the input file "meet.fsm". You may wish to do your own parsing, that is up to you.

Here is a version of "" for the later ML version. Thanks to Chris Vanderknyff for this one.

Run on this Data

Pnet for moderated meeting FSM model CTL formulae

The model we will check is a protocol for managing a moderated meeting. The "Pnet" link above is a PS file you can print to see the Petri Net for this protocol.

I have converted the Petri Net into an annotated FSM for model checking analysis, also available above at the "FSM" link.

Finally, you must run your model checker on the model to check the temporal formulae found at the "CTL" link above.

Check your work against Clark's model checker

Access the mcb code and data and look at the README.txt file for explanation of what to run and what data to use.

Code a CTL Model Checker in ML

Note the information below about what input notation you MUST deal with, and what extensions you may deal with for extra credit.

The Concept

Your program will take text as input and generate text as output.

Inputs will be:

Output will be:

Input Model Format

The model is a text file that contains descriptions of:


   STATES   8 
   ARCS     12
   ATOMIC   welcome, overview, shuttle, engines, allow, inhibit,
            begin, orbiter, propulsion, begin2, return, remove
   #0   100010100000
   #1   010010011000
   #2   010101000011
   #3   000110000010
   #4   110001100001
   #5   010001000001
   #6   011001000101
   #7   001010000100


The Temporal Logic Language CTL

CTL is a subset of the CTL* temporal logic notation.
In CTL, only certain combinations are allowed of the A/E path quantifiers with the G/F/X/U temporal operators.

Note that if you do some rewriting on your formulae as they come from keyboard input, you can implement a subset of the operators in the CTL language. The "*" appears next to the operations above that constitute a complete set according to Clarke's paper.

The REQUIRED functionality is to accept and check the reduced notation (the "*" operators above). You may assume that all CTL formulae have been translated into these operators by the user.

You may wish to make your implementation deal with the full CTL notation as input, and do the reduction/translation in the checker... it's your choice.

As examples of rewriting, consider:

  EF(p1) -> AG(p2)
can be re-written as
  ~EF(p1) | AG(p2)
  ~EU(true,p1) | ~EF(~p2) 
  ~EU(true,p1) | ~EU(true,~p2)     
  ~(EU(true,p1) & EU(true,~p2))
This uses only the ~, &, EU operators

The Algorithm

Your best reference is this paper by Clarke, et al. in which an algorithm is outlined. We want to determine if f0 is true in the structure M = (S,R,P).

The algorithm operates in stages:

At end of stage i each node in the graph will be labeled with the forumlae of length <= i that are true there. We call this set of formulae label(s) for node s.

Other primitives:

Here is an abstract of their algorithm:
proc label_graph (f) is
  handles 7 cases depending on whether f is atomic or has one
  of these forms:
    ~f, f1 and f2, AXf, EXf, A[f1 U f2], E[f1 U f2]
  (* case where operator is AU *)
    for all s in S { marked(s) := false }
    L: for all s in S { if ~marked(s) au(f,s,b) }

proc au (f,s,b) is
  if marked(s) {
    b := labeled(s,f);
  marked(s) := true ;
  if labeled(s,arg2(f)) {
    add_label(s,f) ;
    b := true ;
    return ;
  } elsif ~labeled(s,arg1(f)) {
    b := false ;
    return ;
  for all s1 in successors(s) {
    au(f,s1,b1) ;
    if ~b1 { b := false; return  }
  b := true;
  return ;