CSE308 - Tutorial 3: Omega-Regular Model Checking

Setup

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

A note on the Python version you should use:

• We tested the code with the major Python versions 3.10.
• Python 3.9 should still work.
• Some code will not work in Python 3.8 (some of you found an exception running the code in Python 3.8).

The easiest solution for a Python version mismatch is to switch to version 3.10 (e.g., use Anaconda to manage different python versions on your machine).

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

Evaluation.

You will receive a maximum of 20 points distributed as follows:

• NBA intersection : 8 points
• Persistence checking: 8 points
• Model checking algorithm for omega-regular properties: 4 points

Deadline.

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

Model Checking Omega Regular Properties

Emptiness checking for a NBA.

In the first exercise you will implement the emptiness checking for a Nondeterministicf Büchi Automata (NBA).

The file src/mc308/auto/nba.py defines 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.

You will work in the file src/mc308/td3.py.

Frst, implement the function:

def nba_is_empty(nba : NBA) -> bool

The function implements the language emptyness check for NBAs, returning true if the language accepted by the automaton is empty. 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 will get a higher grade if you implement the nested DFS algorithm.

The python script src/td3_script.py contains some examples of NBAs. You will have to write the code to test the function and see things are working correctly (please do!).

Checking Persistence

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

def check_persistence(ts : TS, pers : BoolFormula) -> bool

Recall that a persistence property says something like:

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

where pers is a propositional logic formula.

Use the transition systems from TD2 and check some persistence properties to test your solution (use src/td3_script.py to write your test cases).

Model Checking Omega-Regular Properties

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

The function check_persistence.py in the src/mc308/td3.py file:

def check_persistence(ts : TS, pers : BoolFormula) -> bool

Submit your work:

You’ll have to upload the following files