This assignment has been closed on April 18, 2025.
You can still upload files, but please note that your submission will be marked as late.
You must be authenticated to submit your files

CSE308 - Tutorial 4 - Linear Time Temporal Logic

Setup

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

Today we will work with an existing model checker, NuSMV, and try to understand linear temporal logic.

You need to install the NuSMV model checker to work on this tutorial. You can download NuSMV here for your platform. If you work on a linux, x86-64, machine you can probably setup everything via terminal with the following commands:

$ cd
$ wget https://nusmv.fbk.eu/distrib/NuSMV-2.6.0-linux64.tar.gz
$ tar xf NuSMV-2.6.0-linux64.tar.gz

Now you’ll have an executable for NuSMV in ~/NuSMV-2.6.0-Linux/bin. NuSMV has a command line interface, so you run it from a terminal.

Symbolic representation and the NuSMV language

The NuSMV model checker takes as input a transition system (as the one we used in class) and a set of specifications (we will see invariant properties and LTL properties). However, the transition system is represented symbolically by means of propositional logic formulas, instead of having an explicit representation as a graph. The symbolic representation is useful in circuit design and other contexts, and we will see more of that in the second part of the course.

We will first see how we can express a transition system using logic and then we will use the NuSMV input language to express such systems.

This first part does not require you to submit anything. However, you need to understand how to represent transition system in NuSMV before proceeding to the other exercises.

Symbolic Transition Systems for a 2 bit counter

Consider the following (explicit) transition system that counts from 0 to 3 and then resets to 0 and starts counting again:

Counter

Consider a set of atomic propositions \(AP=\{b_0, b_1\}\). In the symbolic representation, we represent sets of states as Boolean formulas. So:

So, we can represent the set of initial states as: \(\neg b_0 \land \neg b_1\) (in this case there’s only one initial state). In practice, we use the set of atomic propositions to directly define the state space of the transition systems (i.e., the set of states \(S = 2^{AP}\)).

