In [1]:
import spot
from spot.jupyter import display_inline
spot.setup(show_default='.vtnA')

Examples from our PN'25 paper "Simplifying LTL Model-Checking Given Prior Knowledge"

TL;DR Model checking a system $M$ against a specification $\varphi$ amounts to check whether $\mathscr{L}(M\otimes A)=\emptyset$, where $A$ is an automaton for $\lnot\varphi$. If we have some extra knowledge $K$ about $M$, we can replace the previous check by $\mathscr{L}(M\otimes B)=\emptyset$ where $B$ is an automaton simpler than $A$, but that has been built from $A$ and $K$.

Example from Figure 3

Assuming A is the the automaton for $\lnot\varphi$, and that K is some apriori knowledge about the system to check, this combines A and K into a bounded automaton (Ab), whose labels can then be simplified (Aminato). The resulting automaton can be further minimized. The whole process reduces both the size and the strength of the automaton.

In [2]:
A = spot.translate('F(a & c) | G(Fb & F!b)')
K = 'FG(b) & G(c)'
Ab = spot.update_bounds_given(A, K)
Aminato = spot.bounds_simplify(Ab)
Asimpl = Aminato.postprocess('small')
display_inline(A, Ab, Aminato, Asimpl)
0 0 I->0 0->0 !a | !c 1 1 0->1 a & c 2 2 0->2 !a | !c 1->1 1 ⓿ ❶ 2->2 b ⓿ 2->2 !b ❶
0 0 I->0 0->0 !a & c … !a | !c 1 1 0->1 a & c … a | !c 2 2 0->2 0 … !a | !c 1->1 c … 1 ⓿ ❶ 2->2 0 … 1 ⓿ 2->2 0 … 1 ❶
0 0 I->0 0->0 !a 1 1 0->1 a 1->1 1 ⓿ ❶
1 1 I->1 1->1 !a 0 0 1->0 a 0->0 1 ⓿

Example from Figure 4

This demonstrate the stutterize_given(A, [K1, K2,...], type) function that attempts to build a stutter-invariant automaton. It takes an automaton A to simplify, a list of knowledges [K1, K2, ...] that can be used for simplification, and a type of simplification (True for the relax variant, and False for the retrict variant.) It returns a stutter-invariant automaton if it manages to build one (property prop_stutter_invariant() will be set on the result in this case), or the original automaton otherwise.

In [3]:
A = spot.translate('XFa'); K = spot.translate('!a', 'Buchi')
sirelax = spot.stutterize_given(A, [K], True).postprocess('small')
sirestrict = spot.stutterize_given(A, [K], False).postprocess('small')
display_inline(A, K, sirestrict, sirelax, per_row=2)
1 1 I->1 2 2 1->2 1 0 0 0->0 1 ⓿ 2->0 a 2->2 !a
1 1 I->1 0 0 1->0 !a 0->0 1 ⓿
1 1 I->1 1->1 a ⓿ 2 2 1->2 !a ⓿ 0 0 0->0 1 ⓿ 2->0 a 2->2 !a
1 1 I->1 1->1 !a 0 0 1->0 a 0->0 1 ⓿

Other examples not shown in the paper

This is probably one of the very first example we worked with, but it does not show as much as the one we kept for Figure 3.

In [4]:
aut1 = spot.translate('a | G(Fc & F!q)')
aut2 = spot.update_bounds_given(aut1, 'G(q)')
aut3 = spot.bounds_simplify(aut2)
display_inline(aut1, aut2, aut3, aut3.postprocess())
0 0 I->0 1 1 0->1 a 2 2 0->2 !a 1->1 1 ⓿ ❶ 2->2 !c & q 2->2 c & q ⓿ 2->2 !c & !q ❶ 2->2 c & !q ⓿ ❶
0 0 I->0 1 1 0->1 a & q … a | !q 2 2 0->2 0 … !a | !q 1->1 q … 1 ⓿ ❶ 2->2 0 … 1 2->2 0 … 1 ⓿ 2->2 0 … 1 ❶ 2->2 0 … 1 ⓿ ❶
0 0 I->0 1 1 0->1 a 1->1 1 ⓿ ❶
1 1 I->1 0 0 1->0 a 0->0 1

The following example shows how multiple knowledge can be accumulated in the bounded automaton.

In [5]:
aut1 = spot.translate('a U (b U c)')
aut2 = spot.update_bounds_given(aut1, 'G(b -> Xc)')
aut3 = spot.update_bounds_given(aut2, '!a')
aut4 = spot.bounds_simplify(aut3)
display_inline(aut1, aut2, aut3, aut4, aut4.postprocess(), show='.vt')
Inf( ⓿ ) [Büchi] 2 2 I->2 2->2 a & !c 0 0 2->0 c 1 1 2->1 !a & b & !c 0->0 1 ⓿ 1->0 c 1->1 b & !c
Inf( ⓿ ) [Büchi] 2 2 I->2 2->2 a & !c 0 0 2->0 c 1 1 2->1 !a & b & !c 0->0 1 ⓿ 1->0 c … 1 1->1 0 … !c
Inf( ⓿ ) [Büchi] 2 2 I->2 2->2 0 … a 0 0 2->0 !a & c … a | c 1 1 2->1 !a & b & !c … a | (b & !c) 0->0 1 ⓿ 1->0 c … 1 1->1 0 … !c
Inf( ⓿ ) [Büchi] 2 2 I->2 0 0 2->0 c 1 1 2->1 b & !c 0->0 1 ⓿ 1->0 1
t [all] 0 0 I->0 1 1 0->1 b | c 1->1 1

The following example also accumulates some (trivial) knowledge. It builds an automaton that is unfortunately stutter-sensitive because of the relaxed initial transition. If that transition was restricted to p0&p1, the automaton would be stutter-insensitive.

In [6]:
aut1 = spot.translate('F(!p0 | X!p1)')
aut2 = spot.update_bounds_given(aut1, 'p0')
aut3 = spot.update_bounds_given(aut2, 'p1')
aut4 = spot.bounds_simplify(aut3)
display_inline(aut1, aut2, aut3, aut4)
1 1 I->1 0 0 1->0 !p0 2 2 1->2 p0 0->0 1 ⓿ 2->0 !p0 | !p1 2->2 p0 & p1
1 1 I->1 0 0 1->0 0 … !p0 2 2 1->2 p0 … 1 0->0 1 ⓿ 2->0 !p0 | !p1 2->2 p0 & p1
1 1 I->1 0 0 1->0 0 … !p0 | !p1 2 2 1->2 p0 & p1 … 1 0->0 1 ⓿ 2->0 !p0 | !p1 2->2 p0 & p1
1 1 I->1 2 2 1->2 1 0 0 0->0 1 ⓿ 2->0 !p0 | !p1 2->2 p0 & p1

Passing this result through sutterize_given and then postprocess() achieves the desired reduction.

In [7]:
sg = spot.stutterize_given(aut1, [spot.translate("p0"), spot.translate("p1")])
display_inline(sg, sg.postprocess())
1 1 I->1 0 0 1->0 !p0 | !p1 ⓿ 2 2 1->2 p0 3 3 1->3 p0 & !p1 0->0 1 ⓿ 2->0 !p0 | !p1 ⓿ 2->2 p0 & p1 3->2 p0 & !p1 3->3 p0 & !p1
1 1 I->1 1->1 p0 & p1 0 0 1->0 !p0 | !p1 0->0 1 ⓿