Referencing previous state in Promela LTL statement

Question

I'm getting started with Promela, and I'm having trouble expressing some LTL formulas.

An example is the following sequence value that I'd like to assert is monotonically increasing. Intuitively I want to write that in the next state, sequence is >= its previous value, but looking through documentation, I don't see a way to express this. Is there a method for expressing this type of formula?

byte sequence = 0;
ltl p0 { [] sequence >= prev(sequence) }
... processes that manipulate sequence ...

Assuming that it's possible to express the monotonically increasing property of sequence above, I'm wondering if there is a syntax for wildcard array indexing. Similar to the above example, I intuitively want to reference all previous index entries.

byte values[N];
byte index = 0;
ltl p1 { values[0..index-1] are monotonically increasing }
... processes ...

Thanks a lot for your help. Promela seems really great :)

Answer 1

AFAIK,

Monotonically Non-decreasing Sequence.

Linear Temporal Logic has a X operator that allows one to express a property that refers to a boolean condition holding in the next state, as opposed to the previous state.

However, one cannot directly compare an integer value of the current state with that of the next state within an LTL formula, because X evaluates to a Boolean value.

In theory, what one can do is to encode the <= operator over the integer as a Boolean property by bit-blasting it, e.g. by means of some clever use of the modulo operator or bitwise operations (it should not be too hard with unsigned variables) and a bit-to-bit comparison of the corresponding Boolean values (see final note).

From a modeling point of view, however, the easiest approach is to enrich your model with a prev_value variable and simply check that in each state the property prev_value <= cur_value holds. Notice that in this case you should use the d_step command to group together the two value assignments, so that they are conflated within a single state with no intermediate transitions, e.g.

...
byte prev_value;
byte cur_value;
...
d_step {
    prev_value = cur_value;
    cur_value = ... non-blocking function ...
}

Otherwise, the invariant property relating prev_value to cur_value may result to be broken on the corresponding automaton for some state s_i. (note: this would actually not hinder the verification of the specific LTL property you are interested in, but it can be an issue with other formulas)

Wildcard Indexing.

If I understand correctly, you want to express a property s.t. --in each state-- only memory locations from 0 up to index-1 are required to be monotonically non-decreasing, with index being a variable which can change value (arbitrarily?).

The structure of such property should be:

ltl p1 {
    [] (
        ((1 <= index) -> "... values[0] is monotonically non-decreasing ...") &&
        ((2 <= index) -> "... values[1] is monotonically non-decreasing ...") &&
        ((3 <= index) -> "... values[2] is monotonically non-decreasing ...") &&
        ...
        ((N <= index) -> "... values[N-1] is monotonically non-decreasing ...")
    )
}

I believe the answer to your question is no. However, I suggest you to use macros for the C preprocessor to simplify the encoding of your properties and avoid writing the same things over and over again.

---

Note:

Let's take curr_int and next_int 0-1 Integer variables s.t. next_int is equal to the value of curr_int in the next state (aka, curr_int is the previous value of next_int), and a curr Boolean variable s.t. curr is true if and only if curr_int is equal to 1.

Then, by the LTL semantics, X curr is true if and only if curr_int (next_int) is equal to 1 in the next (current) state.

Consider the following truth-table for state s_i:

curr_int | next_int | curr_int <= next_int

    0    |     0    |          1
    0    |     1    |          1
    1    |     0    |          0
    1    |     1    |          1

From the above definitions, we can rewrite it as:

  curr   |  X curr  |         EXPR

  false  |  false   |         true
  false  |  true    |         true
  true   |  false   |         false
  true   |  true    |         true

From the truth-table it's can be seen that EXPR corresponds to

  !curr v (X curr)

which can be more elegantly rewritten as

  curr -> (X curr)

Thich is our final LTL-encodeable version of curr_int <= next_int for a given state s_i, when both are 0-1 Integer variables.