This assignment will be closed on May 22, 2025 (23:59:59).

You must be authenticated to submit your files

CSE308 - Tutorial 6 - CTL Model Checking

Setup
Evaluation.
Specifying and verifying CTL properties in SMV
Symbolic Transition Systems and BDDs
Compute the denotation of a CTL formula
Submit your work

Setup

Apart from the older dependencies (look at TD1 for reference) in this lab you will need NuSMV (look at TD4 for reference) and the BDD library from PySMT with the following command:

$ pysmt-install --bdd

The BDD installation may not work on MacOS, but it does on the linux lab machines (the one at polytechnique, reachable via ssh).

Note: installing the BDD package may not work on MacOS, but it may work depending on your local configuration (the installer is not robust and there is some work to fix the compilation of repycudd, the python wrapping of the BDD package CUDD written in C). My advice is to work on the lab machine using Linux.

As a reminder, you can work remotely on the lab machines via ssh (read the Remote Lab via SSH document on moodle). Also, you may find the Visual Studio Code extension to work via ssh quite convenient.

After your setup is complete, download and extract the files of the tutorial CSE308-TD6-1-handin.zip. You’ll have a folder called CSE308-TD6-1-handin.

Installing pysmt on the lab machines

Install anaconda with a recent python distribution (you may check your python vesion, it should be >= 3.10)
```
$ wget https://repo.anaconda.com/archive/Anaconda3-2024.02-1-Linux-x86_64.sh
$ bash Anaconda3-2024.02-1-Linux-x86_64.sh
```
Accept the license and take a coffee.
Install the python pysmt package
```
$ pip install pysmt
```
The command will install pysmt in your home directory.
Install the BDD package and Z3 (the SAT solver that we will use next week)
```
$ ~/.local/bin/pysmt-install --bdd
```
```
$ ~/.local/bin/pysmt-install --z3
```

Evaluation.

You will receive a maximum 20 points, subdivided as follows:

CTL specification in SMV: 7 points
Image computation using BDDs: 2 points
Denotation for EX: X points: 2 points
Denotation for EG: X points: 3 points
Denotation for EU: X points: 2 points
Denotation for a ctl formula: 2 points
CTL model checking: 2 points

Deadline.

The deadline for submitting the exercise to obtain a full grade is Thursday May 22nd at 23:59 (there will still be another tutorial on Friday 16 due to Thursday 22nd, but you will have more time to complete this TD). You can submit your work after that deadline but you will receive only 50% of the total grade.

Specifying and verifying CTL properties in SMV

You will work in the SMV file smv/chain.smv.

The file already specifies a simple transition system that increments a variable n from 0 to 255, and then keeps its value at 255. The system has also a transitions from every state n such that n + 1 % 3 = 0 to the the state n + 1 - 3 (0 doe not have such transition, since we’re not considering negative numbers).

