CSE308 - Tutorial 5 - GNBAs and LTL To Buchi transformation.

Setup

Setting up the tutorial.

Download and extract the files of the tutorial CSE308-TD5-1-handin.zip. You’ll have a folder called CSE308-TD5-1-handin.

If you did not work on the previous tutorials, you need to install the python packages contained in the requirements.txt file with pip

$ cd src
$ pip install -r requirements.txt

In case you have conflicts installing the packages versions, you can try with a python environment (or with anaconda).

Installing pysmt on the lab machines

1. Install the python pysmt package

$ pip install pysmt

The command will install pysmt in your home directory.

2. Install the BDD package and Z3 (SAT solver that we will use next week)

$ ~/.local/bin/pysmt-install --bdd

$ ~/.local/bin/pysmt-install --z3

Evaluation.

You will receive 100 points, subdivided as follows:

• 30 points for the GNBA to NBA conversion
• 40 points for the functions on LTL formulas
• 30 points for the conversion of LTL to an GNBA

Deadline.

The deadline for submitting the exercise to obtain a full grade is on Friday March 28 at 23:59 (i.e., in about two weeks, since next week there is no class). You can submit your work after that deadline but you will receive only 50% of the total grade.

De-generalize a Generalized Buchi Automata (GNBA)

Implement the procedure that construct a Non-Deterministic Buchi Automata (NBA) from a Generalized Buchi Automata (GNBA).

Look at the classes NBA and GNBA in mc308/data_structures/nba.py:

• NBA is the same class we used in Tutorial 3.

• GNBA is a class that represent a Generalized NBA. What differs in both classes is the acceptance condition, which is a set of states in a NBA and a set of set of states in a GNBA.

So, for example the following code is the GNBA we saw in class:

G = GNBA(set([0,1,2]),
         set(["green,red"]),
         [(0,TRUE(),0),
          (0,Symbol("red"),1),
          (0,Symbol("green"),2),
          (1,TRUE(),0),
          (2,TRUE(),0)
          ],
         set([0]),
         set([frozenset([1]),frozenset([2])])
         )

Here we also make our life easier and we directly use propositional formulas to label the automata transitions. So:

• Symbol("red") just creates the atomic proposition red (and similarly, Symbol("green")).

• And TRUE() is just the formula \(\text{true}\), meaning you can take that transition with any letter of the alphabet (i.e., any \(a \in 2^{AP}\)).

Both Symbol and TRUE() are from the PySMT library we use to represent formulas.

Your task in this exercise is to implement the function:

def to_nba(self: GNBA) -> NBA:
    ...

in the GNBA class. The function takes as input a GNBA and returns a NBA that accept the same language.

Inputs to test your solution are here mc308/tests/test_gnba.py. You can run the test from the tutorial directory with the command:

pytest mc308/tests/test_gnba.py 

The result to compare with is not provided. Test your solution adding a function to compare NBAs. Clearly, do not try to implement language equivalence, which would require you to implement the NBA complement operation, but provide some high-level comparisons (e.g., same set of initial states, same set states, same transitions modulo re-ordering of the final acceptance sets).

Also, for debugging you use the function nba_to_dot that prints both a NBA and GNBA (WARNING the dot representation for a GNBA just shows with a circle all the states that are accepting in some acceptance condition, so you need to be careful about that).

Submit your solutions

Fun with LTL formulas

In this exercise we will just get familiar with the formula representation and how we can manipulate formulas. Technically, we use the formula reprsentation from the PySMT python package, which can represent propositional logic and some extensions of First-Order logic which we do not care, and we extended it to represent LTL formulas, adding the temporal operators X, F, G, and U.

The LTL grammar we use is similar to the one used in SMV, with X, G, F, and U as temporal operators, and &, |, !, ->, <-> as boolean operators.

“Normalize” a LTL formula

Implement the function normalize_ltl in mc308/data_structures/ltl_functions.py that takes as input a LTL formula containing also the boolean operators Or, Implies, Iff, and the temporal operators F, G, and returns an equivalent LTL formula containing only the boolean operators Not, And and the temporal operators X, and U:

def normalize_ltl(formula : LtlFormula, env = get_env()) -> LtlFormula:
  ...

Some hints: your function can look something like this (the following is a non-well defined pseudo code, not Python!):

if formula is an atomic proposition:
  return formula

elif formula is True
  return True

...

else if formula is the or psi | phi:
  return Not(Not(normalize_ltl(psi)) and Not(normalize_ltl(phi)))

