Verified Certification of Reachability Checking for Timed Automata
429
That is, each transition consists of a delay step that advances all clocks by some
amount of time, followed by an action step that takes a transition and resets the
clocks annotated to the transition. Given a final state predicate F and an initial
state (l 0 , u 0 ), we are interested in whether (l 0 , u 0 ) →
∗
A (l, u) for any l, u with F l.
In Figure 1, the final state is l 3 (i.e. F l ←→ l = l 3 ). As the guard for action a 4
is never enabled, l 3 is unreachable.
Model Checking Due to the use of clock valuations, the state space of timed
automata is inherently infinite. Thus, model checking algorithms for timed
automata are based on the idea of abstracting from concrete valuations to sets
of clock valuations of type (nat ⇒ real ) set, often called zones. The resulting
transition system of reachable states from an initial zone is called the zone graph.
It is explored in an on-the-fly manner, computing successors on zones, which
are typically represented symbolically as Difference Bound Matrices (DBMs).
Knowledge of this data structure is not necessary to understand the rest of the
paper. Thus we refer the interested reader to Bengtsson and Yi [4] and to Wimmer
and Lammich [29,31] for a verification of this data structure. In the remainder
we will only use the term “zones” instead of referring to their implementation as
DBMs.
The delicate part of this method is that the number of reachable zones could
still be infinite. Therefore, over-approximations (or abstractions) of zones are
computed to obtain a finite search space. For our purpose, it sufficient to assume
an abstraction operator α indeed computes an over-approximation, i.e. Z ⊆ α(Z)
for any zone Z. We call the version of the zone graph where abstractions are
applied the abstract zone graph [13]. For a number of such abstraction operators,
it can be shown that the abstract zone graph is sound and complete
2 . The
proofs are rather intricate, however. Thus formalizing them would be a big effort.
By focusing on certification of unreachability, this problem vanishes, as we only
need to ensure that any state (l, Z) that we deem reachable in the zone graph is
subsumed by some state (l, Z
) with Z ⊆ Z
that is part of the certificate and
that was computed by the abstraction (i.e. Z
= α(Z 1 ) for some Z 1 ).
Certificates by Example Figure 2 depicts the zone graph of the automaton in
Figure 1. Each zone Z is given as a clock constraint cc such that Z = {u | u |= cc}.
A model checker like Munta would have to explore the full zone graph before
being able to decide that l 3 is unreachable. Any model checker that uses the same
abstraction technique as Munta [2] would not be able to benefit from abstractions
for this example and thus the abstract zone graph is the same as the zone graph.
However, such a model checker could apply subsumptions while exploring the zone
graph. That is, when a symbolic state of the form (l 2 , {u | u |= c 1 = 0∧c 2 < k+1})
is explored, the state (l 2 , {u | u |= c 1 = 0 ∧ c 2 < k}) can safely be discarded.
This means that at the end of the model checking process, only the three
states in Figure 3a will be stored. The solid edges are part of the zone graph,
2 Soundness: for every abstract run, there is a concrete instantiation. Completeness:
every concrete run can be abstracted.
429
That is, each transition consists of a delay step that advances all clocks by some
amount of time, followed by an action step that takes a transition and resets the
clocks annotated to the transition. Given a final state predicate F and an initial
state (l 0 , u 0 ), we are interested in whether (l 0 , u 0 ) →
∗
A (l, u) for any l, u with F l.
In Figure 1, the final state is l 3 (i.e. F l ←→ l = l 3 ). As the guard for action a 4
is never enabled, l 3 is unreachable.
Model Checking Due to the use of clock valuations, the state space of timed
automata is inherently infinite. Thus, model checking algorithms for timed
automata are based on the idea of abstracting from concrete valuations to sets
of clock valuations of type (nat ⇒ real ) set, often called zones. The resulting
transition system of reachable states from an initial zone is called the zone graph.
It is explored in an on-the-fly manner, computing successors on zones, which
are typically represented symbolically as Difference Bound Matrices (DBMs).
Knowledge of this data structure is not necessary to understand the rest of the
paper. Thus we refer the interested reader to Bengtsson and Yi [4] and to Wimmer
and Lammich [29,31] for a verification of this data structure. In the remainder
we will only use the term “zones” instead of referring to their implementation as
DBMs.
The delicate part of this method is that the number of reachable zones could
still be infinite. Therefore, over-approximations (or abstractions) of zones are
computed to obtain a finite search space. For our purpose, it sufficient to assume
an abstraction operator α indeed computes an over-approximation, i.e. Z ⊆ α(Z)
for any zone Z. We call the version of the zone graph where abstractions are
applied the abstract zone graph [13]. For a number of such abstraction operators,
it can be shown that the abstract zone graph is sound and complete
2 . The
proofs are rather intricate, however. Thus formalizing them would be a big effort.
By focusing on certification of unreachability, this problem vanishes, as we only
need to ensure that any state (l, Z) that we deem reachable in the zone graph is
subsumed by some state (l, Z
) with Z ⊆ Z
that is part of the certificate and
that was computed by the abstraction (i.e. Z
= α(Z 1 ) for some Z 1 ).
Certificates by Example Figure 2 depicts the zone graph of the automaton in
Figure 1. Each zone Z is given as a clock constraint cc such that Z = {u | u |= cc}.
A model checker like Munta would have to explore the full zone graph before
being able to decide that l 3 is unreachable. Any model checker that uses the same
abstraction technique as Munta [2] would not be able to benefit from abstractions
for this example and thus the abstract zone graph is the same as the zone graph.
However, such a model checker could apply subsumptions while exploring the zone
graph. That is, when a symbolic state of the form (l 2 , {u | u |= c 1 = 0∧c 2 < k+1})
is explored, the state (l 2 , {u | u |= c 1 = 0 ∧ c 2 < k}) can safely be discarded.
This means that at the end of the model checking process, only the three
states in Figure 3a will be stored. The solid edges are part of the zone graph,
2 Soundness: for every abstract run, there is a concrete instantiation. Completeness:
every concrete run can be abstracted.