You will write and verify the following CTL properties in NuSMV. CTL properties in SMV are a Boolean combination of atomic proposition and merge path and temporal quantifiers, which are merged together (i.e., E F p is expressed in NuSMV with a single operator EF merging the path quantifier E and temporal quantifier F (you can see the other operators in the NuSMV manual).

Note that in SMV the until operator is written as A [formula U formula], so it uses square brackets to enclose the until part of the operator (instead of normal round parenthesis). When we’ll switch to Python later the concrete syntax will change to formula AU formula instead (and similarly for the EU operator).

The CTL property you have to write and check are described in natural language in the smv file (you have a placeholder for each one of them, you have to replace TRUE with your interpretation of the formula in CTL).

Check CTL properties with NuSMV. We provided you the file smv/check_ctl.cmd that you can use to call NuSMV to read your model and check all the CTL properties in a non-interactive way (so, you don’t have to write the commands every time). Just run NuSMV as follows:

$ NuSMV -source smv/check_ctl.cmd smv/chain.smv

You can also use the interactive mode:

$ NuSMV -int smv/chain.smv

and then control what to do. You can find the commands you can use in the NuSMV manual.

Symbolic Transition Systems and BDDs

Symbolic Transition Systems

The class SymbolicTS represents a transition system symbolically using Boolean formulas (it is defined in the file src/mc308/auto/sts.py). You can create a transition system as follows:

V = [Symbol('a'), Symbol('b'))
a,b = V
a_next = get_next(a)
b_next = get_next(b)

# V = {a,b}
# Init := ! a & ! b
# Trans := a' <-> a
ts = SymbolicTS(V, And([Not(a),Not(b)]), And(Iff(a_next,a)))

As usual, we represent Boolean formulas with the PySMT library. Note that you already have functions like get_next to get the variable (symbol) that correspond to a variable after taking a transition, the “primed” version of a variable (clearly, that naming convention is just an arbitrary choice to distinguish variables representing the “current” and the “next” state).

Binary decision diagrams

You will use Binary Decision Diagrams (BDDs) to reason about Boolean formulas (reason means deciding satisfiability, validity, and eliminating quantifiers).

We will see more about BDDs in class next week, but in a nutshell:

A BDD represents all the possible truth assignment to a Boolean formula.
A BDD is a directed acyclic graph (DAG) where a leaf node is either true or false, and a non-leaf node is a variable. Each non-leaf node has two edges, one to represent the variable is assigned to true and one to represent when the variable is assigned to false. Each non-leaf node is, in the end, an if-then-else.
So, a path from the root node to the true node represent a satisfying assignment to the formula, while a path to the false node is an assignment that does not satisfy the formula.
In practice, we deal with Reduced Ordered Binary Decision Diagrams (ROBDD):
- They are ordered since the order in which the variable appears is fixed a priori.
- They are reduced since all the isomorphic subgraph have been merged together, and if a node has two isomorphic children it is removed from the DAG.
Both features makes ROBDD a canonical representation for Boolean formulas. If two formulas are equivalent, then they have exactly the same ROBDD. Also, after you construct the ROBDD for a formula checking satisfiability and validity can be done in constant time (e.g., is there a true node in the ROBDD? is there a false node?).

We will not implement the BDD operation today, but we will use an existing BDD package and, even more, you will use the class BDDWrapper (src/mc308/bdd/bdd_wrapper.py) that provides you the primitives to work with BDDs (and hides some technical details):

def get_bdd(self, formula):
  ...
def get_formula(self, bdd):
  ...
def And(self, bdd1, bdd2):
  ...
def Or(self, bdd1, bdd2):
  ...
def Not(self, bdd1):
  ...
def Rename(self, bdd, maps):
  ...
def Elim(self, vars_list, bdd):
  ...

get_bdd returns the bdd for a formula, get_formula gets a formula from a BDD, And, Or, Not, performs the logical operations on two BDDs, Rename renames the variables in the BDD, and Elim performs a quantifier elimination.

Image computation with BDDs

You will implement the function:

def get_successors(sts : SymbolicTS, S : BoolFormula) -> BoolFormula:

defined in src/mc308/td6.py.

Given a symbolic transition system and a formula S representing a set of states, computes the set of states $Img$ such that:

\[s_2 \models Img \text{ iff there exists }\ s_1 \text{ such that } s_1 \models S \text{ and } s_1,s_2' \models T\]

where T is the formula representing the transition relation of the symbolic transition system.

That’s it, the state $Image$ is called image of the set $S$ and is the set of all the states that can be reached from S taking the transition T once.

To compute the image symbolically you need to:

“Remove” the quantifiers from this formula:

\[\text{Img}' := \exists v_1,v_2,v_3, \ldots . (S \land T)\]

Intuitively, the formula $\text{Img}'$ represents all the assignments to $v_1', v_2', \ldots$  such that there exists an assignment to the variables $v_1, v_2, \ldots$ (i.e., all the variables of the transition system STS) such that the transition relation T is satisfiable.

Rename all the variables v1’, v2’, in $\text{Img}'$ to $v1, v2, \ldots$ You may want to use the function substitute from pysmt to perform the renaming.

Now, to remove the quantifiers you will have to use a BDD. The idea is that you can convert a formula to a BDD, perform operations on it, and then convert it back to a formula. Take for example the following code:

w = BDDWrapper()
bdd = w.get_bdd(formula)
bdd = w.and(bdd, w.not(bdd))
result = bdd.get_formula(bdd)

that creates a bdd for a formula, computes the and with it’s negation (using BDDs!), and finally converts back the BDD to a formula.

Compute the denotation of a CTL formula

You will first implement the basic operations of CTL symbolic model checking to compute the denotation of a formula $\phi$.

Compute EX

You will start with implementing the denotation computation for the path and temporal operators. First, implement the “pre-image” computation function for computing the denotation of $[\![ \textbf{EF}\ \phi ]\!]$:

def compute_ex(bdd_wrapper : BDDWrapper,
               ts : SymbolicTS,
               bdd_phi : BDD) -> BDD

Observe that the function *takes as input a BDD of the formula $\phi$ and returns a BDD of the denotation as output (also, in a realistic setting you would not pass a symbolic transition system represented with a formulas but already its BDD representations, to compute them only once).

Compute EG

Implement the function:

def compute_eg(bdd_wrapper : BDDWrapper,
               ts : SymbolicTS,
               bdd_phi : BDD) -> BDD

that computes the denotation of the formula EG phi (i.e., [[ EG phi ]]).

Here you will need to compute the denotation as a fix-point.

Compute EU

Implement the function:

def compute_eu(bdd_wrapper : BDDWrapper,
               ts : SymbolicTS,
               bdd_phi1 : BDD,
               bdd_phi2 : BDD) -> BDD

that computes the denotation of the formula [[E phi1 U phi2]].

Compute the denotation of a CTL formula

With the above function you can now implement the symbolic computation of the denotation of a CTL formula expressed in existential normal form (only operators EX, EG, EU):

def compute_bdd_denotation(bdd_wrapper : BDDWrapper,
                           ts : SymbolicTS,
                           ctl_formula : CtlFormula) -> BDD

The function above takes as input a ctl formula an returns the BDD representing its denotation.

The function should proceed by induction on the structure of the formula, checking all the possible cases and managing the BDD construction:

for atomic propositions (i.e., ctl_formula.is_symbol()),
Boolean operators (e.g., ctl_formula.is_and(), …), or
a CTL operator (e.g., ctl_formula.is_ctl_EG()).

Symbolic CTL model checking

Implement the function:

def ctl_mc(ts : SymbolicTS, ctl_formula : CtlFormula) -> bool

that checks if $ts \models \text{ctl_formula}$.

Submit your work

You’ll have to upload the following files

Upload form is only available when connected