CSE308 - Tutorial 3: Omega-Regular Model Checking

Setup

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

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, prefixes, closures: 6 points
• NBA intersection : 8 points
• Persistence checking for TS: 3 points
• Model checking omega-regular properties: 3 points

Model Checking Omega Regular Properties

NBA, prefixes, and closures.

Consider the following linear time properties expressed with the set of atomic propositions \(AP = \{N_1,N_2,C_1,C_2,T_1,T_2\}\) :

1. \(P_a := \{A_0 A_1 \ldots \mid \forall i \ge 0, A_i \models \neg (C_1 \land C_2)\}\)

2. \(P_b := \{A_0 A_1 \ldots \mid \forall i \ge 0, \exists j \ge i, A_j \models C_1\}\)

3. \(P_c := P_a \cap P_b\)

For each property \(P_\alpha\), with \(\alpha \in {a,b,c}\), answer the following questions:

1. Provide a Buchi automaton \(A_\alpha\) such that \(\mathcal{L}(A_\alpha) = P_\alpha\).

2. State whether the property \(P_\alpha\) is a safety property, a liveness property, or neither.

3. Provide a NFA \(B_\alpha\) such that \(\mathcal{L}(B_\alpha) = \text{pref}(P_\alpha)\).

4. Provide a Buchi automaton \(C_\alpha\) such that \(\mathcal{L}(C_\alpha) = \text{closure}(P_\alpha)\).

You can draw your automaton and submit a pdf file (named nba.pdf with your answers).

Emptiness checking for a NBA.

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

From now on, you will work in the file mc308/td3.py.

The file mc308/auto/nba.py defines a class NBA to represent nondeterministic Buchi automata. In the end, the data structure is, unsurprinsigly, very similar to the one we used for NFAs last week.

You will 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 using the nested DFS algorithm we saw in class.

The python script td3_script.py contains some examples of NBAs and a simple test function test_emptiness. The function now just print the result of the is_emptiness check and prints the NBAs in a file. You have to fill the expected result of the emptiness check (see the variable expected_results).

IMPORTANT: you will also submit your version of td3_script.py file.

Checking Persistence

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

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

Recall that a persistence property says that:

“eventually, the transition system will always satisfy Pers”

where Pers is a propositional logic formula.

Use the transition systems from the lecture and check some persistence properties to test your solution, (use 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 mc308/td3.py file:

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

Also here, add your test cases to the td3_script.py file.

Of course, feel free to reuse any code you wrote in the previous tutorials, if that’s useful.

Submit your work:

You’ll have to upload the following files