Verified Certification of Reachability Checking for Timed Automata
431
2 From Model Checking to Certifying Unreachability
This section first describes our approach to certification abstractly. Then, we
detail how the existing formalization of a timed automata model checker was
extended—with rather low effort—to a verified certifier. In practice, networks
of timed automata with additional modeling features such as, e.g. shared state
variables, are used. However, due to the existing verified product construction for
such a formalism [31], it is sufficient to study the case of a single timed automaton
here.
2.1 An Abstract Correctness Theorem
To work towards a rigorous justification of the certification process, we first study
the problem on a more abstract level. Consider a transition system → on states
of type
l ×
s where
l corresponds to the finite state part of timed automata
and
s corresponds to zones. We assume an invariant P on states, i.e.:
P (l 1 , s 1 ) ∧ (l 1 , s 1 ) → (l 2 , s 2 ) =⇒ P (l 2 , s 2 ) .
This invariant essentially represents a restriction of → to valid states. While this
would usually be assumed implicitly, we explicate P here as it is technically more
convenient to do so in the Isabelle/HOL formalization.
The interesting feature that sets timed automata model checking apart is
subsumption. Recall that during the model checking process, it is possible to
first discover some (symbolic) state (l, Z) (a pair of a discrete state l and a zone
Z), and to find at some later point that another reachable state (l, Z
) subsumes
(l, Z) because Z
semantically contains Z
, i.e. Z ⊆ Z
. At this point the state
(l, Z) can be discarded as we know that anything that is reachable from (l, Z) is
also reachable from (l, Z
). Abstractly, subsumption is modeled by some fixed
preorder (i.e. a reflexive and transitive relation) on
s which is a simulation
relation between → and itself:
s 1 s 2 ∧ (l 1 , s 1 ) → (l 2 , t 1 ) ∧ P (l 1 , s 1 ) ∧ P (l 2 , s 2 )
=⇒
∃ t 2 . t 1 t 2 ∧ (l 1 , s 2 ) → (l 2 , t 2 )
In the abstract setting, a certificate consists of a set of discrete states L of
type
l set, and a mapping M of type
l ⇒
s set that gives the set of reachable
symbolic states that were computed for any discrete state l ∈ L. We say that
(L, M ) satisfies P if all states in the certificate (L, M ) satisfy P :
l ∈ L ∧ s ∈ M l =⇒ P (l, s)
Moreover, the certificate needs to be closed. Following Herbreteau et al. [13],
we call a state covered if it is subsumed by another state in the certificate. A
certificate is closed if for each state in the certificate all its successors are covered:
l 1 ∈ L ∧ s 1 ∈ M l 1 ∧ (l 1 , s 1 ) → (l 2 , s 2 ) =⇒ l 2 ∈ L ∧ (∃s 3 ∈ M l 2 . s 2 s 3 ) (∗)
The following key theorem states that all reachable states are covered if the
initial state is covered:
431
2 From Model Checking to Certifying Unreachability
This section first describes our approach to certification abstractly. Then, we
detail how the existing formalization of a timed automata model checker was
extended—with rather low effort—to a verified certifier. In practice, networks
of timed automata with additional modeling features such as, e.g. shared state
variables, are used. However, due to the existing verified product construction for
such a formalism [31], it is sufficient to study the case of a single timed automaton
here.
2.1 An Abstract Correctness Theorem
To work towards a rigorous justification of the certification process, we first study
the problem on a more abstract level. Consider a transition system → on states
of type
l ×
s where
l corresponds to the finite state part of timed automata
and
s corresponds to zones. We assume an invariant P on states, i.e.:
P (l 1 , s 1 ) ∧ (l 1 , s 1 ) → (l 2 , s 2 ) =⇒ P (l 2 , s 2 ) .
This invariant essentially represents a restriction of → to valid states. While this
would usually be assumed implicitly, we explicate P here as it is technically more
convenient to do so in the Isabelle/HOL formalization.
The interesting feature that sets timed automata model checking apart is
subsumption. Recall that during the model checking process, it is possible to
first discover some (symbolic) state (l, Z) (a pair of a discrete state l and a zone
Z), and to find at some later point that another reachable state (l, Z
) subsumes
(l, Z) because Z
semantically contains Z
, i.e. Z ⊆ Z
. At this point the state
(l, Z) can be discarded as we know that anything that is reachable from (l, Z) is
also reachable from (l, Z
). Abstractly, subsumption is modeled by some fixed
preorder (i.e. a reflexive and transitive relation) on
s which is a simulation
relation between → and itself:
s 1 s 2 ∧ (l 1 , s 1 ) → (l 2 , t 1 ) ∧ P (l 1 , s 1 ) ∧ P (l 2 , s 2 )
=⇒
∃ t 2 . t 1 t 2 ∧ (l 1 , s 2 ) → (l 2 , t 2 )
In the abstract setting, a certificate consists of a set of discrete states L of
type
l set, and a mapping M of type
l ⇒
s set that gives the set of reachable
symbolic states that were computed for any discrete state l ∈ L. We say that
(L, M ) satisfies P if all states in the certificate (L, M ) satisfy P :
l ∈ L ∧ s ∈ M l =⇒ P (l, s)
Moreover, the certificate needs to be closed. Following Herbreteau et al. [13],
we call a state covered if it is subsumed by another state in the certificate. A
certificate is closed if for each state in the certificate all its successors are covered:
l 1 ∈ L ∧ s 1 ∈ M l 1 ∧ (l 1 , s 1 ) → (l 2 , s 2 ) =⇒ l 2 ∈ L ∧ (∃s 3 ∈ M l 2 . s 2 s 3 ) (∗)
The following key theorem states that all reachable states are covered if the
initial state is covered: