Hybrid Systems Verification by Location Elimination

Andreas Nonnengart

Deutsches Forschungszentrum für Künstliche Intelligenz (DFKI GmbH) Im Stadtwald, Geb. 36, 66123 Saarbrücken, Germany http://www.dfki.de/˜ nonnenga/

                        Andreas.Nonnengart@dfki.de

Abstract. In this paper we propose a verification method for hybrid systems that is based on a successive elimination of the various system locations involved. Briefly, with each such elimination we compute a weakest precondition (strongest postcondition) on the predecessor (successor) locations such that the property to be proved cannot be violated. Experiments show that this approach is particularly interesting in cases where a standard reachability analysis would require to travel often through some of the given system locations.

1 Introduction

Hybrid Systems are real-time systems that are embedded in analog environments. They contain discrete and continuous components and interact with the physical world through sensors and actuators. A common model for hybrid systems can be found in hybrid automata. These are finite graphs whose nodes correspond to global states as illustrated in the famous “Leaking Gas Burner” example [ACH^{+}95]:

\begin{matrix}ẋ = 1 \\ ẏ = 1 \\ ż = 1 \\ x ≤ 1 \end{matrix}  ^{\begin{matrix}ẋ = 1 \\ ẏ = 1 \\ ż = 0 \end{matrix}} Leak  Non-Leak_{x := 0}_{y := 0, z := 0}_{⊤ | x := 0}_{x ≥ 30 | x := 0}

Nodes “Leak” and “Non-Leak” represent discrete locations, whereas x, y, and z are data variables. Each location may contain a location invariant (x ≤ 1 in the example) and the continuous activity which describes how the values of the data variables change in time. In the above example the value of x and y increase by 1 per time unit (say, second), i.e., the first derivative of the function describing the behavior of x and y over time is the constant 1. z also increases by one per second in location “Leak”, however, it remains unchanged (ż = 0) in location “Non-Leak”. Edges are annotated with guards and discrete actions. Guards form a constraint on the data variables to hold if a transition via the corresponding edge is to be performed. The discrete action specifies how the data variables are to be changed after taking the transition. In the above example the guard of the edge from “Leak” to “Non-Leak” is logical truth (⊤), i.e., no special condition has to be fulfilled, whereas the guard of the edge from “Non-Leak” to “Leak” is x ≥ 30, i.e., this edge may only be taken in case the value of the data variable x is at least 30. The discrete action for both edges is to reset x to 0.

A computation of such an automaton is a sequence of state changes (steps). Within each step the system state evolves continuously according to a dynamical law until a transition from one node to another one occurs.

Since hybrid systems typically operate in safety-critical situations, the development of rigorous analysis techniques is of high importance. In the last ten years several proposals for a verification methodology for hybrid systems arose [ACD90, ACH^{+}95, ACHH93, AD94, AH92, AHH96, AHS96, ANKS95, GNRR93, Hen96, HNSY92]. Most of them are based on a so-called (forward or backward) reachability analysis. Intuitively, a forward reachability analysis (for safety properties) performs the following operation: starting from the initial situation (state), all possible (immediate) time and edge successor states are computed. Then the resulting set is reentered as an input to compute further time and edge successors, and so on. This will go on until no further new states can be derived (reached). Provided this procedure at all terminates, it ultimately comes up with the set of all reachable states (reachable from the initial state) which may be used to check the property to be proved.

Backward reachability, on the other hand, starts from a description of the states that do not fulfill the property to be proved and tries to compute all possible predecessor states, i.e., all the states from which one of the unsafe states could possibly be reached. Again, upon termination, it ends up with a set of states all of whose elements may lead to an unsafe situation, and what remains to be done is to check whether the initial state is contained in this set or not.

At the first glance, at least for forward reachability, and upon termination, it can hardly be seen that anything else could behave better. After all, forward reachability computes exactly the reachable states (and nothing else) and we need to know about all the reachable states in order to perform our verification task. Indeed, forward reachability does not compute any redundant information. However, it may perform redundant computations. For instance, if the property to be proven requires several passes through certain locations, the actual effect is usually very similar to earlier (or later) passes. Only the values of the variables involved might vary a bit, although in some more or less regular way.

The purpose of the approach proposed in this paper is to show how to gain such a knowledge and how to take advantage of it, i.e., to compute the behavior of locations once and for all and to forget about these locations later on. This can result in certain extra properties to be proved for the other locations (weakest preconditions or strongest postconditions) that take over the responsibility of the location just eliminated. The following example illustrates this:

\begin{matrix}ẋ = 2 \\ ẏ = 1 \\ x ≤ y \end{matrix} L_{1}  L_{2}  L_{3}_{x ≤ y}_{x = y | x := 0; y := 0}

