This assignment will be closed on May 06, 2026 (23:59:59).

You must be authenticated to submit your files

CSE308 - Tutorial 6 - CTL Model Checking

Setup
Evaluation.
Exercise 1 - Specialized CTL operators
Exercise 2 - Specifying and verifying CTL properties in SMV
Exercise 3 - Symbolic CTL model checking
- A. Symbolic Transition Systems and BDDs
- B. Denotation and CTL model checking
Submit your work

Setup

In this lab you will need to install the BDD library from PySMT with the following command:

$ pysmt-install --bdd

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

IMPORTANT: The BDD installation will not work on MacOS (and not tried on windows), but it does on the linux lab machines.

You can connect via ssh to the machines at polytechnique. Check the Working via ssh on moodle. You can further use the SSH extension to Visual Studio Code to make your life easier (as explained in the page linked above).

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

Of course, you’ll need to install pysmt on the lab machine. You can follow this guide.

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:

Exercise 1 : Specialized CTL operators: 7 points
Exercise 2 - CTL specification in SMV: 6 points
Exercise 3 - Implementation of CTL model checking: 7 points

Exercise 1 - Specialized CTL operators

In this exercise you will work on pen and paper and submit your answer in the file ctl.pdf.

In class, we considered CTL formula containing the operators the subformulas $\mathbf{EX} \Phi, \mathbf{EG} \Phi$, and $\Phi_1\ \mathbf{U}\ \Phi_2$. While that is sufficient to compute the denotation of a generic CTL formula, you may think of specfic ways of computing the denotation for the remaining operators.

Write the computation of the denotation for the following CTL formulas (in the last two cases you will need to compute a specific fix point):

$\mathbf{AX}\ \Phi$
$\mathbf{AG}\ \Phi$
$\mathbf{A}\ (\Phi_1\ \mathbf{U}\ \Phi_2)$

Exercise 2 - 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 does 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.

Exercise 3 - Symbolic CTL model checking

A. 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 $Img$ 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:

(1) “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.

Now, to remove the quantifiers (step 1) 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.

(2) Rename all the variables $v_1', v_2', \ldots \in Img'$ to $v_1, v_2, \ldots$

You may want to use the function substitute from pysmt to perform the renaming.

B. Denotation and CTL model checking

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 $[\![ \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 $[\![ \textbf{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 $[\![ \textbf{E}\ (\phi_1\ \mathbf{U} \phi_2) ]\!]$.

Compute the denotation recursively 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, formula : CtlFormula) -> bool

that checks if $ts \models formula$.

Submit your work

You’ll have to upload the following files

Upload form is only available when connected