CSE308 - Tutorial 5 - GNBAs and LTL To Buchi transformation.
In this tutorial you will understand better the construction of a GNBA from a LTL formula, a key step for reasoning about LTL.
Setup
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 (10 for exercise 1 and 10 for exercise 2).
1. From LTL to GNBA
In this first set of exercises you will work on pen and paper to understand the different step in the construction of an LTL formula to a GNBA.
You can submit the answer to the following questions in a pdf file
(named ltl.pdf with your answers).
Consider the following LTL formulas:
\(\varphi_1 := (\mathcal{X}\ \mathcal{X}\ a)\ \mathcal{U}\ b\)
\(\varphi_2 := ( a \land \mathcal{X}\ a)\ \mathcal{U}\ (a \land \neg \mathcal{X}\ a)\)
\(\varphi_3 := \mathcal{F}\ (a \leftrightarrow \mathcal{X}\ \neg a)\)
For each formula \(\varphi\), perform the following steps:
Write the elementary sets of formulas for \(\varphi\).
Recall the examples we saw in class where we enumerated the elementary sets with something similar to a “truth” table.
Construct a generalized Büchi automaton \(G_\varphi\) such that \(\mathcal{L}(G_\varphi) = \text{Words}(\varphi)\).
Construct a NBA \(A_\varphi\) such that \(\mathcal{L}(A_\varphi) = \mathcal{L}(G_\varphi)\).
2. Implement the LTL to Büchi construction
The file td5_script.py gives you some hint to run the
function you will implement. For example, there are some LTL formulas
you can use to test your work. As for the last TDs, you will also submit
your td5_script.py file with the code you added to test
your work.
2.1 Compute 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.
We provide you with a parser for LTL formulas and a representation of LTL formulas in PySMT. Conceptually, all the formulas are represented as an abstract syntax tree where leaves are atomic propositions or Boolean constrants and nodes of the tree are Boolean and temporal operators (in practice, formulas are represented as a direct acyclic graph sharing common subformulas).
You will need to check if the top-level operator of the formula
(i.e., your formula is a tree, you want to know what is in the root
node). You can do this with the PySMT functions in fnode.py.
In practice, you have functions you can call directly 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.
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
contain 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 \(\neg\), \(\land\), \(\mathcal{X}\), and \(\mathcal{U}\).get_sub: returns a set containing all the subformulas of an LTL formula.
You can use these functions if they simplify your work.
2.2 Compute the 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.
2.3 Construct the GNBA for a LTL formula
Implement the function:
def ltl2gnba(formula : LtlFormula) -> GNBA :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 you defined so far.
Look at the class GNBA in
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)Try your implementation on the LTL formulas defined in
td5_script.py (at least).
2.4 Convert a GNBA to a NBA
The missing step we need is to implement the procedure that constructs a Non-Deterministic Buchi Automata (NBA) from a Generalized Buchi Automata (GNBA).
In this exercise, you will implement the function:
def gnba_to_nba(gnba : GNBA) -> NBA:
...in mc308/td5.py. The function takes as input a
GNBA and returns a NBA that accept the same
language.
In the file td5_script.py you have some simple GNBA you
can use to test the first implementation of your function.