Let us assume that we want to prove that x+y ≤ 10 is an invariant of the system (from which we can only see a small portion in this illustration). It might very well be that any reachability analysis will have to go through location L_{2} several times and therefore we want to eliminate this very location by computing a weakest precondition on location L_{1} that guarantees that L_{2} could impossibly violate the desired property. The approach to be presented in this paper will come up with the following result: the invariant indeed holds for the whole system if and only if the invariant holds for the “simplified” system

x ≤ y | x := 0; y := 0  L_{1}  L_{3}

provided we can guarantee that x ≤ y → 2y ≤ x + 5 whenever we are within location L_{1}. In what follows we describe formally how such a condition can be computed and how this method can be used as a verification tool for hybrid systems.

2 Preliminaries

Given a fixed variable set X we define the set CT of Constraint Terms (over the variable set X) as the smallest set containing the reals and the set X and that is closed under addition, subtraction and multiplication with reals. The set CF of Constraint Formulas (over the variable set X) is defined as the smallest set containing ⊤, ⊥ (logical truth and falsity respectively), t_{1} > t_{2}, t_{1} ≥ t_{2}, t_{1} < t_{2}, t_{1} ≤ t_{2}, and t_{1} = t_{2} (where t_{1} and t_{2} are constraint terms), and that is closed under logical conjunction.

A hybrid system is a tuple of the form H = (X, L, E, dif, inv, guard, act) where X is a finite set of real-valued data variables, L is a finite set of locations, i.e., nodes of a graph, E ⊆ L × L is a finite (multi)set of transitions, i.e., edges of the graph with nodes from L, dif: L × X ↦ CT is a mapping that associates with each location and each data variable a constraint term (over X), inv: L ↦ CF is a mapping that associates with each location a constraint formula, representing the location invariant, guard: E ↦ CF is a mapping that associates with each edge a constraint formula, representing the enabling condition for this transition, and, act: E ×X ↦ CT is a mapping that associates with each edge and each data variable a constraint term, representing the value of the variable after traveling along the edge.

As usual, we define a state of a hybrid system as a pair (L, ϕ) where L ∈ L is a location and ϕ: X ↦ ℝ is a valuation of the data variables. ϕ naturally extends to (constraint) terms and (constraint) formulas. A state (L, ϕ) is called admissible if ϕ(inv(L)) holds. Given two admissible states s = (L, ϕ) and s′ = (L′, ϕ′) we say that s′ is transition-reachable from s – denoted by s ↦^{tr} s′ – if there exists a transition t = (L, L′) ∈ E with source L and target L′, and both ϕ(guard(t)) and ϕ′(x) = ϕ(act(t, x)) for each x ∈ X. We call s′ timely-reachable from s with delay δ – denoted by s ↦^{δ} s′ – where δ is a non-negative real number, if L = L′ and for each x ∈ X there exists a differentiable function f_{x}: [0, δ] ↦ ℝ, with the first derivative ḟ_{x}: (0, δ) ↦ ℝ, such that (1) f_{x}(0) = ϕ(x) and f_{x}(δ) = ϕ′(x) and (2) for all ϵ ∈ ℝ with 0 < ϵ < δ: both inv(L)[x_{1}/f_{x_{1}}(ϵ), …, x_{n}/f_{x_{n}}(ϵ)] and ḟ_{x}(ϵ) = dif(L, x)[x_{1}/f_{x_{1}}(ϵ), …, x_{n}/f_{x_{n}}(ϵ)] are true. s′ is timely-reachable from s – denoted by s ↦^{⋆} s′ – if there exists a non-negative δ ∈ ℝ such that s ↦^{δ} s′. s′ is said to be reachable from s if (s, s′) ∈ (↦^{⋆} ∪ ↦^{tr})^{∗}. A run ρ of H with initial state σ_{0} = (L_{0}, ϕ_{0}) is a maximal sequence of states represented as

ρ = σ_{0} ↦_{f_{0}}^{t_{0}} σ_{1} ↦_{f_{1}}^{t_{1}} σ_{2} ↦_{f_{2}}^{t_{2}} σ_{3} ↦_{f_{3}}^{t_{3}} ⋯