Then, the transition relation just relates a “source” state and a “target” state. We represent such relation using a formula. While we have a set of atomic propositions \(AP\), we do not have a set of atomic proposition to express the “target” states (the “next” states the system can move to taking a transition). We just use a new set \(AP' = \{a' \mid a \in AP\}\) that just renames the variables in \(AP\) (so, in our example \(AP' = \{b_0', b_1'\}\)).

The transition relation represented with a Boolean formula can just “enumerate” these pairs of states as follows:

\[\left( (\neg b_0 \land \neg b_1) \land (b_0' \land \neg b_1') \right) \lor \left( (b_0 \land \neg b_1) \land (\neg b_0' \land b_1') \right) \lor \ldots\]

If you think a second, you want to express the following relation:

b1 b0 b1’ b0’
0 0 0 1
0 1 1 0
1 0 1 1
1 1 0 0

So, your transition relation can be much more succint:

\[ (b_0' \leftrightarrow \neg b_0) \land (b_1' \leftrightarrow ( b_0 \oplus b_1 )) \]

where \(\leftrightarrow\) is the “if and only if” operator (or equality) and \(\oplus\) is the xor operator (the result is 1 only if the two operand are different, 0 otherwise).

That’s it, now you have:

The tuple \((AP, I, T)\) defines a symbolic transition system.

Note that we don’t care about the labeling function. We will assume that the states are labeled directly with their assignments. You’ll see we can add more atomic propositions if we need a specific labeling. Also, we don’t care about the actions on the transitions in the symbolic transition system, as we will not look into asynchronous systems today. Also here though, you can think of adding more atomic propositions to represent the labels on the transitions.

Writing transition systems in NuSMV

The following text describes the counter transition system in the input language of NuSMV:

-- The text following "--" is a comment.
--
-- This is a NuSMV model describing a binary counter with 2 bits.
--
-- All the SMV models have a "main" module that is "instantiated" by default (more later)
MODULE main

-- variable declaration block, can declare veriables
-- of an arbitrary type (also modules, as earlier)
-- WARNING: the language is declarative, the order of declarations does not matter.
VAR 
  bit0 : boolean;
  bit1 : boolean;

-- The set of initial state is 00
-- !: boolean complement
-- &: boolean AND
INIT ! bit0 & ! bit1;

-- Transition relation
--
-- next(formula): constrain the value of the formula in the NEXT STATE (i.e., the 
-- "destination" of the transition).
--
-- <->: is the equality operator (i.e., a <-> b := a -> b & b -> a)
--
-- The following formula expresses the following relation between current states and
-- next states (i.e., each line is a transition!)
--
-- Current State | Next state
--         b1 b0 |      b1 b0
--          0  0 |       0  1
--          0  1 |       1  0
--          1  0 |       1  1
--          1  1 |       0  0
TRANS
  (next(bit0) <-> !bit0) &          -- bit0 is always the complement of bit1
  (next(bit1) <-> (bit0 xor bit1))  -- bit1 is 1 when both bit0 and bit1 are
                                    -- different

You can read your model in NuSMV as follows (the model is already in a file in smv/counter.smv):

$ ./NuSMV -int smv/counter.smv
...
NuSMV >

NuSMV opens an interactive shell that you use to provide commands. You can simulate your model (e.g., take 5 transitions in the transition systems) as follows:

NuSMV > go

NuSMV > pick_state -v
Trace Description: Simulation Trace 
Trace Type: Simulation 
  -> State: 1.1 <-
    bit0 = FALSE
    bit1 = FALSE

NuSMV > simulate -k 5 -v

********  Simulation Starting From State 1.1   ********
Trace Description: Simulation Trace 
Trace Type: Simulation 
  -> State: 1.1 <-
    bit0 = FALSE
    bit1 = FALSE
  -> State: 1.2 <-
    bit0 = TRUE
    bit1 = FALSE
  -> State: 1.3 <-
    bit0 = FALSE
    bit1 = TRUE
  -> State: 1.4 <-
    bit0 = TRUE
    bit1 = TRUE
  -> State: 1.5 <-
    bit0 = FALSE
    bit1 = FALSE
  -> State: 1.6 <-
    bit0 = TRUE
    bit1 = FALSE

The commands:

NuSMV outputs a trace, a sequence of states visited in the transition system (this corresponds to an execution fragment). Note that NuSMV uses the term trace for the sequence of states and input variables. So, in practice the labeling function is just the “name” of the state in the system.

You can use the documentation and the language tutorial to get a reference on the language syntax and commands.

Modules in NuSMV

The SMV language allows you to write modules, which in some way define part of your final transition system and that you can reuse multiple times. So, for the counter example you could have used a module as follows:

-- All the SMV models have a "main" module that is instantiated by default
MODULE main

-- instantiate a binary_counter
VAR
  bc : binary_counter; -- bc is a variable name, binary_counter its type


-- Define the type the binary_counter (i.e., a MODULE)
MODULE binary_counter

VAR
  bit0 : boolean;
  bit1 : boolean;

INIT ! bit0 & ! bit1;

TRANS
  (next(bit0) <-> !bit0) &          -- bit0 is always the complement of bit1
  (next(bit1) <-> (bit0 xor bit1))  -- bit1 is 1 when both bit0 and bit1 are
                                    -- different

In the main module, you could have created another binary counter, for example:

-- All the SMV models have a "main" module that is instantiated by default
MODULE main

-- instantiate a binary_counter
VAR
  bc : binary_counter; -- bc is a variable name, binary_counter its type
  bc2 : binary_counter; -- 2nd counter

The idea is to have a synchronous composition of bc and bc2, so that the two “sub” transition systems always take a transition together. You can create submodules and pass parameters when you instantiate a module (you pass parameter by reference).

Verifying an invariant property on the counter

You will first try to verify an invariant property on the counter model in smv/counter_spec.smv. The model adds to the binary counter a decimal counter dc (a variable instantiating a module of type decimal_counter) that counts from 0 to 3 and then resets the counter to 0 and continues counting (so, it does not use our manual encoding of the “binary” operations).

We want to check if the binary counter bc is equivalent to the decimal counter dc. We write an invariant property with the keyword INVARSPEC (it is already specified in the SMV file):

-- Invariant property: in all the states, the value of the
-- two counters must be the same
INVARSPEC (!bc.bit0 & !bc.bit1 & dc.value = 0) |
  (bc.bit0 & !bc.bit1 & dc.value = 1) |
  (!bc.bit0 & bc.bit1 & dc.value = 2) |
  (bc.bit0 & bc.bit1 & dc.value = 3);

We can check the invariant property using the command check_invar. Read the model in NuSMV (with the command go), and then use the command check_invar. The system will tell output

NuSMV > check_invar
-- invariant (((((!bc.bit0 & !bc.bit1) & dc.value = 0) | ((bc.bit0 & !bc.bit1) & dc.value = 1)) | ((!bc.bit0 & bc.bit1) & dc.value = 2)) | ((bc.bit0 & bc.bit1) & dc.value = 3))  is true

Telling you the invariant property holds.

Verifying the counter module with LTL

The SMV model in smv/counter_ltl.smv models a counter that counts from 0 to 3, and then resets back to 0. In this first exercise you will write the following LTL specifications:

  1. The counter starts from 0

  2. The counter visits the sequence 0,1,2,3 (from the initial state).

  3. The counter always increments its value in the next state, apart when the value is 3.

  4. The counter always resets the counter to 0 immediately after visiting 3.

  5. The counter visits 0 infinitely often.

  6. The counter visits the sequence 0, 1, 2, 3 infinitely often.

Here’s some hints to get you started with the task.

You can express that the counter is always less than 3, which does not hold in the model, with the expression:

LTLSPEC G ! (bit0 & bit1);

LTLSPEC is the NuSMV keyword after which you declare a LTL property: you write each property in a different LTLSPEC declaration.

You can write your LTLSPEC property in both the main or the binary_counter module. In the main module, you have to add the context of the specific counter variable you want to verify (e.g., LTLSPEC G ! (bc.bit0 & bc.bit1);, where bc is the name of the module instantiation for the counter). Write the LTL properties in the binary_counter module, since you don’t need to tell anything about the rest of the system. You will find an “empty” LTL property for each property you have to write, e.g. the first property is named P1:

-- counter always starts from 0
LTLSPEC NAME P1 := TRUE;

Important: use the NuSMV manual if you need help on the language syntax or on the available commands in NuSMV.

Verifying the MUL module with LTL

Focus on the mul.smv model. The model contains a module MUL that implements a multiplication between 2 bit-vectors of 3-bit width (i.e., a sequence of 3 bits) using repeated additions. In practice, the module computes the product in several steps instead of a single one. The module takes as input 3 parameters, input1,input2, and start:

MODULE MUL(input1, input2, start)

input1, and input2 are the two words to multiply together and start is a boolean. The module starts a new computation as soon as the start signal is true AND the previous computation terminated. When the computation terminates, the variable result stores the result of the multiplication. The module uses a boolean variable is_done that is true when result contains the result of the multiplication of the values input1 and input2 contained when the computation started. is_done is false while the module is currently computing the multiplication. Observe that the value of input1 and input2 are stored the variables tmp_input1 and counter repsectively as soon as the computation starts. Thus, input1 and input2 may change after the computation started, but the module still computes the multiplication of their values before the change.

You will write the LTL specification that check if the MUL module is correct. First, read the following notes to get a better understanding of the module:

Start of the the computation

Write the following LTL properties:

  1. Whenever a computation starts, in the next step is_done becomes false.

  2. Whenever a computation starts, in the next step the result are reset to 0

  3. Whenever a computation starts, in the next step the tmp_input1 is equal to input1 and the counter is equal to input2.

    Here, you would like to express that the next value of tmp_input1 is equal to the current value of input1. If you think carefully, you cannot easily express this fact with the X LTL operator, since you have to compare the value of a variable “at different times” (you can do it looking at each bit of the word, but it’s annoying). Instead, NuSMV allows you to use the next operator directly in the LTL formula. For example, you can write:

    LTLSPEC next(x) = x

    which says that the variable x does not change value after the first transition.

While not computing

  1. When not computing nothing changes inside the module.

Check the computation

  1. Each computation eventually terminates.

  2. Whenever a computation starts, tmp_input1 does not change while the computation is ongoing.

  3. Whenever a computation ends, the computed result is correct.

    Here, limit your specification to the case when the inputs input1 and input2 do not change while the computation is ongoing. You have to add this constraint explicitly in your LTL property (e.g., you need to specify in your assumptions that G next(input1) = input1 ...).

Evaluation and Submission

You will receive 20 points, distributed as follows:

Submission

Upload form is only available when connected
Upload form is only available when connected