CSE308 - Tutorial 3: Omega-Regular Model Checking

Setup

Setting up the tutorial.

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

You need to install the python package 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).

If you’re working on the lab machines, you need to install pip yourself (you need to do this operation once, when pip is installed you can use it):

$ wget https://bootstrap.pypa.io/get-pip.py
$ python3 get-pip.py

pip may be already in your path after this, otherwise you can run pip from: ~/.local/bin/pip (or add it to your PATH variable as usual).

Evaluation.

You will receive 100 points.

I will mainly evaluate if your code implements the algorithms we saw in class, but it’s ok if the code fails for some corner case.

Deadline.

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

Emptiness Checking for Nondeterministic Buchi Automata

The file mc308/data_structures/nba.py define a class NBA to represent nondeterministic Buchi automata. In the end, the data structure is exactly the same as the NFA we saw last week (but we like to duplicate code…).

You will first implement the function is_empty in the NBA class:

is_empty(self : NBA) -> Tuple[True,Option[List[State]]]

The function implements the language emptyiness check for NBAs. Recall that you can check for language emptiness in two steps:

• find a reachable final state \(s\) in the NBA.

• check if there is a cycle starting at \(s\).

You can implement both with a Depth First Search (DFS).

The function returns:

• (True, None) if the language of the NBA is empty; and

• (False, run) otherwise.

run is an infinite run of the automaton. Since we cannot have an infinite list, we use the implicit representation:

\(s0 s1 ... s_{(i-1)} s_i ... s_{(i+k)} s_i\)

where \(s_i\) is the final state that repeats infinitely often. In practice, the finite path just append \(s_i\) again the the end of a run. The corresponding infinite path would be:

\(s0 s1 ... s_{(i-1)} (s_i s_{(i+1)} ... s_{(i+k)})^{\omega}\)

In practice:

• \(s0 s1 ... s_{(i-1)}\) is a finite prefix (it may also be of zero length)
• \((s_i s_{(i+1)} ... s_{(i+k)})^{\omega}\) is the part of the run repeats infinitely often

The python script nba_emptiness.py contains a main function that you can run to test your emptiness check. We provided you with some Buchi automata (they are in the buchi folder in xml format, which we do not care about). The script loops through all of them and check each one for emptiness (and also prints a dot representation of the automata, which you can visualize with the graphviz program or online, for example here, among others).

Then, implement the function is_run of the class NBA:

is_run(self : NBA, run : List[States], accepting : bool) -> Tuple[bool,Option[List[T]]]

The function takes as input an NBA, an infinite run (as before), and a boolean, and returns:

• (False, None) if run is not a run of the NBA (and not an accepting run if accepting is true)

• (True, trace) if run is a run of the NBA, with trace being the trace accepted by the run.

In practice, the function just checks that the sequence of states run can be “executed” in the NBA (i.e., \(s_0\) is an initial state, \(s_i\) can transition to \(s_{i+1}\), …). The trace is just the sequence of labels corresponding to the run.

The script nba_emptiness.py already calls is_run after checking for emptiness. This function helps you debugging your result.

Checking Persistence for a Transition System

You will implement the persistene checking for a transition system in the function check_persistence.py in the mc308/algorithms/omega_regular.py file:

check_persistence(ts : TS,
  f_persistence : PropFormula) -> Tuple[bool, Optional[List[States]]]

Recall that a persistence property says something like:

“eventually, globally the transition system does not visit any state in f_persistence”

where f_persistence is a propositional logic formula.

The function returns:

• (True, None) if the transition system satisfy the persitence property

• (False, cex) otherwise.

cex here represents an INFINITE PATH of the transition system that does not satisfy the persistence property (i.e., wher states satisfying f_persistence repeats infinitely often).

Since cex infinite, we represent it as a finite sequence of states similarly as for a run of the NBA:

\(s0 s1 ... s_{(i-1)} s_i ... s_i\)

Such path represents a prefix \(s0 s1 ... s_{(i-1)}\) and a suffix \(s_i ... s_{(i-1)}\) that repeats infinitely often.

HINT: implement the double dfs algorithmm, similarly to what you did for cheking emptiness for an NBA (the implementation is almost the same)

You can try your code running the script check_persitence.py. The script loads some transition systems from the ts folder and check some persistence property on them (here, we already gave you a function in the TS class to simulate a run…).

Omega-Regular Model Checking

Finally, you will implement the omega-regular model checking for a transition system and a NBA (representing the negation of the omega regular property you want to check).

The function check_omega_regular is also in the file mc308/algorithms/omega_regular.py:

HINT: construct the product automaton of the transition system and the Buchi automaton first, then check a persistent property on the product.