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 a U b, 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. a U b
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

Our simple model-checker reads transitions systems specified using the graphviz/dot file format. Here follows a description of the drink vendor machine (depicted below):

digraph dvm {
    idle [initial="true", labels="pay"];
    coke [labels="drink"];
    sprite [labels="drink"];
    idle -> select;
    select -> coke;
    select -> sprite;
    coke -> idle;
    sprite -> idle;
}

The file specifies a graph named dvm with four nodes: idle, select, coke and sprite, and five edges. The node select is implicitly defined. The other nodes are explicitly defined. Our model-checker accepts two optional attributes on nodes:

• initial (which can have any non-empty string value) defines the initial node of the transition system. There must be exactly one initial node in the transition system.
• labels (non-empty comma-separated list of string) defines the set of atomic propositions that label the node. As an example, the declaration n [labels="a,b,c"]; defines a node n with labels a, b and c (i.e. labels set {a,b,c}).

In the specification above, the node idle is initial and labeled {pay}. The nodes coke and sprite are labeled {drink}. The node select is not labeled (i.e. it has empty label set {}).

1. Download the file model-checker.py from the GitHub repository (or directly clone the repository). Copy and paste the dvm graph above in a file dvm.dot. Then, run the command ./model-checker.py --output dvm dvm.dot true, and finally, the command dot -Tpdf -o dvm-kripke.pdf dvm-kripke.dot. Nota bene: run ./model-checker.py -h for how to run the model-checker.

2. Check that the transition system in the file dvm-kripke.pdf corresponds to the drink vendor machine depicted below.

Model-checking LTL specifications over Kripke structures

We implement the following model-checking function:

def model_check(k, formula, d):
    """ model-check LTL formula on transition system k using dictionary d for atomic 
    propositions """
    # 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 (a_neg_formula, product, run)

1. What is returned by this function?
2. Run the model-checker.py script for model dvm.dot and specification [](pay -> X(!pay U drink)) with option --output dvm. 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. Refer back to the model of the drink vendor machine that takes into account the stock of available drinks. Check that your model satisfies the two requirements above. Express in LTL that the machine is refilled infinitely often (add new atomic propositions if needed). Check that your model satisfies this property.
4. Refine the abstract 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 the program below that consists in a shared variable x and N threads that run the function increment. This function first stores the value of x in a local variable y. Then, it writes y+1 into x. We assume that each assignment is an atomic instruction.

int x = 0;

void increment()
{
    int y = x;
    x = y + 1;
}

1. Write a transition system using the graphviz/dot format explained above in a file concurrent_inc.dot. Add atomic propositions all_done and x_eq_2 that label states where all processes have terminated, and where x is equal to 2, respectively. Nota bene: the transition system should describe the state-space and transitions of the entire algorithm, taking into account the two processes and the three variables.
2. Write an LTL formula that is true on runs such that x has value 2 when the system terminates. Using the script model-checker.py, check if your formula holds on your model. What can you conclude?