where t_{i} ∈ ℝ^{≥0} and f_{i}: [0, t_{i}] ↦ (X ↦ ℝ), such that (i) f_{i}(0) = ϕ_{i}, (ii) inv(L_{i})[X/f_{i}(t)(X)] holds for all 0 ≤ t ≤ t_{i}, (iii) (L_{i}, f_{i}(t_{i})) ↦^{tr} σ_{i+1} and (iv) for all 0 ≤ t′ ≤ t′ + δ ≤ t_{i} : (L_{i}, f_{i}(t′)) ↦^{δ} (L_{i}, f_{i}(t′ + δ)). The set of states contained in such a run ρ is given as {(L_{i}, f_{i}(t)) | t ∈ ℝ, 0 ≤ t ≤ t_{i}}. The set of all runs of a hybrid system H with initial state σ is denoted by runs(H, σ). A position π of a run ρ = σ_{0} ↦_{f_{0}}^{t_{0}} σ_{1} ↦_{f_{1}}^{t_{1}} σ_{2} ↦_{f_{2}}^{t_{2}} σ_{3} ↦_{f_{3}}^{t_{3}} ⋯ is a pair π = (i, r) ∈ ℕ×ℝ such that 0 ≤ r ≤ t_{i}. Positions are ordered lexicographically, i.e., (i, r) < (j, s) if and only if i < j or (i = j and r < s). Also, (i, r) ≤ (j, s) if and only if (i, r) < (j, s) or (i = j and r = s). By ρ(π) with π = (i, r) we denote the state (L_{i}, f_{i}(r)). A run is said to be non-zeno if ∑ t_{i} diverges. In the sequel we assume that the runs of the hybrid system under consideration are all non-zeno.^{1}

In order to formulate properties of hybrid systems we consider (a fragment of) ICTL, the Integrator Computation Tree Logic [AHH96]. For simplicity we omit the Until-operators in this paper. Their introduction does not cause much more effort, though (see [Non99]).

Given some hybrid system with locations L and data variables X, the set of ICTL formulas is defined as the smallest set containing all constraint formulas from CF over X, all location names from L, and that is closed under the usual boolean connectives together with temporal (ICTL) operators AG , EF , EG , and AF . Moreover, if Φ is an ICTL formula, z is a new data variable, and {L_{1}, …, L_{n}} ∈ L then z^{{L_{1},... ,L_{n}}}.Φ is an ICTL formula as well. Intuitively, the

1 The assumption of non-zenoness implies that hybrid systems are deadlock-free, i.e., there is no reachable state that has no successor. So-called livelocks, however, are not excluded. This means that we absolutely allow states which have only themselves as future states. The latter case just states that the situation does not change in time, whereas the former case (deadlock) would claim that time itself has come to an end.

temporal operators AG Φ, AF Φ, EG Φ, EF Φ mean “always”, “inevitably”, “possibly always”, and “possibly” respectively. Their formal semantics with respect to hybrid systems is defined below.

Definition 1. Given a hybrid system H = (X, L, E, dif, inv, guard, act) and a state σ = (L, ϕ), the semantics of ICTL with respect to H and σ is defined as:

H, σ ⊧ c  iff ⊧ ϕ(c) for constraint formula c
H, σ ⊧ N  iff locations N and L are identical
H, σ ⊧ ¬Φ iff H, σ |̸= Φ
H, σ ⊧ Φ ∧ Ψ iff H, σ ⊧ Φ & H, σ ⊧ Ψ

and similarly for the other boolean connectives

H, σ ⊧ AG Φ iff ∀ρ (ρ ∈ runs(H, σ) ⇒ ∀π (π ∈ positions(ρ) ⇒ H, ρ(π) ⊧ Φ))
H, σ ⊧ EG Φ iff ∃ρ (ρ ∈ runs(H, σ) & ∀π (π ∈ positions(ρ) ⇒ H, ρ(π) ⊧ Φ))
H, σ ⊧ z^{N} .Φ iff H^{z^{N}} , (L, ϕ[z/0]) ⊧ Φ,  where N ⊆ L,

where EF Φ ≡ ¬AG ¬Φ and AF Φ ≡ ¬EG ¬Φ. By H^{z^{{L_{1},... ,Ln}}} we mean the extended system we obtain by adding the new clock z (initialized with 0) which is supposed to run with slope 1 within locations L_{1}, …, L_{n} and with slope 0, i.e., it is stopped, for all other locations.

Given a variable valuation ϕ we define the new valuation ϕ[z/0] as

