We show how theorem proving and methods for handling real algebraic constraints can be combined for hybrid system verification. In particular, we highlight the interaction of deductive and algebraic reasoning that is used for handling the joint discrete and continuous behaviour of hybrid systems. We illustrate proof tasks that occur when verifying scenarios with cooperative traffic agents. From the experience with these examples, we analyse proof strategies for dealing with the practical challenges for integrated algebraic and deductive verification of hybrid systems, and we propose an iterative background closure strategy.
Safety-critical systems occurring in traffic scenarios [
Most verification tools for hybrid systems such as HyTech [
Because of intricacies of complex continuous dynamics, numerical issues
during computations, and general limits of numerical approximation [
We have introduced a family of logics for deductive verification of hybrid
systems [
While the theoretical background and technical details of our approach can
be found in [
In this paper, we study the modular combination in the dL calculus. Our observations are of more general interest, though, and we conjecture that similar results hold for other tableaux prover combinations of logics with interpreted function symbols that are handled using background decision procedures for computationally expensive theories including real arithmetic, approximations of natural arithmetic, or arrays.
Related Work. There are a selected number of logics dedicated to hybrid
systems [
A few other approaches [
Several other approaches combine deductive and arithmetic reasoning, e.g. [
In this section, we briefly recapitulate the differential logic dL that we have
introduced [
The principle of dynamic logic [
L
Hybrid programs generalise discrete programs to hybrid change. In addition to the operations of discrete while programs, they have continuous evolution along differential equations as a fundamental operation. For example, the evolution of a train with constant braking can be expressed with a system action for the differential equation z¨ = −b with second time-derivative z¨ of z. 2.1
Terms and Formulas. The formulas of dL are built over a finite set V of realvalued variables and a signature Σ containing the usual function and predicate symbols for real arithmetic, such as 0, 1, +, ·, =, ≤, <, ≥, >. Observe that there is no need to distinguish between discrete and continuous variables in d . L
The set Trm(V ) of terms is defined as in classical first-order logic
yielding polynomial expressions. The set Fml(V ) of formulas of dL is defined as in
first-order dynamic logic [
The effect of x := θ is a discrete jump in state space by an instantaneous
assignment. That of x˙ = θ is an ongoing continuous evolution controlled by the
differential equation x˙ = θ. Systems of differential equations, higher-order derivatives,
and evolution invariant regions [
The test action ?χ is used to define conditions. Its semantics is that of a
no-op if χ is true in the current state, and that of a failure divergence blocking
all further evolution, otherwise. The non-deterministic choice α ∪ β, sequential
composition α; β and non-deterministic repetition α∗ of hybrid programs are as
usual. They can be combined with ?χ to form other control structures, see [
The interpretations of dL consist of states assigning real values to state variables, which progress along a sequence of states. A potential behaviour of a hybrid system corresponds to a sequence of states that contain the observable values of system variables during its hybrid evolution. The semantics of a hybrid program α is captured by the state transitions that are possible by running α.
A state is a map ν : V → R; the set of all states is denoted by Sta(V ). Further, we use ν[x 7→ d] to denote the modification of a state ν that is identical to ν except for the interpretation of the symbol x, which is d ∈ R.
For discrete operations, the semantics, ρ(α), of hybrid program α as a state transition relation in dL is as customary in dynamic logic (Def. 3). For continuous evolutions, the transition relation holds for pairs of states that can be interconnected by a continuous system flow respecting the differential equation.
the valuation val(ν, ·) with respect to state ν is defined as usual for first-order
modal logic (e.g. [
In this section, we briefly review the dL sequent calculus that we introduced [
The dL calculus combines deduction and handling of real algebraic
constraints modularly. Simply speaking, the purely deductive part of the dL calculus
handles the discrete part, whereas the continuous part is tackled by real
algebraic constraint techniques. On this basis, hybrid system behaviour of interacting
discrete-continuous dynamics is handled by a modular calculus combination [
The dL sequent calculus is summarised in Fig. 1. A sequent is of the form Γ ` Δ, where Γ and Δ are finite sets of formulas. Its semantics is that of the formula Vφ∈Γ φ → Wψ∈Δ ψ. Sequents will be treated as an abbreviation. As usual in sequent calculus—although the direction of entailment is from premisses (above rule bar) to conclusion (below)—the order of reasoning is goal-directed : Rules are applied in tableau-style, that is, starting from the desired conclusion at the bottom (goal) to the premisses (sub-goals).
The rule schemata in Fig. 1 can be applied anywhere in the sequent, in
particular after adding an arbitrary context Γ, Δ, see [
For propositional logic, standard rules P1–P9 are listed in Fig. 1. The other
rules transform hybrid programs into simpler logical formulas, thereby relating
the meaning of programs and formulas. Rules D1–D7 are as in discrete dynamic
logic [
At this point, the full details of how F1–F4 use side deductions to lift
quantifier elimination to dynamic logic are not important (they can be found in [
In this section, we report on the applications in safety-critical system verification
that we verify in the dL calculus, see [
We assume that an MA has been granted up to track position m and the
train is located at position z, heading with initial speed v towards m. In this
situation, dL can verify safety properties of speed supervision of the form
ψ → [(corr ; drive)∗]z ≤ m
where corr ≡ (?m − z < s; a := −b) ∪ (?m − z ≥ s; a := . . . )
drive ≡ τ := 0; (z˙ = v, v˙ = a, τ˙ = 1; ?v ≥ 0 ∧ τ ≤ ε)
ψ ≡ v2 ≤ 2b(m − z) ∧ b > 0 ∧ > 0 .
(1)
(2)
It expresses that a train will always remain within its MA m, assuming a
constraint ψ for the parameters. In corr , the train corrects its acceleration or brakes
with force b (as a failsafe recovery manoeuvre [
The principle how the dL calculus in Fig. 1 combines deduction technology
with methods for handling real algebraic constraints complies with the general
background reasoning principles [
In this context, the propositional rules and D-rules (D1–D11) constitute the foreground rules in the main prover (left box of Fig. 2) and the arithmetic rules F1–F4 form the set of rules that invoke the background prover (right box).
The tableaux procedure [
F : selectFormula, i.e., which formula(s) to select for rule applications from the current branch in the current mode. while t a b l e a u x T has open branches do
B := s e l e c t B r a n c h (T) (∗ B−nondeterminism ∗) M := selectMode (B) (∗ M−nondeterminism ∗) F := s e l e c t F o r m u l a s (B,M) (∗ F−nondeterminism ∗) i f M = f o r e g r o u n d then
B2 := r e s u l t o f a p p l y i n g a D−r u l e or P−r u l e to F i n B r e p l a c e B by B2 i n T else send key F to background d e c i s i o n procedure QE receive r e s u l t R from QE apply a r u l e F1−F4 to T with QE−r e s u l t R end i f end while
A further, but minor, nondeterminism is whether to expand loops using D6 or to go for an induction by D11. The other dL rules do not produce any conflicts once a formula has been selected as they apply to formulas of distinct structures.
At this point, notice that, unlike the classical tableaux procedure [
Despite this, the influence of nondeterminism on the practical prover
performance is remarkable. Even though the theory of real arithmetic is decidable
by quantifier elimination [
In principle, exhaustive fair application of background rules by the nondeterminisms M and F remains complete for appropriate fragments of dL. In practice, however, the complexity of real arithmetic quickly makes this na¨ıve approach infeasible. In the remainder of this section, we discuss the consequences of the nondeterminisms and sketch guidelines to overcome the combination problems. 4.2
In classical uninterpreted tableaux, branch selection has no impact on completeness but can have impact on the proving duration as closing substitutions can sometimes be found much earlier on one branch than on the others. In the interpreted case of dL, branch selection is even less important. As dL has no closing substitutions, there is no direct interference among multiple branches. Branches with (explicitly or implicitly) universally quantified variables have to be closed independently, hence the branch order is not important. For instance, when x is an implicitly universally quantified variable, the branches in the following proof can be handled separately (branches are implicitly combined by conjunction and universal quantifiers distribute over conjunctions):
P5
QE(∀x . . . ) QE(∀x . . . ) F1Γ, b > 0 ` bx2 ≥ 0 F1Γ, b > 0 ` bx4 + x2 ≥ 0
Γ, b > 0 ` (bx2 ≥ 0 ∧ bx4 + x2 ≥ 0)
For existentially quantified variables, the situation is a bit more subtle as multiple branches interfere indirectly in the sense that a simultaneous solution needs to be found for all branches at once. In ∃v (v > 0 ∧ v < 0), for instance, the two branches resulting from the cases v > 0 and v < 0 cannot be handled separately as the existential quantifier claims the existence of a simultaneous solution for v > 0 and v < 0, not two different solutions. Thus, when v is an implicitly existentially quantified variable, the branches in the following proof need to synchronise before quantifier elimination is applied:
QE(∃v . . . ) b > 2 ` b(v − 1) > 0 b > 2 ` (v + 1)2 + b (v + 1) > 0 D8b > 2 ` [v := v − 1]bv > 0 D8b > 2 ` [v := v + 1]v2 + b v > 0 b > 2 ` ([v := v − 1]bv > 0 ∧ [v := v + 1]v2 + b v > 0) The order in which the intermediate steps at two branches are handled has no impact on the proof. Branches like these synchronise on an existential variable v in the sense that all occurrences of v need to be first-order for quantifier elimination to work. Consequently, the only fairness assumption for B is that whenever a formula of a branch is selected that is waiting for synchronisation with another branch to become first-order, then it propagates its rule application to the other branch. In the above case the left branch synchronises with the right branch on v. Hence, rule F3 can only be applied to b(v − 1) > 0 on the left branch after D8 has been applied on the right branch to yield first-order occurrences of v. 4.3
In background proving mode, it turns out that nondeterminism F is important for the practical performance. When a branch closes or, at least, can be simplified significantly by a quantifier elimination call, then the running time of a single decision procedure call seems to depend strongly on the number of irrelevant formulas that are selected in addition to the relevant ones by F .
Clearly, when Φ is a set of formulas that yields a tautology such that applying F1–F4 closes a branch, then selecting any superset Ψ ⊇ Φ of Φ from a branch yields the same answer in the end (a sequent forms a disjunction of its formulas hence it can be closed to true when any subset closes). However, the running time until this result will be found in the larger Ψ is strongly disturbed by the presence of complicated additional but irrelevant formulas. From our experience with Mathematica, decision procedures for full real arithmetic seem to be distracted considerably by such irrelevant additional information.
Yet, such additional information accumulates in tableaux procedures quite naturally, because the purpose of a proof branch in dL is to keep track of all that is known about a particular (symbolic) case of the system behaviour. Generally, not all of this knowledge finally turns out to be relevant for that case but only plays a role in other branches. Nevertheless, throwing away part of this knowledge light-heartedly would, of course, endanger completeness.
For instance, the safety statement (1) in Section 3 depends on a constraint
on the safety envelope s that regulates braking versus acceleration by the
condition m − z ≥ s in corr . A maximal acceleration of a is permitted in case
m − z ≥ s, when adaptively choosing s depending on the current speed v,
maximum braking force b, and maximum controller response time in accordance
with the following constraint (which can be discovered by the dL calculus [
A possible solution for this is to iteratively consider more formulas of the sequent and attempt decision procedure calls. There, only those additional formulas need to be considered that share variables with any of the other selected v2 s ≥ 2b + a b + 1 a ε2 + εv 2 . (3) formulas. Further, timeouts can be used to discontinue lengthy decision procedure calls and continue along other choices of the nondeterminisms in Fig. 3. For complicated cases with a prohibitive complexity, this heuristic process, which we followed manually, worked well on our examples. 4.4
In its own right, nondeterminism M has less impact on the prover performance than F . Every part of a branch could be responsible for closing it. In particular, the foreground closing rule P9 of the main prover can only close branches for comparatively trivial reasons like b > 0, > 0 ` > 0. Hence, mode selection has to give a chance to the background procedure every once in a while, following some fair selection strategy. From the observation that some decision procedure calls can run for hours without terminating, we can see, however, that M needs to be devised with considerable care.
As the reason for closing a branch can be hidden in any part of the sequent, some expensive decision procedure calls can be superfluous if the branch can be closed by continuing dL reasoning on the other parts. For instance, if F is some complicated algebraic constraint, decision procedure calls triggered by nondeterminism M can lead to nontermination within any feasible time for . . . , > 0, m − z ≥ s ` F, [drive] > 0, . . .
Instead, if M chooses foreground rules, then an analysis of [drive] > 0 by dL rules will quickly discover that the maximum reaction-time remains constant while driving. Then, this part of the induction step closes without the need to solve constraint F at all. For this reason, proof strategies that eagerly check for closing branches by background procedure calls are not successful in practice.
Unfortunately, converse strategies that strongly favour foreground dL rule applications in M, are not appropriate either. There, splitting rules like P5 and P7 can eagerly split the problems onto multiple branches without necessarily making them any easier to solve. If this happens, then slightly different but similar arithmetic problems of about the same complexity need to be solved on multiple branches rather than just one resulting in runtime blow-up.
The reason why this can happen is that there is a syntactic redundancy in the sequent encoding of formulas. For instance, the sets of sequents before and after the following rule application are equivalent:
P5 ψ ` v2 ≤ 2b(m − z)
ψ ` ψ ` v2 ≤ 2b(m − z) ∧ > 0 ψ ` (z ≥ 0 → v ≤ 0) > 0 ∧ (z ≥ 0 → v ≤ 0) Yet, closing the three sequents above the bar by quantifier elimination is not necessarily easier than the single sequent below (neither conversely). Even worse, if the sequents close by applying rules to ψ, then similar reasoning has to be repeated for three branches. This threefold reasoning may not be detected as identical when ψ is again split differently on the three resulting branches.
Further, the representational equivalence in sequents is purely syntactic, i.e., up to permutation, the representations share the same disjunctive normal form. In the uninterpreted case, this syntactic redundancy is exploited by the rules P1– P9 in order to transform sequents towards a canonical form with atomic formulas, where partial closing situations are more readily identifiable. In the presence of a background decision procedure, however, reduction to sequents with atomic formulas is no longer necessary as it will be undone when handing the formulas over to the background decision procedure.
Even worse, algebraic constraint handling techniques as in Mathematica can come up with a result that is only a restated version of the input when a selected (open) formula cannot be simplified or closed. For instance, the sequent z < m ` v2 ≤ 2b(m − z) “reduces” to ` b ≥ v2/(2m − 2z) ∨ m ≤ z without any progress. Such reformulation can easily lead to infinite proof loops when the outcome is split by P8 and again handled by the background procedures. 4.5
As a strategy to solve the previously addressed issues, we propose the priorities for rule applications in Fig. 5a (with rules at the top taking precedence over rules at the bottom). In this strategy, algebraic constraints are left intact as opposed to being split among multiple branches, because arithmetic rules have a higher priority than propositional rules on first-order constraints. Further, the result of the background procedure is only accepted when the number of variables has decreased to avoid proof loops. Arithmetic background rules have priority 1 or 6.
The effect of using priority 1 is that branches are checked eagerly for closing conditions or variable reductions. If reasoning about algebraic constraints does not yield any progress (no variables can be eliminated), then dL rules further analyse the system. For this choice, it is important to work with timeouts to prevent lengthy decision procedure calls from blocking dL proof progress. 1. arithmetic rules F1–F4 if variable eliminated 2. propositional rules P1–P4, P8–P9 on modalities 3. dynamic rules D1–D4, D7–D8 4. dynamic evolution rules D9–D10 5. splitting rules P5–P7 on modalities 6. arithmetic rules F1–F4 if variable eliminated 7. propositional rules P1–P9 on first-order formulas 16 16 8 2∗ 4 1 8 2 16 ∗4 5a: Proof strategy priorities.
5b: Iterative background closure.
This problem is reduced significantly when priority 6 is used for arithmetic rules instead. The effect of priority 6 is that formulas containing modalities are analysed as much as possible before arithmetic reasoning is applied to algebraic constraint formulas. Then, however, the prover can again take too much time analysing the effects of programs on branches which would already close due to simple arithmetic facts like in > 0, < 0 ` [α]φ.
A simple compromise is to use a combination of background rules with
priority 1 for quick linear arithmetic [
As a more sophisticated control strategy on top of the static priorities in Fig. 5a, we propose iterative background closure (IBC). There, the idea is to periodically apply arithmetic rules with a timeout T that increases by a factor of 2 after background procedure runs have timed out, see Fig. 5b. Thus, background rules interleave with other rule applications (triangles in Fig. 5b), and the timeout for the sub-goals increases as indicated until the background procedure successfully eliminated variables on a branch (marked by ∗). The effect is that the prover avoids splitting in the average case but is still able to split cases when combined handling turns out to be prohibitively expensive. 5
From the experience of using our dL calculus [
Future work includes validation of the IBC strategy by experiments in other case studies using a full implementation in our verification tool. Further, we will develop techniques that guide the selection of algebraic constraints by term weight and variable occurrence to discharge simple cases quickly. Acknowledgements. I thank the anonymous referees for their helpful comments.