§Linear-time Temporal Logic

The two basic operators:

  • [] P: P should hold all the time; invariance
  • <> P: P should hold at least once: guarantee

Based on their definition, one can see that they are dual; therefore, ! [] P == <> ! P

Additionally, we can compose them:

  • [] <> P: P should hold infinitely often or is the final state; progress
  • <> [] P: P should always hold sometime in the future or is the final state; stability

§LTL in SPIN

Each LTL formula is checked for every execution trace. Run it using spin -run -a test.pml, and assertion failure or acceptance cycle means that the property denoted by the LTL formula does not hold.

§Example 1

1
2
3
4
5
6
7
8
9
10
11
12
13
byte x = 0
active proctype t0() {
  x++
}

active proctype t1() {
  x--
}
ltl { [] (x == 0) } // fails, since x could be 1 or -1 during the execution
ltl { <> (x == 0) } // succeeds, since x == 0 initially
// since the traces are finite, the final state is the one that matters
ltl { [] <> (x == 0) } // succeeds
ltl { <> [] (x == 0) } // succeeds

§Example 2

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
byte x = 0
active proctype t0() {
  if
  :: skip
  :: x++
  fi
}

active proctype t1() {
  x--
}
ltl { [] (x == 0) } // fails
ltl { <> (x == 0) } // succeeds
// since the traces are finite, the final state is the one that matters
ltl { [] <> (x == 0) } // fails
ltl { <> [] (x == 0) } // fails

§Example 3

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
byte x = 0
active proctype t0() {
  do
  :: x == 0 -> x = 1
  :: x == 1 -> x = 0
  od
}

ltl { [] (x == 0) } // fails
ltl { [] (x == 0 || x == 1) } // succeeds
ltl { <> (x == 0) } // succeeds
ltl { <> (x == 1) } // succeeds

// infinitely 0 or 1
ltl { [] <> (x == 0) } // succeeds
ltl { [] <> (x == 1) } // succeeds

// doesn't converge, no stability
ltl { <> [] (x == 0) } // fails
ltl { <> [] (x == 1) } // fails

§Example 4

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
byte x = 0
active proctype t0() {
  if
  :: skip
  :: x++
  fi
}

active proctype t1() {
  x++
}

// x == 2 is *not* guaranteed
ltl { <> (x == 2) } // fails; doesn't hold for some trace
// but x == 2 is reachable; proved using contradiction
ltl { [] (x != 2)  } // fails;

// [] P and <> ! P are dual, but both of them fails here, because SPIN considers all traces;
// for a particular trace, one and only one of them holds

§Example 5

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
bool x = false
bool y = false
bool run_done = false

active proctype t() {
  if
  :: x = true; y = true
  :: skip
  fi
  run_done = true
}

// two properties we want to prove, using assertion or ltl
// 1. x == true is reachable
// 2. run_done == true && x == true implies y == true

init {
  run_done
  // using asserations
  // assert(x == false)
  // if
  // :: x -> assert(y == true)
  // :: else -> skip
  // fi
}

// using ltl
ltl { [] !x } // fail; contradiction
ltl { [] (run_done && x -> y) } // succeeds

§References