ϕ[z/0](x) = \{ \begin{matrix}ϕ(x) & if x ≠ z \\ 0 & otherwise. \end{matrix}

3 The Verification Approach

Here we restrict our view to linear hybrid systems, where dif(L, x) is a constant, say k_{L}^{x}, for each location L and data variable x. This restriction can easily be weakened to rectangular hybrid systems (where dif(L, x) is given as an interval of reals) without any real effort. For a better readability we denote sequences of the form x_{1} + k_{L}^{x_{1}}δ, …, x_{n} + k_{L}^{x_{n}}δ by X + k_{L}^{X}δ where X = {x_{1}, …, x_{n}}, and, similarly we mean L(act(T, x_{1}), …, act(T, x_{n})) whenever we write L(act(T, X)).

3.1 First-order Theories for Reachability and Inevitability

As usual, an interpretation ℑ = (D, ℑ_{L}, ϕ) for a first-order theory associated with a hybrid system H with locations L has a fixed domain D (the reals or the rationals, say), a valuation ϕ for the data variables in X, and a meaning function ℑ_{L} for the locations in L such that ℑ_{L}(L) ∈ D^{n}, where n is the number of data variables in X. A model of a formula Φ is an interpretation satisfying this formula. We often also speak of a model as a set of ground atoms of the form

{L(ℑ(t_{1}), …, ℑ(t_{n})) | ℑ ⊧ L(t_{1}, …, t_{n})}, where t_{i} are constraint terms} where ℑ is a model in the above sense. Interpretations (models) are partially ordered by set-inclusion. A minimal model of Φ is a model of Φ such that there exists no proper subset of it that also satisfies Φ.

We now define two different kind of first-order theories for a given hybrid system: one that is responsible for the possible states, and one that is responsible for the unavoidable states.

Definition 2 (Reachability Theory). Let H = (X, L, E, dif, inv, guard, act) be a hybrid system. For each L ∈ L we define the first-order theory

