434
S. Wimmer and J. von Mutius
operation when the algorithm is refined to an executable version where sets are
implemented as lists. Line 8 checks that l
is also part of the certificate. Then, in
line 9 the set of corresponding symbolic states is retrieved and converted to a list
ys. Finally, lines 10-12 ensure that all states in xs are subsumed by some state
in ys.
To prove soundness of check , we mainly need correctness theorems for the
monadic combinators monadic list all and monadic list ex. Given a list xs and
a monadic implementation Q i of a predicate Q, they check whether all states
(at least one state) in xs satisfy (satisfies) Q. This is the correctness theorem for
monadic list all, for instance:
(∀x. Q i x ≤ SPEC (λr. r ←→ Q x))
=⇒
monadic list all xs Q i ≤ SPEC (λr. r ←→ list all xs Q)
where list all xs Q holds if and only if Q holds for all elements in xs. After setting
up the IRF’s verification condition generator with this rule and the corresponding
rule for monadic list ex, it is easy to prove that check is sound:
check (L, M ) ≤ SPEC (λr. r =⇒ closed (L, M ))
where the property closed (L, M ) corresponds to condition (∗) from above.
We then use standard refinement techniques to obtain an algorithm check i that
refines check , replacing sets by lists. However, the algorithm is still specified in the
non-determinism monad and therefore not executable. We use a simple technique
to make it executable. Consider the following theorem for monadic list all :
monadic list all xs (λx. return (P x)) = return (list all xs P ) .
It allows us to replace the non-deterministic combinator monadic list all by the
deterministic list all , pushing return to the outside. By exhaustively applying a
set of such rewrite rules we obtain an alternative definition of check i where return
appears only on the outermost level, and the inner term is deterministic and thus
executable. Using these techniques, we obtain a simple certificate checker that
is executable, provided that we can implement the elementary model checking
primitives such as the subsumption check or computing the list of successors of a
state.
2.3 Transferring the Correctness Theorem
For timed automata, the abstract transition system studied above is the zone
graph → ZG(A) of a given (single) automaton A. One can show that it simulates
→ A (completeness of → ZG(A) ):
(l, u) → A (l
, u
) ∧ u ∈ Z =⇒ (∃Z
. (l, Z) → ZG(A) (l
, Z
) ∧ u
∈ Z
) .
This simulation property is sufficient to establish that if there is no reachable
state (l, Z) in → ZG(A) with F l, then no final state (l, u) is reachable in → A :
(l, Z. (l 0 , Z 0 ) →
∗
ZG(A) (l, Z) ∧ F l) ∧ u 0 ∈ Z 0
=⇒
(l, u. (l 0 , u 0 ) →
∗
A (l, u) ∧ F l)
S. Wimmer and J. von Mutius
operation when the algorithm is refined to an executable version where sets are
implemented as lists. Line 8 checks that l
is also part of the certificate. Then, in
line 9 the set of corresponding symbolic states is retrieved and converted to a list
ys. Finally, lines 10-12 ensure that all states in xs are subsumed by some state
in ys.
To prove soundness of check , we mainly need correctness theorems for the
monadic combinators monadic list all and monadic list ex. Given a list xs and
a monadic implementation Q i of a predicate Q, they check whether all states
(at least one state) in xs satisfy (satisfies) Q. This is the correctness theorem for
monadic list all, for instance:
(∀x. Q i x ≤ SPEC (λr. r ←→ Q x))
=⇒
monadic list all xs Q i ≤ SPEC (λr. r ←→ list all xs Q)
where list all xs Q holds if and only if Q holds for all elements in xs. After setting
up the IRF’s verification condition generator with this rule and the corresponding
rule for monadic list ex, it is easy to prove that check is sound:
check (L, M ) ≤ SPEC (λr. r =⇒ closed (L, M ))
where the property closed (L, M ) corresponds to condition (∗) from above.
We then use standard refinement techniques to obtain an algorithm check i that
refines check , replacing sets by lists. However, the algorithm is still specified in the
non-determinism monad and therefore not executable. We use a simple technique
to make it executable. Consider the following theorem for monadic list all :
monadic list all xs (λx. return (P x)) = return (list all xs P ) .
It allows us to replace the non-deterministic combinator monadic list all by the
deterministic list all , pushing return to the outside. By exhaustively applying a
set of such rewrite rules we obtain an alternative definition of check i where return
appears only on the outermost level, and the inner term is deterministic and thus
executable. Using these techniques, we obtain a simple certificate checker that
is executable, provided that we can implement the elementary model checking
primitives such as the subsumption check or computing the list of successors of a
state.
2.3 Transferring the Correctness Theorem
For timed automata, the abstract transition system studied above is the zone
graph → ZG(A) of a given (single) automaton A. One can show that it simulates
→ A (completeness of → ZG(A) ):
(l, u) → A (l
, u
) ∧ u ∈ Z =⇒ (∃Z
. (l, Z) → ZG(A) (l
, Z
) ∧ u
∈ Z
) .
This simulation property is sufficient to establish that if there is no reachable
state (l, Z) in → ZG(A) with F l, then no final state (l, u) is reachable in → A :
(l, Z. (l 0 , Z 0 ) →
∗
ZG(A) (l, Z) ∧ F l) ∧ u 0 ∈ Z 0
=⇒
(l, u. (l 0 , u 0 ) →
∗
A (l, u) ∧ F l)