432
S. Wimmer and J. von Mutius
Theorem 1. Let (L, M ) be closed and invariant under P . Assume l 0 ∈ L,
s
0 ∈ M l 0 , s 0 s
0 , and (l 0 , s 0 ) →
∗ (l, s). Then l ∈ L and there exists s
such
that s
∈ M l and s s
.
Proof. By induction on the number of steps in (l 0 , s 0 ) →
∗ (l, s). The following
sketches how the run of covering states is constructed. The first line represents
(l 0 , s 0 ) →
∗ (l, s) and the states in the third line are all part of the certificate.
(l 0 , s 0 )
→
(l 1 , s 1 )
→
. . .
→
(l, s)
(l 1 , t 1 )
. . .
(l, t)
(l 0 , s
0 )
( l 1 , s
1 )
. . .
(l, s
)
From the assumptions on l 0 , s 0 , and s
0 , we can first apply the self-simulation
property of → to (l 0 , s 0 ) → (l 1 , s 1 ) to obtain a t 1 such that s 1 t 1 and (l 0 , s
0 ) →
(l 1 , t 1 ). As the certificate is closed we thus get l 1 ∈ L and we can find an s
1 ∈ M l 1
such that t 1 s
1 (and thus s 1 s
1 by transitivity). The induction hypothesis
can then be applied to l 1 , s 1 , and s
1 .
We will now say that a certificate (L, M ) is admissible iff
– it satisfies P ,
– it is closed,
– it covers the initial state (i.e. there is an s
0 ∈ M l 0 such that s 0 s
0 ),
– and there is no l ∈ L with F l.
Corollary 1. If F is monotone w.r.t. and the certificate (L, M ) is admissible,
then l s. (l 0 , s 0 ) →
∗ (l, s) ∧ F l .
2.2 An Abstract Certificate Checker
In practice, the certification process has to consider one additional complication.
A model is typically described in terms of human-readable identifiers, while most
model checkers and the verified model checker Munta [30] in particular represent
these as natural numbers internally to allow for efficient indexing. In our certifier,
this is accounted for by relabeling the human-readable identifiers in a given model
to natural numbers in a first (verified) pre-processing step. To save additional
transformations of the certificate after it was emitted, we let the unverified model
checker additionally emit a textual description of such a renaming. The certifier
then just needs to check that the given renaming is injective to ensure that it
can safely be applied.
Together with the theoretical analysis laid out in the last section, we can thus
derive the following strategy for certifying unreachability:
– An unverified model checker explores the reachable state space of a given
model symbolically and checks that none of the discovered states (l, s) fulfills
F l.
S. Wimmer and J. von Mutius
Theorem 1. Let (L, M ) be closed and invariant under P . Assume l 0 ∈ L,
s
0 ∈ M l 0 , s 0 s
0 , and (l 0 , s 0 ) →
∗ (l, s). Then l ∈ L and there exists s
such
that s
∈ M l and s s
.
Proof. By induction on the number of steps in (l 0 , s 0 ) →
∗ (l, s). The following
sketches how the run of covering states is constructed. The first line represents
(l 0 , s 0 ) →
∗ (l, s) and the states in the third line are all part of the certificate.
(l 0 , s 0 )
→
(l 1 , s 1 )
→
. . .
→
(l, s)
(l 1 , t 1 )
. . .
(l, t)
(l 0 , s
0 )
( l 1 , s
1 )
. . .
(l, s
)
From the assumptions on l 0 , s 0 , and s
0 , we can first apply the self-simulation
property of → to (l 0 , s 0 ) → (l 1 , s 1 ) to obtain a t 1 such that s 1 t 1 and (l 0 , s
0 ) →
(l 1 , t 1 ). As the certificate is closed we thus get l 1 ∈ L and we can find an s
1 ∈ M l 1
such that t 1 s
1 (and thus s 1 s
1 by transitivity). The induction hypothesis
can then be applied to l 1 , s 1 , and s
1 .
We will now say that a certificate (L, M ) is admissible iff
– it satisfies P ,
– it is closed,
– it covers the initial state (i.e. there is an s
0 ∈ M l 0 such that s 0 s
0 ),
– and there is no l ∈ L with F l.
Corollary 1. If F is monotone w.r.t. and the certificate (L, M ) is admissible,
then l s. (l 0 , s 0 ) →
∗ (l, s) ∧ F l .
2.2 An Abstract Certificate Checker
In practice, the certification process has to consider one additional complication.
A model is typically described in terms of human-readable identifiers, while most
model checkers and the verified model checker Munta [30] in particular represent
these as natural numbers internally to allow for efficient indexing. In our certifier,
this is accounted for by relabeling the human-readable identifiers in a given model
to natural numbers in a first (verified) pre-processing step. To save additional
transformations of the certificate after it was emitted, we let the unverified model
checker additionally emit a textual description of such a renaming. The certifier
then just needs to check that the given renaming is injective to ensure that it
can safely be applied.
Together with the theoretical analysis laid out in the last section, we can thus
derive the following strategy for certifying unreachability:
– An unverified model checker explores the reachable state space of a given
model symbolically and checks that none of the discovered states (l, s) fulfills
F l.