I am trying to understand how to correctly use the Until operator in an ltl formula. I found this definition (below) to be clear:
Until
AUB: true if there exists i such that:
B is true in [si, si+1, si+2, … ]
for all j such that 0 ≤ j < i, formula A is true in [sj, sj+1, sj+2, … ]
meaning:
B is true at time i
for times between 0 and i-1, formula A is true
still using the formalization of "true at time i"
Sample code with example ltl formula:
mtype = {Regular, Reverse, Quit}
mtype state = Regular;
init {
do ::
if
::state == Regular -> state = Reverse
::state == Reverse -> state = Quit
::state == Quit -> break
fi
od
}
ltl p0 { [] ((state == Reverse) U (state != Reverse))}
Based on the definition of the until operator that I gave, I don't understand how the above ltl formula is not producing any errors. Wouldn't state == Reverse
need to be true for all time up until state != Reverse
? Initially state == Regular
.
Below is the SPIN output after running the test:
(Spin Version 6.4.6 -- 2 December 2016)
+ Partial Order Reduction
Full statespace search for:
never claim + (p0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 28 byte, depth reached 13, errors: 0
9 states, stored (11 visited)
2 states, matched
13 transitions (= visited+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.288 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in init
(0 of 12 states)
unreached in claim p0
_spin_nvr.tmp:14, state 20, "-end-"
(1 of 20 states)
pan: elapsed time 0 seconds
STRONG UNTIL
Its formal definition is:
Explanation:
Conditions (1)-(2) enforce the sequence of states (sk, sk+1, ..., sj, ...) to be a valid execution path of the transition system over which the ltl formula can be evaluated.
Condition (3) forces
ψ
to hold in sj.Condition (4) forces
ϕ
to hold in any state si that lies along the path from sk (included) up to sj (excluded).Since an implication with a
false
premise is alwaystrue
, the logical implication inside condition (4) is trivially satisfied for anyi
that lies outside of the range[k, j)
. Wheneverj
is picked to be equal tok
, as in your question, the range[k, j) = [k, k)
is empty and any choice ofi
lies outside said interval. In this case, regardless of the factM, s ⊨ ϕ
holds (or not) for somes
, condition (4) is trivially satisfied for any choice ofi
and it no longer imposes any constraint over the execution path (sk, sk+1, ..., sj, ...). In other words, whenj = k
condition (4) no longer provides any meaningful contribution to the verification of propertyϕ U ψ
over the state sk.WEAK UNTIL
The difference among weak until, hereby denoted with
ϕ W ψ
, and strong until is that weak until is also satisfied by any execution path s.t.G (ϕ ∧ ¬ψ)
, whereas strong until compelsF ψ
.EXAMPLE ANALYSIS
The property p0
requires p1
to hold in each and every state of your system. I will break down p1 in two components for clarity, and define ϕ to be equal
state == Reverse
and ψ to be equalstate != Reverse
(note:ϕ <-> !ψ
).Let's assume, to simplify things, that your system is comprised by the following three states:
In order for p0 to hold, p1 must hold for each of these states.
j
equal 0.false
. However, we have that ϕ holds in s_1 and ψ holds in s_2 which is its immediate, and only, successor. So property p1 holds in s_1.true
, so p1 is again trivially satisfied.