else if formula is the and operator psi & phi:
  return And((normalize_ltl(psi)) and (normalize_ltl(phi)))

... like this for all your operators!

You can check if a formula is a specific operator with the PySMT functions in fnode.py. In practice, you have functions you can call on your formula such as is_true(), is_false(), is_symbol() (for checking that you have an atomic proposition), and is_not(), …, for checking your formula starts with a not operator. Recall, formulas are represented as a tree, where the root node is the operator …

For LTL you can use the functions is_ltl_U, is_ltl_X, is_ltl_F, is_ltl_G (which we provided for you, so they are not in fnode.pybut in mc308/data_structures/ltl.py). Just call them on your formula object (e.g., formula.is_ltl_X returns true if the top-level operator in your formula is a X).

To get one of the argument of a formula, you can use formula.args(), which returns an array of arguments. So, formula.args() of the formula ! (a) will contains one argument, a, which you can access as formula.args()[0]. If your operator is binary (e.g., until) you will have two arguments.

Also, look in shortcuts.py. There are functions for building a particular operator (e.g., TRUE() creates the true constant, And(left,right) creates the and of the two formulas left and right, …). So, for example And(Symbol("a"), Not(Symbol("b"))) creates the formula a & !b). For LTL operator, you can use the functions LTLX, LTLF, LTLG, and LTLU (so, LTLX(Symbol("a")) creates “X a” and LTLU(LTLX(Symbol("a"), Symbol("b"))) creates the formula “(X a) U b”. `

Note: in mc308/data_structures/ltl.py there is alrady an implementation for the normalize function that uses visitor classes from PySMT to navigate the formula. Clearly, your solution should not use these additional classes.

You can test your solution with:

pytest mc308/tests/test_ltl.py::TestLTL::test_normal_form

Get all sub-formulas

Implement the function:

def get_sub(formula : LtlFormula, env = get_env()) -> Set[LtlFormula]:
    ...

that visits a formula and collects in a set all its subformulas (hint: you need a recursive function similar to the normalization.

You can test your solution with:

pytest mc308/tests/test_ltl.py::TestLTL::test_subs

Elementary set

Implement the function:

def get_elementary(closure : Set[LtlFormula]) -> Set[Set[LtlFormula]]:
    """ Returns the set of all the elementary formula for clousure """
    raise NotImplementedError()

in the mc308/data_structures/ltl_functions.py.

HINT: here, we clearly do not care about performance and scaling to real example. You can solve the problem in two steps:

1. Enumerate all the possible subsets of closure

2. Check each subset for the condition to be an elementary formula.

That’s it, you can implement a function:

def is_elementary(closure : Set[LtlFormula], B : Collection[LtlFormula] ) -> bool:
    """
    Returns true if the subset B of formula is elementary.

    Recall, a subset of closure is elementary if:
    1. it is consistent w.r.t. propositional logic:
      1.a for all \psi \in closure:
        - \psi \in B => \neg \psi \not \in B

      1.b for all \psi_1 land \psi_2 \in closure:
        - \psi_1 land \psi_2 \in B <=> \psi_1 \in B and \psi_2 \in B

    2. it is locally consistent wrt until
      - for all \psi_1 U \psi_2 in closure:
        2.a if \psi_2 in B => \psi_1 U \psi_2 must be in B
        2.b if \psi_2 \not \in B and \psi_1 U \psi_2 in B  => \psi_1 \in B

    3. it is maximal:
      - for all \psi in closure, \psi \in B => \neg \psi \in B

    """

    raise NotImplementedError

You can test your solution with:

pytest mc308/tests/test_ltl.py::TestLTL::test_elementary

Submit your solutions

LTL to Buchi transformation

In the file mc308/data_structures/ltl2buchi.py, implement the function:

def ltl2buchi(ltl :  LtlFormula) -> GNBA:
    raise NotImplementedError

that converts a LTL formula to a GNBA (assume that the set of atomic proposition is the set of proposition you find in the formula, i.e., the atomic propositions that are a sub-formula of the LTL formula). Of course, use all the functions we defined so far!

You should test your construction on, at least, the following tests:

pytest mc308/tests/test_ltl.py::TestLTL2Buchi::test_Xa

pytest mc308/tests/test_ltl.py::TestLTL2Buchi::test_aUb

pytest mc308/tests/test_ltl.py::TestLTL2Buchi::test_XU

WARNING: you need to write a function to check that your final result is correct. Now, in the test function you only get some inputs you can try and not the expected result. You can do several things (e.g., inspect the result you get, test that you get the right initial states and the right final states, …)

Submit your solutions