Model-checking LTL specifications

We will use the tool Spot to write an LTL model-checker in Python. The LTL modalities are denoted: [] “Always”, <> “Eventually”, X “Next” and U “Until”. Boolean operators are written: ! “Not”, & “And”, | “Or” and -> “Implies”. Atomic propositions are strings, like "a", "b", etc. The true formula is denoted true, and false denotes the false formula.

Translating LTL formulas into Büchi automata

For each of LTL formula Φ below, compute a Büchi automaton using Spot tool ltl2tgba, and associate to each state the maximal coherent subset of the subformulas of Φ that are true in any accepting run from that state.

NB: use the command ltl2tgba -Bd -f 'a U b' | dot -Tpdf -o aUb.pdf to compute a Büchi automaton for the formula aUb, and obtain a graphical representation of the automaton in the PDF file aUb.pdf. Add option -C to ltl2tgba to obtain a complete automaton.

1. aUb
2. ⋄a (compare to the previous automaton)
3. □a (compare to the previous automaton)
4. ⋄□a
5. □⋄a
6. □(a ⟹ ⋄b)

Defining a transition system

In order to simplify our model-checker, transition systems will be defined directly in python using Spot libraries. Labelled transition systems are often called Kripke structures. Here is an example of the definition of a Kirpke structure using Spot libraries, where bdddict is a dictionnary implemented using Binary Decision Diagrams (BDDs) that maps atomic propositions (i.e. strings) to identifiers.

def create_kripke_dvm(bdddict):
   k = spot.make_kripke_graph(bdddict)
   pay = bdd_ithvar(k.register_ap("pay"))
   drink = bdd_ithvar(k.register_ap("drink"))
   s_idle = k.new_state(pay & -drink)
   s_select = k.new_state(-pay & -drink)
   s_coke = k.new_state(-pay & drink)
   s_sprite = k.new_state(-pay & drink)
   k.set_init_state(s_idle)
   k.new_edge(s_idle, s_select)
   k.new_edge(s_select, s_coke)
   k.new_edge(s_select, s_sprite)
   k.new_edge(s_coke, s_idle)
   k.new_edge(s_sprite, s_idle)
   k.set_state_names(['idle','select','coke','sprite'])
   return k

Download the file model-checker.py, and run the command ./model-checker.py --output drink-vendor-machine true. Then, run the command dot -Tpdf -o drink-vendor-machine-kripke.pdf drink-vendor-machine-kripke.dot to get a graphical representation of the Kripke structure defined above in the PDF file drink-vendor-machine-kripke.pdf.

1. Open the file drink-vendor-machine-kripke.pdf and explain the instructions in the create_kripke_dvm function above.

Model-checking LTL specifications over Kripke structures

We implement the following model-checking function:

def model_check(model, formula):
    """ model-check model w.r.t. LTL formula """
    d = spot.make_bdd_dict()
    # Create the Kripke structure
    k = create_kripke_structure(model, d)
    # Create the automaton for the negation of the formula
    neg_formula = "!(" + formula + ")"
    a_neg_formula = build_automaton(neg_formula, d)
    # Compute the product
    product = spot.twa_product(k, a_neg_formula)
    # Check emptiness of the product
    run = product.accepting_run()
    return (k, a_neg_formula, product, run)

1. What is returned by this function?
2. Run the model-checker.py script for model drink-vendor-machine and specification [](pay -> X(!pay U drink)) with option --output. Produce PDF files from the .dot files output by the script. Explain what you observe in the three files.
3. Proceed similarly with specification [](pay -> !pay U drink)

Model-checking the drink vendor machine

1. Does the combination of requirements [](pay -> X(!pay U drink)) and [](drink -> X(!drink U pay)) ensures that one cannot get a drink without paying and one is guaranteed a drink after having paid?
2. Check that the drink vendor machine is correct: one cannot get a drink without paying, and one is guaranteed a drink after having paid.
3. Refine the model to deliver drinks only after 2 euros have been paid. Coins of 0.5 euros, 1 euro and 2 euros can be used. The drink vendor machine does not make change. Check that your new model satisfies the requirements above.

Model-checking a concurrent algorithm

Consider a concurrent algorithm with one shared integer-valued variable x, and two processes:

variable
  x = 0;

process (P = 1)
variable
  y = 0;
{
p0: y := x;
p1: x := y + 1
}

process (Q = 2)
variable
  y = 0;
{
q0: y := x;
q1: x := y + 1
}

1. Implement a python function create_kripke_shared similar to function create_kripke_dvm that defines the Kripke structure corresponding to the model above. Update the function create_kripke to call function create_kripke_shared when model shared is selected. Add an atomic proposition to observe whether x=2.
2. Using the script model-checker.py, check if x is equal to 2 when the system terminates.