CSE308 - Tutorial 2: Safety Properties

Setup
- Evaluation.
Model Checking Safety Properties

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-TD2-1-handin.zip. You’ll have a folder called CSE308-TD2-1-handin.

Evaluation.

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

NFA intersection definition (question 1 and 2): 5
Implementation of \(A_1 \cap A_2\) (intersection of two NFA): 5
Implementation of \(TS \otimes A\): 5
Model checking algorithm for safety properties: 5

Deadline.

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

Model Checking Safety Properties

Nondeterministic Finite State Automata (NFA)

Defining the intersection operation

In class we did not define the intersection operation between two NFA, here you will define one.

Question 1: Write the definition of the synchronous product on paper. Given two NFAs:

\(A_1 = (Q_1, \Sigma_1, \delta_1, Q_{0_1}, F_1)\), and
\(A_2 = (Q_1, \Sigma_1, \delta_1, Q_{0_1}, F_1)\)

define the NFA \(A_1 \cap A_2\) such that \(L(A_1 \cap A_2) = L(A_1) \cap L(A_2)\).

Hint: the result is a NFA where the states are \(Q_1 \times Q_2\) (i.e., the Cartesian product, so each state correspond to a pair of states \((a,b)\), were \(a\) is from \(A_1\) and \(b\) is from \(A_2\).) and that has a transition between two states with a letter \(a \in \Sigma\) only if both the “original states” can take a transition labeled with \(a\).

Question 2: Provide a proof sketch showing that \(L(A_1 \cap A_2) = L(A_1) \cap L(A_2)\).

Hint: To prove the language equivalence, prove separately \(L(A_1 \cap A_2) \subseteq L(A_1) \cap L(A_2)\) and \(L(A_1 \cap A_2) \supseteq L(A_1) \cap L(A_2)\).

For example, assume \(w \in L(A_1 \cap A_2)\) and show \(w \in L(A_1) \cap L(A_2)\). To show \(w \in L(A_1)\) (and similarly for \(A_2\)), use the accepting run \(q0 q1 \ldots\) for \(w\) in \(L(A_1 \cap A_2)\).

Write your answers in a pdf file named intersection.pdf and submit that here (you can write your solution by hand and take a readable picture, use a tablet, write it with LaTeX, …).

Implementing the intersection operation

You find a data structure for representing and manipulating a NFA in src/mc308/auto/nfa.py. The class NFA is very similar to the TS class (e.g., its types, how it represent states and transitions), with these obvious differences:

A NFA has a set of initial states
A NFA does not have a state labeling function
A NFA’s transition is not labeled with an action but a set of atomic proposition (i.e., a letter in the alphabet \(\Sigma\)).

Provide your implementation of the intersection operator in the function:

def nfa_intersection(nfa1 : NFA, nfa2 : NFA) -> NFA:
    """
    Implement the intersection (synchronous product) of two NFAs

    This function returns a NFA A such that:
    Language(A) = Language(nfa1) and Language(nfa2)
    """

that you find with an empty implementation in the file src/mc308/td2.py.

The file src/td2_script.py contains some code you can use to help you testing your implementation (look at that, see how you can construct a NFA, and use the simple NFAs defined there as test cases to help you).

You will upload this and the following exercise at once (all will be in the src/mc308/td2.py file).

Checking Safety Properties

Look at the file in src/mc308/td2.py.

Implement first the ts_nfa_product (this is the same product we saw in class).

def ts_nfa_product(ts : TS, nfa : NFA) -> TS:
    """
    Implement the intersection of a TS with a NFA nfa.

    The result is a new transition system TS1 such that:
    Traces_fin(TS1) = Traces_fin(TS) and Language(nfa)
    """
    raise NotImplementedError("TS and NFA intersection not implemented")

Try to test the product on:

German traffic light example we saw in class (you have one transition system and a NFA)
the mutual exclusion property we saw in class. As NFA, write the NFA repenting all the finite paths that can see a \(n1\) after a \(n1\) (which should not be possible).

Then, implement the function:

def check_safety(ts : TS, bad_prefixes : NFA) -> Tuple[bool, Optional[FinitePath]]:
    """
    bad_prefixes describes is a (regular) set of bad prefixes for a safety
    property P_safe

    This function checks if ts |= P_safe and returns either:
    - (True, None) if ts |= safety
    - (False, cex)    otherwise
      cex is a sequence of states of ts starting from the initial state and
      reaching a state s that does not satisfy the safety property.
    """
    raise NotImplementedError("check_safety not implemented")

Here, you can reuse the ts_nfa_product and the check_invar function you implemented last week (copy your implementation in src/mc308/td2.py.

Upload your work

You’ll have to upload the following files

Upload form is only available when connected