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

Setup

If you still did not do it in the last TDs, you need to install some Python dependencies and GraphViz: look here.

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

Evaluation.

You will receive a maximum 20 points, subdivided as follows:

• 5 points for the GNBA to NBA conversion
• 2 points for implementing the closure operation
• 5 points for implementing the generation of the elementary set of formulas
• 7 points for the conversion of a LTL formula to a NBA

Deadline.

The deadline for submitting the exercise to obtain a full grade is Thursday May 1st at 23:59. You can submit your work after that deadline but you will receive only 50% of the total grade.

GNBAs and LTL To Buchi transformation.

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 class GNBA in src/mc308/auto/gnba.py. GNBA represents a Generalized NBA. What’s different from a NBA is the acceptance condition that is a set of sets of states in a GNBA.

You can create a GNBA as follows:

ap = [Symbol("p_%d" % int(s)) for s in range(1)]
a1 = ap[0]
GNBA([1], [(1,[a1],1)], [1], [[1]], ap)

In the file src/td5_script.py you have some simple GNBA you can use to get familiar with the representation and test the following function.

In this exercise, you will implement the function:

def gnba_to_nba(gnba : GNBA) -> NBA:
    ...

in src/mc308/td5.py. The function takes as input a GNBA and returns a NBA that accept the same language.

Computing the closure of a LTL formula

You will implement the function:

def get_closure(formula : LtlFormula) -> Set[LtlFormula]:

that, given a LTL formula, returns its closure.

In the file src/td5_script.py there are some LTL formulas you can use to test your work.

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/logics/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 arguments 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. Some operators, as and and or in pysmt allow you to have multiple children, but you can work under the assumptions they only have two children (formulas from the parser we give you ensure this).

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).

Important: in mc308/logics/ltl.py there are two useful functions already implemented for you:

• normalize_ltl: rewrites a LTL formula to only have the operator not, and, next, and until.

• get_sub: returns a set containing all the subformulas of an LTL formula.

Use them to simplify your life.

Elementary set

Implement the function:

def elementary_formulas( closure : Set[LtlFormula] ) -> Set[Set[LtlFormula]] :

that returns the set of sets of elementary formulas given the closure of a LTL formula.

HINT: here we do not care about performance. So, you can solve the problem in two steps:

1. Enumerate all the possible subsets of closure

2. Check each subset you generate to be an elementary set of formulas.

LTL to Buchi transformation

Implement the function:

def ltl2buchi(formula : LtlFormula) -> NBA :

that converts a LTL formula to a NBA (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 you defined so far!

Try your implementation on the LTL formulas defined in src/td5_script.py.

Submit your work:

You’ll have to upload the following file