∀X L(X) → \{ \begin{matrix}inv(L) ∧ \\ ∀δ (δ ≥ 0 ∧ inv(L)[X/X + k_{L}^{X}δ] → L(X + k_{L}^{X}δ)) ∧ \\ ⋀_{T =(L,N)∈E}guard(T) → N(act(T, X)) \end{matrix}

as the local reachability theory of L in H, R_{H}^{L} for short. By the reachability theory of H – which we call R_{H}, or simply R if H is clear from the context – we understand the conjunction of all local reachability theories, i.e., R_{H} = ⋀_{L∈L}R_{H}^{L}.

What the reachability theory expresses is that (for each location L) (i) the location invariant must hold, (ii) that there is a possible time transition, and (iii) for each outgoing edge: if the enabling guard is true then the target location can be reached provided the corresponding discrete action has been peformed.

Definition 3 (Inevitability Theory). Let H = (X, L, E, dif, inv, guard, act) be a hybrid system. For each L ∈ L we define the first-order theory

∀X L(X) → inv(L)

∀X L(X) → \{ \begin{matrix}∀δ δ ≥ 0 → L(X + k_{L}^{X}δ) ∨ \\ ∃δ \{ \begin{matrix}δ ≥ 0 ∧ \\ ∀δ′ 0 ≤ δ′ ≤ δ → L(X + k_{L}^{X}δ′) ∧ \\ ⋁_{T =(L,N)∈E} & guard(T)[X/X + k_{L}^{X}δ] ∧ N(act(T, X)[X/X + k_{L}^{X}δ]) \end{matrix} \end{matrix}

as the local inevitability theory of L in H, I_{H}^{L} for short. By the inevitability theory of H – which we call I_{H}, or simply I if H is clear from the context – we understand the conjunction of all local inevitability theories, i.e., I_{H} = ⋀_{L∈L}I_{H}^{L}.

The inevitability theory might require some more explanation. In a sense it expresses (for each given state) between which possibilities the system can choose. The first part of any local inevitability theory is trivial. It just guarantees the mere fact that for each location predicate the corresponding location invariant is supposed to hold. The second part is more complicated and more interesting.

Note that, given an arbitrary state represented by the location predicate L(X), either the system remains forever in this location, i.e., ∀δ δ ≥ 0 → L(X + k_{L}^{X}δ), or it will sooner or later leave this very location. In the latter case we know that there is a time delay δ after which one of the guards of the outgoing edges is true and until then the system remains within location L. This is exactly what is expressed by the complicated second part of the local inevitability theories.

Intuitively, the reachability theory tells us what can be done in certain situations (states), whereas the inevitability theory describes what must be done, it collects all the immediate future possibilities.

The importance of these two theories will become apparent from the following Lemma.

Lemma 1. Given a hybrid system H and an initial state (L, ϕ).

– The (unique) minimal model of L(ϕ(X))∧R_{H} corresponds to the set of states that are reachable from (L, ϕ) in the hybrid system H.

– Each minimal model of L(ϕ(X)) ∧ I_{H} corresponds to the set of states of one of the runs of H.

– The set of states of each run of H forms a model of L(ϕ(X)) ∧ I_{H}.

Proof. Can be found in [Non99].

The above lemma provides us with a formal connection between the reachability theory (inevitability theory) and the reachable (inevitable) states. Briefly, Φ holds always (AG Φ) iff Φ holds in all reachable states iff Φ holds for every element in the unique minimal model of the reachability theory (together with the initial state) iff Φ holds for every element of some model of the reachability theory (together with the initial state). This observation leads to the following definition and main theorem.

Definition 4 (Characteristic Constraint Formulas). The (second-order) formula associated with an ICTL formula Φ, the hybrid system H, and location L, ⌈Φ⌉_{H}^{L(X)}, representing a characteristic constraint formula for Φ given H in L, is recursively defined by

⌈c⌉_{H}^{L(X)}  = c
⌈L′⌉_{H}^{L(X)} = \{ \begin{matrix}⊤ if L and L′ are identical \\ ⊥ otherwise \end{matrix}
⌈¬Φ⌉_{H}^{L(X)} = ¬⌈Φ⌉_{H}^{L(X)}
⌈Φ ∧ Ψ⌉_{H}^{L(X)} = ⌈Φ⌉_{H}^{L(X)} ∧ ⌈Ψ⌉_{H}^{L(X)}

and similarly for the other boolean connectives

⌈z^{N} .Φ⌉_{H}^{L(X)} = ⌈Φ⌉_{H^{z^{N}}}^{L(X,0)} where N ⊆ L
⌈AG Φ⌉_{H}^{L(X)} = ∃L_{1}, …, L_{n} L(X) ∧ R_{H} ∧ ⋀_{N∈L} ∀X N(X) → ⌈Φ⌉_{H}^{N(X)}
⌈EG Φ⌉_{H}^{L(X)} = ∃L_{1}, …, L_{n} L(X) ∧ I_{H} ∧ ⋀_{N∈L} ∀X N(X) → ⌈Φ⌉_{H}^{N(X)}

Theorem 1. Given a hybrid system H with data variables X, an initial state (L, ϕ) and an ICTL formula Φ. Then

H, (L, ϕ) ⊧ Φ  iff  ⊧ ϕ (⌈Φ⌉_{H}^{L(X)})

Proof. By induction on the structure of Φ. The base cases are trivial. Also in case of a boolean connective there are no problems at all. The induction steps are exemplified for the case Φ = AG Ψ. For the other cases see [Non99].

H, (L, ϕ) ⊧ AG Ψ

iff H, σ ⊧ Ψ for every σ reachable from (L, ϕ)
iff ∀σ ((L, ϕ), σ) ∈ (↦^{⋆} ∪ ↦^{tr})^{∗} ⇒ H, σ ⊧ Ψ
iff ∀N, ϕ′ N(ϕ′(X)) ∈ minMod(L(ϕ(X)) ∧ R_{H}) ⇒ H, (N, ϕ′) ⊧ Ψ

(Lemma 1)

iff ∃ℑ ℑ ⊧ L(ϕ(X)) ∧ R_{H} & ∀N, ϕ′ (N, ϕ′) ∈ ℑ ⇒ H, (N, ϕ′) ⊧ Ψ
iff ∃ℑ ℑ ⊧ L(ϕ(X)) ∧ R_{H} & ∀N, ϕ′ (N, ϕ′) ∈ ℑ ⇒ ⊧ ϕ′ (⌈Ψ⌉_{H}^{N(X)})

(induction hypothesis)

iff ∃ℑ ℑ ⊧ L(ϕ(X)) ∧ R_{H} & ℑ ⊧ ⋀_{N∈L} ∀X N(X) → ⌈Ψ⌉_{H}^{N(X)}
iff ∃ℑ ℑ ⊧ L(ϕ(X)) ∧ R_{H} ∧ ⋀_{N∈L} ∀X N(X) → ⌈Ψ⌉_{H}^{N(X)}
iff ⊧ ∃L_{1}, …, L_{n} L(ϕ(X)) ∧ R_{H} ∧ ⋀_{N∈L} ∀X N(X) → ⌈Ψ⌉_{H}^{N(X)}
iff ⊧ ϕ (⌈AG Ψ⌉_{H}^{L(X)})

3.2 Eliminating Locations

Theorem 1 tells us that we can solve a hybrid system verification problem by proving the satisfiability of some suitable first-order theory, or equivalently, by showing the validity of some corresponding second-order formula. The Elimination Theorem below helps us in this respect, for it allows us to transform a given second-order formula into an equivalent first-order formula (if this is at all possible).^{2}

2 In general, second-order formulas do not necessarily have a (finite or infinite) firstorder equivalent. However, in case the second-order formula is of the form ∃P Φ, where Φ is a first-order formula that is Horn in P, then we know that there exists a first-order equivalent (which may be infinite, though). Note that proving Safety properties, i.e. proving the validity of second-order formulas involving reachability theories, are just of this form.

Theorem 2 (Elimination Theorem). Let Φ and Ψ be two first-order formulas that are positive with respect to the predicate symbol L. Then

∃L (∀\overline{x} (L(\overline{x}) → Φ) ∧ Ψ) ≡ Ψ [L(\overline{α})/ (νL(\overline{x}).Φ)\overline{x} ; \overline{α}]
where νL(\overline{x}).Φ(L) = ⋀_{i≤ω}Φ^{i}(⊤) with Φ^{0}(⊤) = ⊤, Φ^{n+1}(⊤) = Φ(Φ^{n}(⊤))

The proof of this Theorem can be found in [NS95] (but also see [NS99] and [NOS99]). There also some generalizations and dual forms are examined. For the purpose of this paper, however, the above form suffices.

The Elimination Theorem tells us that any second-order formula of the form ∃L (∀\overline{x} (L(\overline{x}) → Φ) ∧ Ψ) is equivalent to Ψ with every occurrence of L (with actual argument list \overline{α}) within Ψ replaced by the greatest fixpoint of Φ (after instantiating the abstract parameters with the actual arguments). Notice that the second-order formulas we are dealing with are indeed of the form required. Therefore, with each application of the Elimination Theorem we get rid of one of the existentially quantified predicate symbols. Now, since these predicate symbols are just the location names of the hybrid system under consideration, each application of the Elimination Theorem also eliminates one of the locations.

Evidently, it cannot be guaranteed that the fixpoint computation will terminate in general. However, it can easily be shown (see [Non99]) that in case we are about to eliminate a location which has no outgoing edge leading to itself, the fixpoint computation will definitely terminate after two iterations.

Coming back to the example on page 2 where we wanted to examine the effect of eliminating location L_{2}, we now know that we have to compute – in fact, find a first-order equivalent for – the second-order formula

∃L_{2} [ \begin{matrix}∀x, y L_{1}(x, y) → x ≤ y → L_{2}(x, y) ∧ \\ ∀x, y L_{2}(x, y) → \{ \begin{matrix}x ≤ y ∧ \\ x + y ≤ 10 ∧ \\ ∀δ (δ ≥ 0 ∧ x + 2δ ≤ y + δ → L_{2}(x + 2δ, y + δ)) ∧ \\ x = y → L_{3}(0, 0) \end{matrix} \} \end{matrix}

The five conjuncts of the above second-order formula describe the transition from L_{1} to L_{2}, the location invariant for L_{2}, the property to be proved, the time transition for location L_{2}, and the edge transition from L_{2} to L_{3} respectively. In order to apply the Elimination Theorem to this second-order formula, let Ψ = ∀x, y L_{1}(x, y) → x ≤ y → L_{2}(x, y) and Φ = x ≤ y ∧ x + y ≤ 10 ∧ ∀δ (δ ≥ 0 ∧ x + 2δ ≤ y + δ → L_{2}(x + 2δ, y + δ)) ∧ x = y → L_{3}(0, 0). Then Φ^{0}(⊤) = ⊤, Φ^{1}(⊤) = x ≤ y ∧ x + y ≤ 10 ∧ x = y → L_{3}(0, 0), Φ^{2}(⊤) = Φ^{1}(⊤) ∧ x ≤ y → 2y ≤ 5 + x, and Φ^{3}(⊤) = Φ^{2}(⊤) as can easily be checked by the reader. We thus have found the fixpoint and substitute it for L_{2} in Ψ resulting in

\begin{matrix}∀x, y L_{1}(x, y) → x ≤ y → L_{3}(0, 0) \\ ∀x, y L_{1}(x, y) → x ≤ y → 2y ≤ x + 5 \end{matrix}

The first formula describes just the new edge to be introduced. The second formula, on the other hand, tells us about the necessary and sufficient condition on the data variables for location L_{1} such that it would be impossible to violate x + y ≤ 10 in location L_{2}.

3.3 Examples and Experimental Results

There exists a prototype implementation of the Elimination Approach (for proving safety-properties) written in Sicstus-Prolog with the CLP(Q,R)-library for constraint handling. It has been tested on a lot of examples known from the literature (or taken from hybrid system verifier distributions). The experimental results can briefly be summarized as follows: as already expected in the introduction, standard forward reachability (if it at all terminates) can hardly be beaten in case we are about to prove safety properties for non-trivial systems that only require a single pass through the reachable locations. This is the case for instance for the famous “audio-protocol”-example.^{3} For other, unfortunately still trivial systems like the “Leaking Gas Burner” or the “Billiards”-example, the Elimination Approach showed a slightly better behavior than standard reachability analysis.^{4} However, in such cases, where safety properties can be proved in milliseconds anyway, this can hardly be called evidence. The lack of non-trivial hybrid system in the literature that require several passes through some of their locations made us compose our own examples. They are designed as simple as possible such that they may serve to illustrate the effect of the Elimination Approach compared to reachability analysis methods. Two such examples are given below.

A Silly Multiplier This is an example within which three numbers a, b, and c are to be multiplied and the final product is stored in the data variable p. The multiplication is performed by successively adding 1 to p, similar to the nested for-loop

for (w = 0; w < c; w++)
for (v = 0; v < b; v++)
for (u = 0; u < a; u++)
p := p + 1

3 In case of more trivial such examples like the “Water-Level-Monitor” or the

“Railroad-Gate-Controller” there is not so much of a difference. 4 It should be noted here that it is in fact very easy to compare the Elimination

Approach with standard reachability analysis methods for, in a sense, reachability analysis can be viewed as a special case of the Elimination Approach: we just have to move the location names to the argument list as a further additional argument (leaving a single unique dummy predicate as the only remaining predicate symbol). This then leads to backward reachability, whereas, by using a dual form of the Elimination Theorem, we can also get forward reachability (see also [Non99]).

\begin{matrix}ẋ = 1 \\ ṗ = 1 \\ u̇ = 0 \\ v̇ = 0 \\ ẇ = 0 \\ x ≤ 1 \end{matrix} \begin{matrix}ẋ = 1 \\ ṗ = 0 \\ u̇ = 1 \\ v̇ = 0 \\ ẇ = 0 \\ x ≤ 1 \end{matrix}  \begin{matrix}ẋ = 1 \\ ṗ = 0 \\ u̇ = 0 \\ v̇ = 1 \\ ẇ = 0 \\ x ≤ 1 \end{matrix} \begin{matrix}ẋ = 1 \\ ṗ = 0 \\ u̇ = 0 \\ v̇ = 0 \\ ẇ = 1 \\ x ≤ 1 \end{matrix} \begin{matrix}x = 1 \\ x := 0 \end{matrix} \begin{matrix}x = 1 \\ u < a \\ x := 0 \end{matrix} \begin{matrix}x = 1 \\ u = a \\ x := 0 \end{matrix} \begin{matrix}x = 1 \\ v = b \\ x := 0 \end{matrix} \begin{matrix}x = 1 \\ v < b \\ x := 0 \\ u := 0 \end{matrix}  F \begin{matrix}x = 1 \\ w = c \end{matrix} \begin{matrix}x = 1 \\ w < c \\ x := 0 \\ u := 0 \\ v := 0 \end{matrix}

It is to be shown that the location F can be reached – after all, as soon as F is reached, the data variable p contains the multiplication result we are interested in. (Backward or forward) reachability analysis in a sense simulates the behavior of the multiplier. I.e., since this system is fully deterministic, it takes a walk through the whole computation. Evidently, this is very time consuming even if we only attempted to compute 10 × 10 × 10. Now, compare this with the Elimination Approach. It takes two steps to eliminate the top left location, another 2a iterations for the bottom left location, some 2b iterations for the bottom right location, and finally, 2c iterations for the top right location. We then end up with a single location, namely F, for which the data variable p is initialized with the product a × b × c. Thus, even for big numbers a, b, and c the elimination approach is able to fulfill its task in a very short amount of time, whereas any kind of reachability analysis requires much more effort (essentially a + b + c versus a × b × c).

An Example where Reachability Fails The particularity about the following example is that it contains an “impossible” transition, i.e., one of the locations – the one at the bottom – is unreachable because the guard (y = 2) of the transition that may lead to this very location will never be enabled. In a sense, forward reachability analysis detects this, though rather indirectly, for it never tries to compute states involving this location. However, forward reachability nevertheless does not terminate, since the data variable y may become arbitrarily big and therefore the fixpoint computation finds new possible states in each iteration. At the first glance, backward reachability might have a better chance. Suppose we were about to prove that x ≤ y is an overall invariant of the system. If there were not the bottom location, backward reachability would have no problem to detect that the invariant indeed holds. But it this very location (or actually the transition that leads to itself) that prevents backward reachability from termination.

\begin{matrix}ẋ = 1 \\ ẏ = 1 \\ x ≤ 1 \end{matrix}  \begin{matrix}ẋ = 1 \\ ẏ = 1 \\ x ≤ 1 \end{matrix} \begin{matrix}ẋ = 1 \\ ẏ = 1 \\ x ≤ 1 \end{matrix}  \begin{matrix}ẋ = 1 \\ ẏ = 1 \\ x ≤ 1 \end{matrix} x := 0 y = 2 x := 0 x := 0; y := 0 x := 0 x := 0; y := y − 1 x := 0; y := 0

As for the Elimination Approach, recall that the real purpose of the Elimination Theorem is to provide us with a model for the given first-order theory. The Elimination Theorem is just one of the possible means we can imagine that may help us finding such a model. There are, however, cases for which we can (even by mere syntactic examinations) find out that a given first-order formula indeed has a (trivial) model. This is the case, for instance, if we reach a situation (maybe after having performed some eliminations) where every conjunct of the intermediate result contains a negative location predicate literal. In this case we can conclude that all locations that have not yet been eliminated are unreachable. This is in fact very common. The famous “Railroad-Gate-Controller” for example, has 22 (compound) locations. But only 7 of them are in fact reachable. Our implementation of the Elimination Approach first eliminates these seven reachable locations and then detects that all others are unreachable and terminates with success. The same happens for the example above: first the top three locations get eliminated and then the unreachability of the final (bottom) location is detected. Thus the system terminates with success.

4 Summary and Conclusion

We presented a hybrid systems verification methodology that is based on a successive location elimination procedure that allows us to simplify the system until it becomes trivial. This approach turns out to be particularly useful in case standard forward or backward reachability analysis methods would require to pass some of the locations several times (long lasting loops). There are even examples where a reachability analysis fails, whereas the Elimination Approach terminates successfully. However, there also are some non-trivial examples where forward reachability seems unbeatable, namely systems which contain quite a huge amount of locations, yet require merely a single pass in order to compute the set of reachable states. This observation leads to the conjecture that it might make sense to suitably combine the two methodologies: in case a non-trivial system (with many locations) contains long-lasting loops that prevent a reachability analysis from termination within some reasonable amount of time, it certainly makes sense to try and eliminate such loops with the help of the Elimination Approach and maybe to proceed with the reachability analysis after that.

References

[ACD90] R. Alur, C. Courcoubetis, and D. L. Dill. Model checking for real-time systems. In Proceedings of the 5th Annual Symposium on Logic in Computer Science, pages 414–425, 1990.

[ACH^{+}95] R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifaksi, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.

[ACHH93] R. Alur, C. Courcoubetis, T. A. Henzinger, and P.-H. Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 209–229. Springer Verlag, Lecture Notes in Computer Science, vol. 736, 1993.

[AD94] R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.

[AH92] R. Alur and T. A. Henzinger. Logics and models of real-time: A survey. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, pages 74–106. Springer Verlag, New York, LNCS 600, 1992.

[AHH96] Rajeev Alur, Thomas A. Henzinger, and Pei-Hsin Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 22(3):181–201, 1996.

[AHS96] R. Alur, T. A. Henzinger, and E. Sontag, editors. Hybrid Systems III. Lecture Notes in Computer Science, Springer Verlag, 1996.

[ANKS95] P. Antsaklis, A. Nerode, W. Kohn, and S. Sastry, editors. Hybrid Systems II. Lecture Notes in Computer Science, vol. 999, Springer Verlag, 1995.

[GNRR93] R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors. Hybrid Systems. Springer Verlag, Lecture Notes in Computer Science, vol. 736, 1993.

[Hen96] T. A. Henzinger. The theory of hybrid automata. In Proceedings of the 11th LICS, pages 278–292. IEEE Comp. Soc. Press, 1996.

[HNSY92] T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proceedings of the 7th Annual Symposium on Logic in Computer Science, pages 394–406. IEEE Computer Society Press, New York, 1992.

[Non99] Andreas Nonnengart. A deductive model checking approach for hybrid systems. Technical Report MPI-I-1999-2-006, Max-Planck-Institute for Computer Science, Saarbrücken, Germany, November 1999. Available via http://www.mpi-sb.mpg.de/.

[NOS99] Andreas Nonnengart, Hans Jürgen Ohlbach, and Andrzej Szałas. Elimination of predicate quantifiers. In Hans Jürgen Ohlbach and Uwe Reyle, editors, Logic, Language and Reasoning – Essays in Honour of Dov Gabbay. Kluwer, Dordrecht, Netherlands, 1999. ISBN: 0-7923-5687-X.

[NS95] Andreas Nonnengart and Andrzej Szałas. A fixpoint approach to secondorder quantifier elimination with applications to correspondence theory.

Technical Report MPI-I-95-2-007, Max-Planck-Institute for Computer Science, Saarbrücken, Germany, March 1995. Available via: http://www.mpisb.mpg.de/.

[NS99] Andreas Nonnengart and Andrzej Szalas. A fixpoint approach to secondorder quantifier elimination with applications to correspondence theory. in: [Orł99], 1999.

[Orł99] Ewa Orłowska, editor. Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa, volume 24 of Studies in Fuzziness and Soft Computing. Physica-Verlag, c/o Springer Verlag, 1999. ISBN: 3-7908-1164-5.