Verified Certification of Reachability Checking for Timed Automata
437
3.2 Integer Representation
Types such as int or nat are unbounded in Isabelle/HOL meaning they are
implemented with the help of big integers in the target languages. To improve performance, we want to use machine integers instead, and instruct Isabelle/HOL’s
code generator to do that. This is still sound: SML’s standard integer operations
throw an exception if an overflow occurs instead of silently wrapping around. The
code generator can only achieve partial correctness anyway: if program execution
does not fail, then its result is consistent with the evaluated HOL term.
3.3 Refined Code Equations
The last type of optimizations we use can be considered to belong to the category of micro-optimizations. These are improved code generator translations for
elementary operations and combinators. We employ such improved translations
to use native implementation language primitives to convert from mutable to
immutable arrays and back. The other such optimizations we use, is to directly
use integer values as counters in imperative loops instead of a natural number
representation that would box the integers in a data constructor. In the same
way, we use integers directly for array indexing.
4 Certificate Compression
In this section, we present two techniques to compress the unreachability certificate. By compression we mean reducing the number of zones that are present in
the certificate for each discrete state, using the unverified model checker. The
first technique relies on subsumption. As explained above, it is possible that the
model checker adds a zone Z to the set of explored states and later another zone
Z
with Z ⊆ Z
(i.e. Z
subsumes Z). Thus the first technique simply filters the
set w.r.t. ⊆ in the end.
The second technique relies on the following idea: we replace one or more
zones by their union, and check that the state space is still closed. This means
that we have to check that all the successors of the larger zone are still covered
by the current set of states. In that case, we can discard the old zones, and
replace them by their union. As the union of two zones is not necessarily convex
and thus cannot be represented as a DBM, we do not compute a precise union
of zones but their convex hull. This operation is rather cheap as it amounts to
taking the pointwise maximum of DBM entries. After computing the convex hull
of a number of zones (in canonical form), we only need to apply the expensive
operation to restore a canonical form once.
The latter technique yields a whole family of compression algorithms by
iterating one of the following operations for each discrete state until a fixed-point
is reached:
a) the convex hull of all zones is computed;
b) the convex hull of the first two zones is computed;
437
3.2 Integer Representation
Types such as int or nat are unbounded in Isabelle/HOL meaning they are
implemented with the help of big integers in the target languages. To improve performance, we want to use machine integers instead, and instruct Isabelle/HOL’s
code generator to do that. This is still sound: SML’s standard integer operations
throw an exception if an overflow occurs instead of silently wrapping around. The
code generator can only achieve partial correctness anyway: if program execution
does not fail, then its result is consistent with the evaluated HOL term.
3.3 Refined Code Equations
The last type of optimizations we use can be considered to belong to the category of micro-optimizations. These are improved code generator translations for
elementary operations and combinators. We employ such improved translations
to use native implementation language primitives to convert from mutable to
immutable arrays and back. The other such optimizations we use, is to directly
use integer values as counters in imperative loops instead of a natural number
representation that would box the integers in a data constructor. In the same
way, we use integers directly for array indexing.
4 Certificate Compression
In this section, we present two techniques to compress the unreachability certificate. By compression we mean reducing the number of zones that are present in
the certificate for each discrete state, using the unverified model checker. The
first technique relies on subsumption. As explained above, it is possible that the
model checker adds a zone Z to the set of explored states and later another zone
Z
with Z ⊆ Z
(i.e. Z
subsumes Z). Thus the first technique simply filters the
set w.r.t. ⊆ in the end.
The second technique relies on the following idea: we replace one or more
zones by their union, and check that the state space is still closed. This means
that we have to check that all the successors of the larger zone are still covered
by the current set of states. In that case, we can discard the old zones, and
replace them by their union. As the union of two zones is not necessarily convex
and thus cannot be represented as a DBM, we do not compute a precise union
of zones but their convex hull. This operation is rather cheap as it amounts to
taking the pointwise maximum of DBM entries. After computing the convex hull
of a number of zones (in canonical form), we only need to apply the expensive
operation to restore a canonical form once.
The latter technique yields a whole family of compression algorithms by
iterating one of the following operations for each discrete state until a fixed-point
is reached:
a) the convex hull of all zones is computed;
b) the convex hull of the first two zones is computed;