Generalized Property-Directed Reachability for Hybrid Systems

Abstract

Generalized property-directed reachability (GPDR) belongs to the family of the model-checking techniques called IC3/PDR. It has been successfully applied to software verification; for example, it is the core of Spacer, a state-of-the-art Horn-clause solver bundled with Z3. However, it has yet to be applied to hybrid systems, which involve a continuous evolution of values over time. As the first step towards GPDR-based model checking for hybrid systems, this paper formalizes $\textsc {HGPDR}$, an adaptation of GPDR to hybrid systems, and proves its soundness. We also implemented a semi-automated proof-of-concept verifier, which allows a user to provide hints to guide verification steps.

1 Introduction

A hybrid system is a dynamical system that exhibits both continuous-time dynamics (called a flow) and discrete-time dynamics (called a jump). This combination of flows and jumps is an essential feature of cyber-physical systems (CPS), a physical system governed by software. In the modern world where safety-critical CPS are prevalent, their correctness is an important issue.

Model checking [14, 19] is an approach to guaranteeing hybrid system safety. It tries to prove that a given hybrid system does not violate a specification by abstracting its behavior and by exhaustively checking that the abstracted model conforms to the specification.

In the area of software model checking, an algorithm called property-directed reachability (PDR), also known as IC3, is attracting interest [5, 7, 12]. IC3/PDR was initially proposed in the area of hardware verification; it was then transferred to software model checking by Cimatti et al. [10]. Its effectiveness for software model checking is now widely appreciated. For example, the SMT solver Z3 [29] comes with a Horn-clause solver Spacer [21] that uses PDR internally; Horn-clause solving is one of the cutting-edge techniques to verify functional programs [6, 8, 17] and programs with loops [6].

We propose a model checking method for hybrid automata [3] based on the idea of PDR; the application of PDR to hybrid automata is less investigated compared to its application to software systems. Concretely, we propose an adaptation of a variant of PDR called generalized property-directed reachability (GPDR) proposed by Hoder and Bjørner [20]. Unlike the original PDR, which is specialized to jump-only automata-based systems, GPDR is parametrized over a map over predicates on states (i.e., a forward predicate transformer); the detail of the underlying dynamic semantics of a verified system is encapsulated into the forward predicate transformer. This generality of GDPR enables the application of PDR to systems outside the scope of the original PDR by itself; for example, Hoder et al. [20] show how to apply GPDR to programs with recursive function calls.

An obvious challenge in an adaptation of GPDR to hybrid automata is how to deal with flow dynamics that do not exist in software systems. To this end, we extend the logic on which the forward predicate transformer is defined so that it can express flow dynamics specified by an ordinary differential equation (ODE). Our extension, inspired by the differential dynamic logic ($d\mathcal {L}$) proposed by Platzer [32], is to introduce continuous reachability predicates (CRP) of the form $\langle {\mathcal {D}} \mid {\varphi _I}\rangle \varphi$ where $\mathcal {D}$ is an ODE and $\varphi _I$ and $\varphi$ are predicates. This CRP is defined to hold under valuation $\sigma$ if there is a continuous transition from $\sigma$ to certain valuation $\sigma '$ that satisfies the following conditions: (1) the continuous transition is a solution of $\mathcal {D}$, (2) the valuation $\sigma '$ makes $\varphi$ true, and (3) $\varphi _I$ is true at every point on the continuous transition. With this extended logic, we define a forward predicate transformer that faithfully encodes the behavior of a hybrid automaton. We find that we can naturally extend GPDR to hybrid automata by our predicate transformer.

We formalize our adaptation of GPDR to hybrid automata, which we call $\textsc {HGPDR}$. In the formalization, we define a forward predicate transformer that precisely expresses the behavior of hybrid automata [3] using $d\mathcal {L}$. We prove the soundness of $\textsc {HGPDR}$. We also describe our proof-of-concept implementation of $\textsc {HGPDR}$ and show how it verifies a simple hybrid automaton with human intervention.

In order to make this paper self-contained, we detail GPDR for discrete-time systems before describing our adaptation to hybrid automata. After fixing the notations that we use in Sect. 2, we define a discrete-time transition system and hybrid automata in Sect. 3. Section 4 then reviews the GPDR procedure. Section 5 presents $\textsc {HGPDR}$, our adaptation of GPDR to hybrid automata, and states the soundness of the procedure. We describe a proof-of-concept implementation in Sect. 6. After discussing related work in Sect. 7, we conclude in Sect. 8.

For readability, several definitions and proofs are presented in the appendices.

2 Preliminary

We write $\mathbb {R}$ for the set of reals. We fix a finite set $V:= \left\{ {x _1,\dots ,x _N}\right\}$ of variables. We often use primed variables $x '$ and $x ''$. The prime notation also applies to a set of variables; for example, we write $V'$ for $\left\{ {x _1',\dots ,x _N'}\right\}$. We use metavariable $\varvec{x}$ for a finite sequence of variables. We write $\mathbf {Fml}$ for the set of quantifier-free first-order formulas over $V\cup V' \cup V''$; its elements are ranged over by $\varphi$. We call elements of the set $\varSigma {{\,\mathrm{{:=}}\,}}(V\cup V' \cup V'') \rightarrow \mathbb {R}$ a valuations; they are represented by metavariable $\sigma$. We use the prime notation for valuations. For example, if $\sigma \in V\rightarrow \mathbb {R}$, then we write $\sigma '$ for $\left\{ {x_1' \mapsto \sigma (x_1), \dots , x_N' \mapsto \sigma (x_N)}\right\}$. We write $\sigma [x \mapsto r]$ for the valuation obtained by updating the entry for $x$ in $\sigma$ with r. We write $\sigma \models \varphi$ if $\sigma$ is a model of $\varphi$; $\sigma \not \models \varphi$ if $\sigma \models \varphi$ does not hold; $\models \varphi$ if $\sigma \models \varphi$ for any $\sigma$; and $\not \models \varphi$ if there exists $\sigma$ such that $\sigma \not \models \varphi$. We sometimes identify a valuation $\sigma$ with a logical formula $\bigwedge _{x \in V}x = \sigma (x)$.

3 State-Transition Systems and Verification Problem

We review the original GPDR for discrete-time systems [20] in Sect. 4 before presenting our adaptation for hybrid systems in Sect. 5. This section defines the models used in these explanations (Sects. 3.1 and 3.2) and formally states the verification problem that we tackle (Sect. 3.3).

3.1 Discrete-Time State-Transition Systems (DTSTS)

We model a discrete-time program by a state-transition system.

Definition 3.1

A discrete-time state-transition system (DTSTS) is a tuple $\left\langle {Q,q_0,\varphi _0,\delta } \right\rangle$. We use metavariable $\mathcal {S}_D$ for DTSTS. $Q= \left\{ {q_0,q_1,q_2,\dots }\right\}$ is a set of locations. $q_0$ is the initial location. $\varphi _0$ is the formula that has to be satisfied by the initial valuation. $\delta \subseteq Q\times \mathbf {Fml}\times \mathbf {Fml}\times Q$ is the transition relation. We write $\left\langle {q,\sigma _1} \right\rangle \rightarrow _{\delta } \left\langle {q',\sigma _2} \right\rangle$ if $\left\langle {q, \varphi , \varphi _c, q'} \right\rangle \in \delta$ where $\sigma _1 \models \varphi$ and $\sigma _1 \cup \sigma _2' \models \varphi _c$; we call relation ${\rightarrow _{\delta }}$ the jump transition. A run of a DTSTS $\left\langle {Q,q_0,\varphi _0,\delta } \right\rangle$ is a finite sequence $\left\langle {q^0,\sigma _0} \right\rangle ,\left\langle {q^1,\sigma _1} \right\rangle ,\dots ,\left\langle {q^N,\sigma _N} \right\rangle$ where (1) $q^0 = q_0$, (2) $\sigma _0 \models \varphi _0$, and (3) $\left\langle {q^i,\sigma _i} \right\rangle \rightarrow _{\delta } \left\langle {q^{i+1},\sigma _{i+1}} \right\rangle$ for any $i \in [0,N-1]$.

$\left\langle {q,\varphi ,\varphi _c,q'} \right\rangle \in \delta$ intuitively means that, if the system is at the location q with valuation $\sigma _1$ and $\sigma _1 \models \varphi$, then the system can make a transition to the location $q'$ and change its valuation to $\sigma _2'$ such that $\sigma _1 \cup \sigma _2' \models \varphi _c$. We call $\varphi$ the guard of the transition. $\varphi _c$ is a predicate over $V\cup V'$ that defines the command of the transition; it defines how the value of the variables may change in this transition. The elements of $V$ represent the values before the transition whereas those of $V'$ represent the values after the transition.

Fig. 1.

An example of DTSTS

Example 3.2

Figure 1 is an example of a DTSTS that models a program to compute the value of $1 + \dots + x$; $Q:= \{q_0,q_1\}$ and $\varphi _0 := x \ge 0 \wedge sum = 0$. In the transition from $q_0$ to $q_0$, the guard is $x > 0$; the command is $sum' = sum + x \wedge x' = x - 1$. In the transition from $q_0$ to $q_1$, the guard is $x \le 0$; the command is $x' = x \wedge sum' = sum$ because this transition does not change the value of x and sum. Therefore, the transition relation $\delta = \big \{\left\langle {q_0, x > 0, sum' = sum + x \wedge x' = x - 1, q_0} \right\rangle , \langle q_0, x \le ~0, x' = x \wedge sum' = sum, q_1\rangle \big \}$. The finite sequence $\langle q_0,\{x \mapsto 3,sum \mapsto 0\}\rangle ,\left\langle {q_0, \{x \mapsto 2, sum \mapsto 3\}} \right\rangle , \left\langle {q_0, \{x \mapsto 1, sum \mapsto 5\}} \right\rangle ,\ \left\langle {q_0,\,\{x \mapsto 0, sum \mapsto 6\}} \right\rangle ,\langle q_1, \{x \mapsto 0, sum \mapsto 6\}\rangle$ is a run of the DTSTS Fig. 1.

3.2 Hybrid Automaton (HA)

We model a hybrid system by a hybrid automaton (HA) [3]. We define an HA as an extension of DTSTS as follows.

Definition 3.3

A hybrid automaton (HA) is a tuple $\left\langle {Q,q_0,\varphi _0,F, inv ,\delta } \right\rangle$. The components $Q$, $q_0$, $\varphi _0$, and $\delta$ are the same as Definition 3.1. We use metavariable $\mathcal {S}_H$ for HA. $F$ is a map from $Q$ to ODE on $V$ that specifies the flow dynamics at each location; $inv$ is a map from $Q$ to $\mathbf {Fml}$ that specifies the stay condition¹ at each state.

A state of a hybrid automaton is a tuple $\left\langle {q,\sigma } \right\rangle$. A run of $\left\langle {Q,q_0,\varphi _0,F, inv ,\delta } \right\rangle$ is a sequence of states $\left\langle {q_0,\sigma _0} \right\rangle \left\langle {q_1,\sigma _1} \right\rangle \dots \left\langle {q_n,\sigma _n} \right\rangle$ where $\sigma _0 \models \varphi _0$. The system is allowed to make a transition from $\left\langle {q_i,\sigma _i} \right\rangle$ to $\left\langle {q_{i+1},\sigma _{i+1}} \right\rangle$ if (1) $\sigma _i$ reaches a valuation $\sigma '$ along with the flow dynamics specified by $F(q_i)$, (2) $inv (q_i)$ holds at every point on the flow, and (3) $\left\langle {q_i,\sigma '} \right\rangle$ can jump to $\left\langle {q_{i+1},\sigma _{i+1}} \right\rangle$ under the transition relation $\delta$. In order to define the set of runs formally, we need to define the continuous-time dynamics that happens within each location.

Definition 3.4

Let $\mathcal {D}$ be an ordinary differential equation (ODE) on $V$ and let $x_1(t),\dots ,x_n(t)$ be a solution of $\mathcal {D}$ where t is the time. Let us write $\sigma ^{(t)}$ for the valuation $\left\{ {x_1 \mapsto x_1(t), \dots , x_n \mapsto x_n(t)}\right\}$. We write $\sigma {\rightarrow }_{{\mathcal {D}},{\varphi }} \sigma '$ if (1) $\sigma = \sigma ^{(0)}$ and (2) there exists $t' \ge t$ such that $\sigma ' = \sigma ^{(t')}$ and $\sigma ^{(t'')} \models \varphi$ for any $t'' \in (0,t']$. We call relation ${\rightarrow _{\mathcal {D},\varphi }}$ the flow transition.

Fig. 2.

An example of a hybrid automaton.

Intuitively, the relation $\sigma {\rightarrow }_{{\mathcal {D}},{\varphi }} \sigma '$ means that there is a trajectory from the state represented by $\sigma$ to that represented by $\sigma '$ such that (1) the trajectory is a solution of $\mathcal {D}$ and (2) $\varphi$ holds at any point on the trajectory. For example, let $\mathcal {D}$ be $\dot{x} = v, \dot{v} = 1$, where x and v are time-dependent variables; $\dot{x}$ and $\dot{v}$ are their time derivative. The solution of $\mathcal {D}$ is $v = t + v_0$ and $x = \frac{t^2}{2} + v_0 t + x_0$ where t is the elapsed time, $x_0$ is the initial value of x, and $v_0$ is the initial value of v. Therefore, $\left\{ {x \mapsto 0, v \mapsto 0}\right\} {\rightarrow }_{{\mathcal {D}},{ true }} \left\{ {x \mapsto \frac{1}{2}, v \mapsto 1}\right\}$ holds because $(x,v) = (\frac{1}{2}, 1)$ is the state at $t = 1$ on the above solution with $x_0 = 0$ and $v_0 = 0$. $\left\{ {x \mapsto 0, v \mapsto 0}\right\} {\rightarrow }_{{\mathcal {D}},{x \ge 0}} \left\{ {x \mapsto \frac{1}{2}, v \mapsto 1}\right\}$ also holds because the condition $x \ge 0$ continues to hold along with the trajectory from $(x,v) = (0,0)$ to $(\frac{1}{2},1)$. However, $\left\{ {x \mapsto 0, v \mapsto 0}\right\} {\rightarrow }_{{\mathcal {D}},{x \ge \frac{1}{4}}} \left\{ {x \mapsto \frac{1}{2}, v \mapsto 1}\right\}$ does not hold because the condition $x \ge \frac{1}{4}$ does not hold for the initial $\frac{1}{\sqrt{2}}$ seconds in this trajectory.

Using this relation, we can define a run of an HA as follows.

Definition 3.5

A finite sequence $\left\langle {q^0,\sigma _0} \right\rangle ,\left\langle {q^1,\sigma _1} \right\rangle ,\dots ,\left\langle {q^N,\sigma _N} \right\rangle$ is called a run of an HA $\left\langle {Q,q_0,\varphi _0,F, inv ,\delta } \right\rangle$ if (1) $q^0 = q_0$, (2) $\sigma _0 \models \varphi _0$, (3) for any i, if $0 \le i \le N-2$, there exists $\left\langle {q^i, \varphi _i, \varphi _c^i, q^{i+1}} \right\rangle \in \delta$ and $\sigma ^I$ such that $\sigma _i {\rightarrow }_{{F(q^i)},{ inv (q^i)}} \sigma ^I$ and $\sigma ^I \models \varphi _i$ and $\left\langle {q^i,\sigma ^I} \right\rangle \rightarrow _{\delta } \left\langle {q^{i+1},\sigma _{i+1}} \right\rangle$, and (4) $\sigma _{N-1} {\rightarrow }_{{F(q^{N-1})},{ inv (q^{N-1})}} \sigma _{N}$.

Remark 3.6

This definition is more complicated than that of runs of DTSTS because we need to treat the last transition from $\left\langle {q^{N-1},\sigma _{N-1}} \right\rangle$ to $\left\langle {q^{N},\sigma _{N}} \right\rangle$ differently than the other transitions. Each transition from $\left\langle {q^i,\sigma _i} \right\rangle$ to $\left\langle {q^{i+1},\sigma _{i+1}} \right\rangle$, if $0 \le i \le N-2$, is a flow transition followed by a jump transition; however, the last transition consists only of a flow transition.

Example 3.7

Figure 2 shows a hybrid automaton with $Q:= \left\{ {q_0,q_1}\right\}$ schematically. Each circle represents a location $q$; we write $F(q)$ for the ODE associated with each circle. Each edge between circles represents a transition; we present the guard of the transition on each edge. We omit the $\varphi _c$ part; it is assumed to be the do-nothing command represented by $\wedge _{x \in V}x' = x$.

Both locations are equipped with the same flow that is the anticlockwise circle around the point $(x,y)=(0,0)$ on the xy plane. The system can stay at $q_0$ as long as $y \ge 0$ and at $q_1$ as long as $y \le 0$. $y=0$ holds whenever a transition is invoked. Indeed, for example, $inv (q_0) = y \ge 0$ and the guard from $q_0$ to $q_1$ is $y \le 0$; therefore, when the transition is invoked, $inv (q_0) \wedge y \le 0$ holds, which is equivalent to $y=0$.

Starting from the valuation $\sigma _0 := \left\{ {x \mapsto 1, y \mapsto 0}\right\}$ at location $q_0$, the system reaches $\sigma _1 := \left\{ {x \mapsto -1, y \mapsto 0}\right\}$ by the flow $F(q_0)$ along which $inv (q_0) \equiv y \ge 0$ continues to hold; then the transition from $q_0$ to $q_1$ is invoked. After that, the system reaches $\sigma _2 := \left\{ {x \mapsto 0, y \mapsto -1}\right\}$ by $F(q_1)$. Therefore, $\left\langle {q_0,\sigma _0} \right\rangle \left\langle {q_1,\sigma _1} \right\rangle \left\langle {q_1,\sigma _2} \right\rangle$ is a run of this HA.

3.3 Safety Verification Problem

Definition 3.8

We say that $\sigma$ is reachable in DTSTS $\mathcal {S}_D$ (resp., HA $\mathcal {S}_H$) if there is a run of $\mathcal {S}_D$ (resp., $\mathcal {S}_H$) that reaches $\left\langle {q,\sigma } \right\rangle$ for some $q$. A safety verification problem (SVP) for a DTSTS $\left\langle {\mathcal {S}_D,\varphi } \right\rangle$ (resp., HA $\left\langle {\mathcal {S}_H,\varphi } \right\rangle$) is the problem to decide whether $\sigma ' \models \varphi$ holds for all the reachable valuation $\sigma '$ of the given $\mathcal {S}_D$ (resp., $\mathcal {S}_H$).

If an SVP is affirmatively solved, then the system is said to be safe; otherwise, the system is said to be unsafe. One of the major strategies for proving the safety of a system is discovering its inductive invariant.

Definition 3.9

• Let $\left\langle {\mathcal {S}_D,\varphi _P} \right\rangle$ be an SVP for DTSTS where $\mathcal {S}_D= \left\langle {Q,q_0,\varphi _0,\delta } \right\rangle$. Then, a function $R{{\,\mathrm{{:}}\,}}Q\rightarrow \mathbf {Fml}$ is called an inductive invariant if (1) $\models \varphi _0 \implies R(q_0)$; (2) if $\sigma \models R(q)$ and $\left\langle {q,\sigma } \right\rangle \rightarrow _{\delta } \left\langle {q',\sigma '} \right\rangle$, then $\sigma ' \models R(q')$; and (3) $\models R(q) \implies \varphi _P$ for any $q$.

• Let $\left\langle {\mathcal {S}_H,\varphi _P} \right\rangle$ be an SVP for HA where $\mathcal {S}_H= \left\langle {Q,q_0,\varphi _0,F, inv ,\delta } \right\rangle$. Then, a function $R{{\,\mathrm{{:}}\,}}Q\rightarrow \mathbf {Fml}$ is called an inductive invariant if (1) $\models \varphi _0 \implies R(q_0)$; (2) if $\sigma \models R(q)$ and $\left\langle {q,\sigma } \right\rangle {\rightarrow }_{{F(q)},{ inv (q)}} \left\langle {q'',\sigma ''} \right\rangle$ and $\left\langle {q'',\sigma ''} \right\rangle \rightarrow _{\delta } \left\langle {q',\sigma '} \right\rangle$, then $\sigma ' \models R(q')$; and (3) $\models R(q) \implies \varphi _P$ for any $q$.

Unsafety can be proved by discovering a counterexample.

Definition 3.10

Define $\mathcal {S}_D$, $\varphi _P$, and $\mathcal {S}_H$ as in Definition 3.9. A run $\left\langle {\sigma _0,q_0} \right\rangle \dots \left\langle {\sigma _N,q_N} \right\rangle$ of $\mathcal {S}_D$ (resp. $\mathcal {S}_H$) is called a counterexample to the SVP $\left\langle {\mathcal {S}_D,\varphi _P} \right\rangle$ (resp. $\left\langle {\mathcal {S}_H,\varphi _P} \right\rangle$) if $\sigma _N \models \lnot \varphi _P$.

GPDR is a procedure that tries to find an inductive invariant or a counterexample to a given SVP. SVP is in general undecidable. Therefore, the original GPDR approach [20] and our extension with hybrid systems presented in Sect. 5 do not terminate for every input.

4 GPDR for DTSTS

Before presenting our extension of GPDR with hybrid systems, we present the original GPDR procedure by Hoder and Bjørner [20] in this section. (The GPDR presented here, however, is slightly modified from the original one; see Remark 4.4.)

Given a safety verification problem $\left\langle {\mathcal {S}_D,\varphi _P} \right\rangle$ where $\mathcal {S}_D= \left\langle {Q,q_0,\varphi _0,\delta } \right\rangle$, GPDR tries to find (1) an inductive invariant to prove the safety of $\mathcal {S}_D$, or (2) a counterexample to refute the safety. To this end, GPDR (nondeterministically) manipulates a data structure called configurations. A configuration is either $\mathbf {Valid}$, ${{\,\mathrm{\mathbf {Model}}\,}}M$, or an expression of the form $M\> || \> R_0,\dots ,R_N; N$. We explain each component of the expression $M\> || \> R_0,\dots ,R_N; N$ in the following. ($\mathbf {Valid}$ and ${{\,\mathrm{\mathbf {Model}}\,}}M$ are explained later.)

• $R_0,\dots ,R_N$ is a finite sequence of maps from $Q$ to $\mathbf {Fml}$ (i.e., elements of $\mathbf {Fml}$). Each $R_i$ is called a frame. The frames are updated during an execution of GPDR so that $R_i(q_j)$ is an overapproximation of the states that are reachable within i steps from the initial state in $\mathcal {S}_D$ and whose location is $q_j$.

• N is the index of the last frame.

• $M$ is a finite sequence of the form $\left\langle {\sigma _i,q_i,i} \right\rangle ,\left\langle {\sigma _i,q_i,i+1} \right\rangle ,\dots ,\left\langle {\sigma _N,q_N,N} \right\rangle$. This sequence is a candidate partial counterexample that starts from the one that is i-step reachable from the initial state and that ends up with a state $\left\langle {\sigma _N,q_N} \right\rangle$ such that $\sigma _N \models \lnot \varphi _P$. Therefore, in order to prove the safety of $\mathcal {S}_D$, a GPDR procedure needs to prove that $\left\langle {q_i,\sigma _i} \right\rangle$ is unreachable within i steps from an initial state.

In order to formalize the above intuition, GPDR uses a forward predicate transformer determined by $\mathcal {S}_D$. In the following, we fix an SVP $\left\langle {\mathcal {S}_D,\varphi _P} \right\rangle$.

Definition 4.1

$\mathcal {F}(R)(q')$, where $\mathcal {F}$ is called the forward predicate transformer determined by $\mathcal {S}_D$, is the following formula:

$$ \begin{array}{l} (q' = q_0 \wedge \varphi _0) \vee \displaystyle \bigvee _{ (q,\varphi ,\varphi _c,q') \in \delta } \exists \varvec{x''}. \left( \begin{array}{ll} &{} [\varvec{x''}/\varvec{x}]R(q)\\ \wedge &{} [\varvec{x''}/\varvec{x}]\varphi \wedge [\varvec{x}/\varvec{x'},\varvec{x''}/\varvec{x}]\varphi _c\end{array} \right) , \end{array} $$

where $\varvec{x''}$ is the sequence $x _1'',\dots ,x _N''$.

Notice that $\mathcal {F}(\lambda q. false )$ is equivalent to $\varphi _0$. Intuitively, $\sigma ' \models \mathcal {F}(R)(q')$ holds if $\left\langle {q',\sigma '} \right\rangle$ is an initial state (i.e., $q'=q_0$ and $\sigma ' \models \varphi _0$) or $\left\langle {q',\sigma '} \right\rangle$ is reachable in 1-step transition from a state that satisfies R. The latter case is encoded by the second disjunct of the above definition: The valuation $\sigma '$ satisfies the second disjunct if there are $q,\varphi$, and $\varphi _c$ such that $(q,\varphi ,\varphi _c,q') \in \delta$ (i.e., $q'$ is 1-step after $q$ in $\delta$) and there is a valuation $\sigma$ such that $\sigma \models R(q) \wedge \varphi$ (i.e., $\sigma$ satisfies the precondition $R(q)$ and the guard $\varphi$) and $\sigma '$ is a result of executing command c under $\sigma$.

The following lemma guarantees that $\mathcal {F}$ soundly approximates the transition of an DTSTS.

Lemma 4.2

If $\sigma _1 \models R(q_1)$ and $\left\langle {q_1,\sigma _1} \right\rangle \rightarrow _{\delta } \left\langle {q_2,\sigma _2} \right\rangle$, then $\sigma _2 \models \mathcal {F}(R)(q_2)$.

Proof

Assume $\sigma _1 \models R(q_1)$ and $\left\langle {q_1,\sigma _1} \right\rangle \rightarrow _{\delta } \left\langle {q_2,\sigma _2} \right\rangle$. Then, by definition, $(q_1,\varphi ,\varphi ',q_2) \in \delta$ and $\sigma _1 \models \varphi$ and $\sigma _1 \cup \sigma _2' \models \varphi _c$ for some $\varphi$ and $\varphi _c$. $\sigma _1'' \cup \sigma _2 \models [\varvec{x''}/\varvec{x}]R(q_1)$ follows from $\sigma _1 \models R(q_1)$. $\sigma _1'' \cup \sigma _2 \models [\varvec{x''}/\varvec{x}]\varphi$ follows from $\sigma _1 \models \varphi$. $\sigma _1'' \cup \sigma _2 \models [\varvec{x}/\varvec{x'}, \varvec{x''}/\varvec{x}]\varphi _c$ follows from $\sigma _1 \cup \sigma _2' \models \varphi _c$. Therefore, $\sigma _1'' \cup \sigma _2 \models [\varvec{x''}/\varvec{x}]R(q_1) \wedge [\varvec{x''}/\varvec{x}]\varphi \wedge [\varvec{x}/\varvec{x'}, \varvec{x''}/\varvec{x}]\varphi _c$. Hence, we have $\sigma _2 \models \exists \varvec{x''}. [\varvec{x''}/\varvec{x}]R(q) \wedge [\varvec{x''}/\varvec{x}]\varphi \wedge [\varvec{x}/\varvec{x'},\varvec{x''}/\varvec{x}]\varphi _c$ as required.

By using the forward predicate transformer $\mathcal {F}$, we can formalize the intuition about configuration $M\> || \> R_0,\dots ,R_N; N$ explained so far as follows.

Definition 4.3

Let $\mathcal {S}_D$ be $\left\langle {Q,q_0,\varphi _0,\delta } \right\rangle$, $\mathcal {F}$ be the forward predicate transformer determined by $\mathcal {S}_D$, and $\varphi _P$ be the safety condition to be verified. A configuration C is said to be consistent if it is (1) of the form $\mathbf {Valid}$, (2) of the form ${{\,\mathrm{\mathbf {Model}}\,}}\left\langle {\sigma ,q_0,0} \right\rangle M$, or (3) of the form $M\> || \> R_0,\dots ,R_N; N$ that satisfies all of the following conditions:

• (Con-A) $R_0(q_0) = \varphi _0$ and $R_0(q_i) = false$ if $q_i \ne q_0$;

• (Con-B) $\models R_i(q) \implies R_{i+1}(q)$ for any $q$;

• (Con-C) $\models R_i(q) \implies \varphi _P$ for any $q$ and $i < N$;

• (Con-D) $\models \mathcal {F}(R_i)(q) \implies R_{i+1}(q)$ for any $i < N$ and $q$;

• (Con-E) if $\left\langle {\sigma ,q,N} \right\rangle \in M$, then $\sigma \models R_N(q) \wedge \lnot \varphi _P$²; and

• (Con-F) if $\left\langle {\sigma _1,q_1,i} \right\rangle , \left\langle {\sigma _2,q_2,i+1} \right\rangle \in M$ and $i < N$, then $\left\langle {q_1,\varphi ,\varphi _c,q_2} \right\rangle \in \delta$ and $\sigma _1,\sigma _2' \models R_i(q_1) \wedge \varphi \wedge \varphi _c$.

If C is consistent, we write $\mathbf {Con}(C)$.

Fig. 3.

The rules for the original PDR. Recall that $\lnot \sigma '$ in the rule $\textsc {Conflict}$ denotes the formula $\displaystyle \lnot \left( \bigwedge _{x \in V}x = \sigma '(x)\right)$.

The GPDR procedure rewrites a configuration following the (nondeterministic) rewriting rules in Fig. 3. We add a brief explanation below; for more detailed exposition, see [20]. Although the order of the applications of the rules in Fig. 3 is arbitrary, we fix one scenario of the rule applications in the following for explanation.

• 1. The procedure initializes $M$ to $\emptyset$, $R_0$ to $\mathcal {F}(\lambda q. false )$, and N to 0 ($\textsc {Initialize}$).

• 2. If there are a valuation $\sigma$ and a location $q$ such that $\sigma \models R_N(q) \wedge \lnot \varphi _P$ ($\textsc {Candidate}$), then the procedure adds $\left\langle {\sigma ,q,N} \right\rangle$ to $M$. The condition $\sigma \models R_N(q) \wedge \lnot \varphi _P$ guarantees that the state $\left\langle {q,\sigma } \right\rangle$ violates the safety condition $\varphi _P$; therefore, the candidate $\left\langle {\sigma ,q,N} \right\rangle$ needs to be refuted. If not, then the frame sequence is extended by setting N to $N+1$ and $R_{N+1}$ to $\lambda q. true$ ($\textsc {Unfold}$); this is allowed since $\forall q\in Q. \models R_N(q) \implies \varphi _P$ in this case.

• 3. The discovered $\left\langle {q,\sigma } \right\rangle$ is backpropagated by successive applications of $\textsc {Decide}$: In each application of $\textsc {Decide}$, for $\left\langle {q_2,\sigma _2,i+1} \right\rangle$ in $M$, the procedure tries to find $\sigma$ and $q$ such that $\left\langle {q_1,\varphi ,\varphi _c,q_2} \right\rangle \in \delta$ and $\sigma _1,\sigma _2' \models R_i(q_1) \wedge \varphi \wedge \varphi _c$ where $\sigma _2'$ is the valuation obtained by replacing the domain of $\sigma _2$ with their primed counterpart. These conditions in combination guarantee $\left\langle {q_1,\sigma _1} \right\rangle \rightarrow _{\delta } \left\langle {q_2,\sigma _2} \right\rangle$ and $\sigma _1 \models R_i(q_1)$.

  • (a) If this backpropagation reaches $R_0$ (the rule $\textsc {Model}$), then it reports the trace of the backpropagation returning ${{\,\mathrm{\mathbf {Model}}\,}}\ M$.

  • (b) If it does not reach $R_0$, in which case there exists i such that $\sigma ' \wedge \mathcal {F}(R_i)(q')$ is not satisfiable, then we pick a frame R such that $\models R(q') \implies \lnot \sigma '$ and $\models \mathcal {F}(R_i)(q) \implies R(q)$ for any $q$ (the rule $\textsc {Conflict}$). Intuitively, R is a frame that separates (1) the union of the initial states denoted by $\varphi _0$ and the states that are one-step reachable from a state denoted by $R_i(q')$ and (2) the state denoted by $\left\langle {q',\sigma '} \right\rangle$. In a GPDR term, R is a generalization of $\lnot \sigma '$. This formula is used to strengthen $R_j$ for $j \in \left\{ {1,\dots ,i+1}\right\}$.

• 4. The frame R obtained in the application of the rule $\textsc {Conflict}$ is propagated forward by applying the rule $\textsc {Induction}$. The condition $\forall q\in Q. \models \mathcal {F}(\lambda q.R_i(q) \wedge R(q))(q) \implies R(q)$ forces that $R$ holds in the one-step transition from a states that satisfies $R_i$. If this condition holds, then $R$ holds for $i+1$ steps (Theorem 4.5); therefore, we conjoin $R$ to $R_1(q), \dots , R_{i+1}(q)$. In order to maintain the consistency conditions (Con-E) and (Con-F), this rule clears $M$ to the empty set to keep its consistency to the updated frames.³

• 5. If $\forall q\in Q. \models R_i(q) \implies R_{i-1}(q)$ for some $i < N$, then the verification succeeds and $R_i$ is an inductive invariant ($\textsc {Valid}$). If such i does not exist, then we go back to Step 2.

Remark 4.4

One of the differences of the above GPDR from the original one [20] is that ours deals with the locations of a given DTSTS explicitly. In the original GPDR, information about locations are assumed to be encoded using a variable that represents the program counter. Although such extension was proposed for IC3 by Lange et al. [26], we are not aware of a variant of GPDR that treats locations explicitly.

Soundness. We fix one DTSTS $\left\langle {Q,q_0,\varphi _0,\delta } \right\rangle$ in this section. The correctness of the GPDR procedure relies on the following lemmas.

Lemma 4.5

$\mathbf {Con}$ is invariant to any rule application of Fig. 3.

Theorem 4.6

If the GPDR procedure is started from the rule $\textsc {Initialize}$ and leads to $\mathbf {Valid}$, then the system is safe. If the GPDR procedure is started from the rule $\textsc {Initialize}$ and leads to ${{\,\mathrm{\mathbf {Model}}\,}}\left\langle {\sigma _0,q_0,0} \right\rangle \dots \left\langle {\sigma _N,q_N,N} \right\rangle$, then the system is unsafe.

5 $\textsc {HGPDR}$

We now present our procedure $\textsc {HGPDR}$ that is an adaptation of the original GPDR to hybrid systems. An adaptation of GPDR to hybrid systems requires the following two challenges to be addressed.

• 1. The original definition of $\mathcal {F}$ (Definition 4.1) captures only a discrete-time transition. In our extension of GPDR, we need a forward predicate transformer that can mention a flow transition.

• 2. A run of an HA (Definition 3.5) differs from that of DTSTS in that its last transition consists only of flow dynamics; see Remark 3.6.

In order to address the first challenge, we extend the logic on which $\mathcal {F}$ is defined to be able to mention flow dynamics and define $\mathcal {F}$ on the extended logic (Sect. 5.1). To address the second challenge, we extend the configuration used by GPDR so that it carries an overapproximation of the states that are reachable from the last frame by a flow transition; the GPDR procedure is also extended to maintain this information correctly (Sect. 5.2).

5.1 Extension of Forward Predicate Transformer

In order to extend $\mathcal {F}$ to accommodate flow dynamics, we extend the logic on which $\mathcal {F}$ is defined with continuous reachability predicates (CRP) inspired by the differential dynamic logic ($d\mathcal {L}$) proposed by Platzer [33].

Definition 5.1

Let $\mathcal {D}$ be an ODE over $Y := \left\{ {y_1,\dots ,y_k}\right\} \subseteq V$. Let us write $\sigma$ for $\left\{ {y_1 \mapsto e_1, \dots , y_k \mapsto e_k}\right\}$ and $\sigma '$ for $\left\{ {y_1 \mapsto e_1', \dots , y_k \mapsto e_k'}\right\}$. We define a predicate $\langle {\mathcal {D}} \mid {\varphi }\rangle \varphi '$ by: $\sigma \models \langle {\mathcal {D}} \mid {\varphi }\rangle \varphi ' \mathrm {\quad iff. \quad } \exists \sigma '. \sigma {\rightarrow }_{{\mathcal {D}},{\varphi }} \sigma ' \wedge \sigma ' \models \varphi '$. We call a predicate of the form $\langle {\mathcal {D}} \mid {\varphi _I}\rangle \varphi$ a continuous reachability predicate (CRP).

Using the above predicate, we extend $\mathcal {F}$ as follows.

Definition 5.2

For an HA $\left\langle {Q,q_0,\varphi _0,F, inv ,\delta } \right\rangle$, the forward predicate transformer $\mathcal {F_H}(R)(q')$ is the following formula:

$$ \begin{array}{ll} (q'=q_0 \wedge \varphi _0) \vee \\ \displaystyle \bigvee _{(q,\varphi ,\varphi _c,q') \in \delta } \exists \varvec{x''}.\left( \begin{array}{ll} &{} [\varvec{x''}/\varvec{x}]R(q)\\ \wedge &{} \langle {[\varvec{x''}/\varvec{x}]F(q)} \mid {[\varvec{x''}/\varvec{x}] inv (q)}\rangle ([\varvec{x''}/\varvec{x}]\varphi \wedge [\varvec{x}/\varvec{x'},\varvec{x''}/\varvec{x}]\varphi _c) \end{array} \right) . \end{array} $$

In the above definition, $[\varvec{x''}/\varvec{x}]F(q)$ is the ODE obtained by renaming the variables $\varvec{x}$ that occur in ODE $F(q)$ with $\varvec{x''}$.

We also define predicate $\mathcal {F_C}(R)(q')$ as follows:

$$ \begin{array}{l} \exists \varvec{x''}. ([\varvec{x''}/\varvec{x}]R(q') \wedge \langle {[\varvec{x''}/\varvec{x}]F(q')} \mid {[\varvec{x''}/\varvec{x}] inv (q')}\rangle \varvec{x} = \varvec{x''}). \end{array} $$

Intuitively, $\sigma ' \models \mathcal {F_H}(\varphi )(q')$ holds if either (1) $\left\langle {q',\sigma '} \right\rangle$ is an initial state or (2) it is reachable from R by a flow transition followed a jump transition. Similarly, $\sigma ' \models \mathcal {F_C}(R)(q')$ holds if $\sigma '$ is reachable in a flow transition (not followed by a jump transition) from a state denoted by $R(q')$. This definition of $\mathcal {F_H}$ is an extension of Definition 4.1 in that it encodes the “flow-transition" part of the above intuition by the CRP. In the case of $\mathcal {F_C}$, the postcondition part of the CRP is $\varvec{x}=\varvec{x''}$ because we do not need a jump transition in this case.

Lemma 5.3

If $\sigma _1 \models R(q_1)$ and $\sigma _1 {\rightarrow }_{{F(q_1)},{ inv (q_1)}} \sigma ^I$ and $\left\langle {q_1,\sigma ^I} \right\rangle \rightarrow _{\delta } \left\langle {q_2,\sigma _2} \right\rangle$, then $\sigma _2 \models \mathcal {F_H}(R)(q_2)$.

Proof

Assume (1) $\sigma _1 \models R(q_1)$, (2) $\sigma _1 {\rightarrow }_{{F(q_1)},{ inv (q_1)}} \sigma ^I$, and (3) $\left\langle {q_1,\sigma ^I} \right\rangle \rightarrow _{\delta } \left\langle {q_2,\sigma _2} \right\rangle$. Then, by definition, (4) $(q_1,\varphi ,\varphi _c,q_2) \in \delta$ and (5) $\sigma ^I \models \varphi$ and (6) $\sigma ^I \cup \sigma _2' \models \varphi _c$ for some $\varphi$ and $\varphi _c$. We show $\exists \varvec{x''}.\left( [\varvec{x''}/\varvec{x}]R(q) \wedge \langle {[\varvec{x''}/\varvec{x}]F(q)} \mid {[\varvec{x''}/\varvec{x}] inv (q)}\rangle ([\varvec{x''}/\varvec{x}]\varphi \wedge [\varvec{x}/\varvec{x'},\varvec{x''}/\varvec{x}]\varphi _c) \right)$. (5) implies (7) $\sigma ^I \cup \sigma _2' \models \varphi$. (6) and (7) imply (8) ${\sigma ^I}'' \cup \sigma _2' \models [\varvec{x''}/\varvec{x}]\varphi \wedge [\varvec{x''}/\varvec{x}]\varphi _c$. (2) implies (9) $\sigma _1'' {\rightarrow }_{{[\varvec{x''}/\varvec{x}]F(q_1)},{[\varvec{x''}/\varvec{x}] inv (q_1)}} {\sigma ^I}''$. Therefore, from (8) and (9), we have (10) $\sigma _1'' \cup \sigma _2 \models \langle {[\varvec{x''}/\varvec{x}]F(q_1)} \mid {[\varvec{x''}/\varvec{x}] inv (q_1)}\rangle ([\varvec{x''}/\varvec{x}]\varphi \wedge [\varvec{x''}/\varvec{x}, \varvec{x}/\varvec{x'}]\varphi _c)$. (Note that the variables in $\varvec{x'}$ appear only in $\varphi _c$.) $\sigma _1'' \cup \sigma _2 \models [\varvec{x''}/\varvec{x}]R(q_1)$ follows from (1); therefore, we have $\sigma _1'' \cup \sigma _2 \models [\varvec{x''}/\varvec{x}]R(q_1) \wedge \langle {[\varvec{x''}/\varvec{x}]F(q_1)} \mid {[\varvec{x''}/\varvec{x}] inv (q_1)}\rangle ([\varvec{x''}/\varvec{x}]\varphi \wedge [\varvec{x''}/\varvec{x}, \varvec{x}/\varvec{x'}]\varphi _c)$. This implies $\exists \varvec{x''}.\left( [\varvec{x''}/\varvec{x}]R(q) \wedge \langle {[\varvec{x''}/\varvec{x}]F(q)} \mid {[\varvec{x''}/\varvec{x}] inv (q)}\rangle ([\varvec{x''}/\varvec{x}]\varphi \wedge [\varvec{x}/\varvec{x'},\varvec{x''}/\varvec{x}]\varphi _c) \right)$ as required.

Lemma 5.4

If $\sigma _1 \models R(q_1)$ and $\sigma _1 {\rightarrow }_{{F(q_1)},{ inv (q_1)}} \sigma _2$, then $\sigma _2 \models \mathcal {F_C}(R)(q_1)$.

Proof

Almost the same argument as the proof of Lemma 5.3.

Fig. 4.

The rules for $\textsc {HGPDR}$.

5.2 Extension of GPDR

We present our adaptation of GPDR for hybrid systems, which we call $\textsc {HGPDR}$. Recall that the original GPDR in Sect. 4 maintains a configuration of the form $M\> || \> R_0,\dots ,R_N; N$. $\textsc {HGPDR}$ uses a configuration of the form $M\> || \> R_0,\dots ,R_N; R_{ rem }; N$. In addition to the information in the original configurations, we add $R_{ rem }$ which we call remainder frame. $R_{ rem }$ overapproximates the states that are reachable from $R_N$ within one flow transition.

Figure 4 presents the rules for $\textsc {HGPDR}$. The rules from $\textsc {Initialize}$ to $\textsc {Conflict}$ are the same as Fig. 3 except that (1) $\textsc {Initialize}$ and $\textsc {Unfold}$ are adapted so that they set the remainder frame to $\lambda q. true$ and (2) $\textsc {Candidate}$ is dropped. We explain the newly added rules.

• $\textsc {PropagateCont}$ discovers a fact that holds in $R_{ rem }$. The side condition $\models R_N(q) \vee \mathcal {F_C}(R_N)(q) \implies R(q)$ for any $q$ guarantees that $R(q)$ is true at the remainder frame; hence R is conjoined to $R_{ rem }$.

• $\textsc {CandidateCont}$ replaces $\textsc {Candidate}$ in the original procedure. It tries to find a candidate from the frame $R_{ rem }$. The candidate $\left\langle {q,\sigma } \right\rangle$ found here is added to $M$ in the form $\left\langle {\sigma ,q, rem } \right\rangle$ to denote that $\left\langle {q,\sigma } \right\rangle$ is found at $R_{ rem }$.

• $\textsc {DecideCont}$ propagates a counterexample $\left\langle {\sigma ',q', rem } \right\rangle$ found at $R_{ rem }$ to the previous frame $R_N$. This rule computes the candidate to be added to $M$ by deciding $\sigma \cup \sigma ' \models R_N(q) \wedge \langle {F(q)} \mid { inv (q)}\rangle (\varvec{x}=\varvec{x'})$, which guarantees that $\sigma$ evolves to $\sigma '$ under the flow dynamics determined by $F(q)$ and $inv (q)$.

• $\textsc {Conflict}$ uses $\mathcal {F_H}$ instead of $\mathcal {F}$ in the original GPDR. As in the rule $\textsc {Conflict}$ in GPDR, the frame R in this rule is a generalization of $\lnot \sigma '$ which is not backward reachable to $R_i$.

• $\textsc {ConflictCont}$ is the counterpart of $\textsc {Conflict}$ for the frame $R_{ rem }$. This rule is the same as $\textsc {Conflict}$ except that it uses $\mathcal {F_C}$ instead of $\mathcal {F_H}$; hence, R separates $\sigma '$ from both the states denoted by $\varphi _0$ and the states that are reachable from $R_i$ in a flow transition (not followed by a jump transition).

5.3 Soundness

In order to prove the soundness of $\textsc {HGPDR}$, we adapt the definition of $\mathbf {Con}$ in Definition 4.3 for $\textsc {HGPDR}$.

Definition 5.5

Let $\mathcal {S}_H$ be $\left\langle {Q,q_0,\varphi _0,F, inv ,\delta } \right\rangle$, $\mathcal {F_H}$ and $\mathcal {F_C}$ be the forward predicate transformers determined by $\mathcal {S}_H$, and $\varphi _P$ be the safety condition to be verified. A configuration C is said to be consistent if it is $\mathbf {Valid}$, ${{\,\mathrm{\mathbf {Model}}\,}}\left\langle {\sigma ,q_0,0} \right\rangle M$, or $\mathbf {Con}_H(M\> || \> R_0,\dots ,R_N; R_{ rem }; N)$ that satisfies all of the following:

• (Con-A) $R_0(q_0) = \varphi _0$ and $R_0(q_i) = false$ if $q_i \ne q_0$;

• (Con-B-1) $\models R_i(q) \implies R_{i+1}(q)$ for any $q$ and $i < N$;

• (Con-B-2) $\models R_N(q) \implies R_{ rem }(q)$ for any $q$;

• (Con-C) $\models R_i(q) \implies \varphi _P$ if $i < N$;

• (Con-D-1) $\models \mathcal {F_H}(R_i)(q) \implies R_{i+1}(q)$ for any $i < N$ and $q$;

• (Con-D-2) $\models \mathcal {F_C}(R_N)(q) \implies R_{ rem }(q)$ for any $q$;

• (Con-E) if $\left\langle {\sigma ,q, rem } \right\rangle \in M$, then $\sigma \models R_ rem (q) \wedge \lnot \varphi _P$;

• (Con-F-1) if $\left\langle {\sigma _1,q_1,i} \right\rangle , \left\langle {\sigma _2,q_2,i+1} \right\rangle \in M$ and $i < N$, then $\left\langle {q_1,\varphi ,\varphi _c,q_2} \right\rangle \in \delta$ and $\sigma _1,\sigma _2' \models R_i(q_1) \wedge \varphi \wedge \varphi _c$; and

• (Con-F-2) if $\left\langle {\sigma _1,q_1,N} \right\rangle , \left\langle {\sigma _2,q_2, rem } \right\rangle \in M$, then $\left\langle {q_1,\varphi ,\varphi _c,q_2} \right\rangle \in \delta$ and $\sigma _1,\sigma _2' \models R_i(q_1) \wedge \varphi \wedge \varphi _c$.

The soundness proof follows the same strategy as that of the original GPDR.

Lemma 5.6

$\mathbf {Con}_H$ is invariant to any rule application of Fig. 4.

Theorem 5.7

If $\textsc {HGPDR}$ is started from the rule $\textsc {Initialize}$ and leads to $\textsc {Valid}$, then the system is safe. If $\textsc {HGPDR}$ is started from the rule $\textsc {Initialize}$ and leads to ${{\,\mathrm{\mathbf {Model}}\,}}\left\langle {\sigma _0,q_0,0} \right\rangle \dots \left\langle {\sigma _N,q_N,N} \right\rangle \left\langle {\sigma _ rem ,q_ rem , rem } \right\rangle$, then the system is unsafe.

5.4 Operational Presentation of $\textsc {HGPDR}$

The definition of $\textsc {HGPDR}$ in Fig. 4 is declarative and nondeterministic. For the sake of convenience of implementation, we derive an operational procedure from $\textsc {HGPDR}$; we call the operational version $\textsc {DetHybridPDR}$, whose definition is in Algorithm 1.

Discharging Verification Conditions. An implementation of $\textsc {HGPDR}$ needs to discharge verification conditions during verification. In addition to verification conditions expressed as a satisfiability problem of a first-order predicate, which can be discharged by a standard SMT solver, $\textsc {DetHybridPDR}$ needs to discharge conditions including a CRP predicate. Specifically, $\textsc {DetHybridPDR}$ needs to deal with the following three types of problems.

• Checking whether $\delta := \psi \wedge \langle {\mathcal {D}} \mid {\varphi _I}\rangle (\wedge _{x \in V}x = \sigma '(x))$ is satisfiable or not for given first-order predicates $\psi$ and $\varphi _I$, an ODE $\mathcal {D}$, and a valuation $\sigma '$. $\textsc {DetHybridPDR}$ needs to discharge this type of predicates when it decides which of $\textsc {DecideCont}$ and $\textsc {ConflictCont}$ should be applied if the top of $M$ is $\left\langle {\sigma ',q', rem } \right\rangle$. We use Algorithm 3 for discharging $\delta$. This algorithm searches for a valuation $\sigma _i$ that witnesses the satisfiability of $\delta$ by using a time-inverted simulation of $\mathcal {D}$ as follows. Concretely, this algorithm numerically simulates $\mathcal {D}^{-1}$, the time-inverted ODE of $\mathcal {D}$, starting from the point $\left\{ {\varvec{x} \mapsto \sigma '(x)}\right\}$. If it reaches a point $\sigma _i$ that satisfies $\psi$ and if all $\sigma _{i+1} \dots \sigma '$ in the obtained solution satisfy $\varphi _I$, then $\sigma _i$ witnesses the satisfiability of $\delta$. If such $\sigma _i$ does not exist but there is $\sigma _i$ such that $\sigma _i \not \models \varphi _I$, then $\psi$ is not backward reachable from $\sigma '$ and hence $\delta$ is unsatisfiable. In this case, Algorithm 3 needs to return a predicate that can be used as $\psi '$ in the rule $\textsc {ConflictCont}$ in Fig. 4. Currently, we assume that the user provides this predicate. We expect that we can help this step of discovering $\psi '$ by using techniques for analyzing continuous dynamics (e.g., automated synthesizer of barrier certificates [34] and Flow* [9] in combination with Craig interpolant synthesis procedures [2, 31]). If neither holds, then we give up the verification by aborting; this may happen if, for example, the value of T is too small.

• Checking whether $\delta ' := \psi \wedge \langle {F(q)} \mid { inv (q)}\rangle (\varphi \wedge \varphi _c\wedge \varvec{x}=\sigma '(\varvec{x}))$ is satisfiable or not. $\textsc {DetHybridPDR}$ needs to solve this problem in the choice between $\textsc {Decide}$ and $\textsc {Conflict}$. This query is different from the previous case in that the formula that appears after $\langle {F(q)} \mid { inv (q)}\rangle$ in $\delta '$ is $\varphi \wedge \varphi _c\wedge \varvec{x}=\sigma '(\varvec{x})$, not $\varvec{x}=\sigma '(\varvec{x})$; therefore, we cannot use numerical simulation to discharge $\delta '$. Although it is possible to adapt Algorithm 3 to maintain the sequence of predicates $\alpha _0\alpha _1\dots \alpha _{T-1}$ instead of valuations so that each $\alpha _i$ becomes the preimage of $\alpha _{i-1}$ by $\mathcal {D}$, the preimage computation at each step is prohibitively expensive. Instead, the current implementation restricts the input system so that there exists at most one $\sigma$ such that $\sigma \models \varphi \wedge \varphi _c\wedge \varvec{x}=\sigma '(\varvec{x})$ for any $\sigma '$; if this is met, then one can safely use Algorithm 3 for discharging $\delta '$. Concretely, we allow only $\varphi _c$ that corresponds to the command whose syntax is given by $c {:}{:}= \mathbf {skip}\mid x := r_1 x + r_2 \mid x := r_1 x - r_2$ where $\mathbf {skip}$ is a command that does nothing; $r_1$ and $r_2$ are real constants.

• Checking whether $\varphi _1 \wedge \langle {\mathcal {D}} \mid {\varphi _I}\rangle \lnot \varphi _2$ is unsatisfiable. $\textsc {DetHybridPDR}$ needs to discharge this type of queries when it applies $\textsc {Induction}$ or $\textsc {PropagateCont}$. This case is different from the previous case in that (1) $\textsc {DetHybridPDR}$ may answer $Otherwise$ without aborting the entire verification if unsatisfiability nor satisfiability is proved, and (2) $\textsc {DetHybridPDR}$ does not need to return a generalization if the given predicate is unsatisfiable. We use Algorithm 4 to discharge this type of queries. This algorithm first checks the satisfiability of $\varphi _1 \wedge \varphi _2$ in Step 1; if it is satisfiable, then so is the entire formula. Then, Step 5 tries to prove that the entire formula is unsatisfiable by proving (1) $\varphi _1$ is invariant with respect to the dynamics specified by $\mathcal {D}$ and $\varphi _I$ and (2) $\varphi _1 \wedge \varphi _2$ is unsatisfiable. In order to prove the former, the algorithm tries the following sufficient condition: For any positive $dt$ that is smaller than a positive real number r, $\models \varphi _i \wedge \varphi _I \implies [\varvec{x}+\varvec{f}(\varvec{x}) dt /\varvec{x}]\varphi _1$, where $\mathcal {D}\equiv \varvec{\dot{x}} = \varvec{f}(\varvec{x})$.⁴ Step 8 tries the same strategy but tries to prove that $\lnot \varphi _2$ is invariant. If both attempts fail, then the algorithm returns $Otherwise$.⁵ This algorithm could be further enhanced by incorporating automated invariant-synthesis procedures [15, 28, 35]; exploration of this possibilities is left as future work.

6 Proof-of-Concept Implementation

We implemented $\textsc {DetHybridPDR}$ as a semi-automated verifier. We note that the current implementation is intended to be a proof of concept; extensive experiments are left as future work. The snapshot of the source code as of writing can be found at https://github.com/ksuenaga/HybridPDR/tree/master/src.

The verifier takes a hybrid automaton $\mathcal {S}_H$ specified with $\textsc {SpaceEx}$ modeling language [27], the initial location $q_0$, the initial condition $\varphi _0$, and the safety condition $\varphi _P$ as input; then, it applies $\textsc {DetHybridPDR}$ to discover an inductive invariant or a counterexample. The frontend of the verifier is implemented with OCaml; in the backend, the verifier uses Z3 [29] and ODEPACK [1] to discharge verification conditions.

As we mentioned in Sect. 5.4, when a candidate counterexample $\left\langle {q',\sigma ',i+1} \right\rangle$ turns out to be backward unreachable to $R_i$, then our verifier asks for a generalization of $\sigma '$ to the user; concretely, for example in an application of the rule $\textsc {Conflict}$, the user is required to give $\psi$ such that $\models \psi \implies \lnot \sigma ' {{\,\mathrm{\mathbf {and}}\,}}\models (q,\varphi ,\varphi _c,q') \in \delta \wedge [\varvec{x_0}/\varvec{x}]R_i(q) \wedge \langle {[\varvec{x_0}/\varvec{x}]F(q)} \mid {[\varvec{x_0}/\varvec{x}] inv (q)}\rangle [\varvec{x_0}/\varvec{x}, \varvec{x_0}/\varvec{x}](\varphi \wedge \varphi _c) \implies \psi {{\,\mathrm{\mathbf {and}}\,}}\models R_0(q') \implies \psi$. Instead of throwing this query at the user in this form, the verifier asks the following question in order to make this process easier for the user for each $(q,\varphi ,\varphi _c,q') \in \delta$:

In applying $\textsc {ConflictCont}$, the verifier omits the fields Guard and Cmd.

We applied the verifier to the hybrid automaton in Fig. 2 with several initial conditions and the safety condition $\varphi _P := x \le 1$. We remark that the outputs from the verifier presented here are post-processed for readability. We explain how verification is conducted in each setting; we write $\mathcal {D}$ for the ODE $\dot{x} = -y, \dot{y} = x$.

• Initial condition $x = 0 \wedge y = 0$ at location $q_0$: The verifier finds the inductive invariant $\left\{ {q_0 \mapsto x = 0 \wedge y = 0, q_1 \mapsto x = 0 \wedge y = 0}\right\}$ after asking for proofs of unsatisfiability to the user 5 times.

• Initial condition $x \le \frac{1}{2}$ at location $q_0$: The verifier finds a counterexample $\left\{ {x \mapsto 0.490533, y \mapsto 1.93995}\right\}$, from which the system reaches $\left\{ {x \mapsto 2.00100, y \mapsto 0}\right\}$. The verifier asks 5 questions, one of which is the following:

  

  Notice that the stay condition is $y \ge 0$ and the guard is $y \le 0$; therefore the predicate $y = 0$ holds when a jump transition happens. Since the flow specified by $\mathcal {D}$ is an anticlockwise circle whose center is $\left\{ {x \mapsto 0, y \mapsto 0}\right\}$ with the stay condition $y \ge 0$, the states after the flow dynamics followed by a jump transition is $x \le 0.5 \wedge y = 0$, which indeed does not intersect with $x = 0.998516 \wedge y = -1.889365$. The verification proceeds by giving $y \ge 0$ as a generalization in this case.

• Initial condition $0 \le x \le \frac{1}{2} \wedge 0 \le y \le \frac{1}{2}$ at location $q_0$: The verifier finds an inductive invariant

  $$ R := \left\{ \begin{array}{l} q_0 \mapsto (y=0 \wedge 0 \le x \le 0.707107) \vee (0 \le x \le 0.5 \wedge 0 \le y \le 0.5),\\ q_1 \mapsto y=0 \wedge -0.707107 \le x \le 0 \end{array} \right\} $$

  after asking for 8 generalizations to the user. This is indeed an inductive invariant. Noting $0.707107 \approx \frac{1}{\sqrt{2}}$, we can confirm that (1) the states that are reachable by flow dynamics followed by a jump transition is the set denoted by $R(q_0)$; the same holds for the transition from $R(q_1)$; (2) it contains the initial condition $0 \le x \le 0.5 \wedge 0 \le y \le 0.5$ at location $q_0$; and (3) it does not intersect with the unsafe region $x > 1$. The following is one of the questions that are asked by the verifier:

  

  Instead of a precise overapproximation $(x^2 + y^2 = 0.5 \wedge y \le 0) \vee (0 \le x \le 0.5 \wedge 0 \le y \le 0.5)$ of the reachable states, we give $(-0.707107 \le y \le 0 \wedge -0.707107 \le x \le 0.707107) \vee (0 \le x \le 0.5 \wedge 0 \le y \le 0.5)$, which progresses the verification.

7 Related Work

Compared to its success in software verification [5, 10, 12, 20, 21], IC3/PDR for hybrid systems is less investigated. HyComp [11, 13] is a model checker that can use several techniques (e.g., IC3, bounded model checking, and k-induction) in its backend. Before verifying a hybrid system, HyComp discretizes its flows so that the verification can be conducted using existing SMT solvers that do not directly deal with continuous-time dynamics. Compared to HyComp, $\textsc {HGPDR}$ does not necessarily require prior discretization for verification. We are not aware of an IC3/PDR-based model checking algorithm for hybrid systems that does not require prior discretization.

Kindermann et al. [24, 25] propose an application of PDR for a timed system—a system that is equipped with clock variables; the flow dynamics of a clock variable c is limited to $\dot{c}=1$. A clock variable may be also reset to a constant in a jump transition. Kindermann et al. finitely abstract the state space of clock variables by using region abstraction [38]. The abstracted system is then verified using the standard PDR procedure. Later Isenberg et al. [22] propose a method that abstracts clock variables by using zone abstraction [4]. They do not deal with a hybrid system whose flow behavior at each location cannot be described by $\dot{c}=1$; the system in Fig. 2 is out of the scope of their work.

Our continuous-reachability predicates (CRP) are inspired by Platzer’s $d\mathcal {L}$ [33]. We may be able to use the theorem prover KeYmaera X for $d\mathcal {L}$ predicates [16] for our purpose of discharging CRP.

8 Conclusion

We proposed an adaptation of GPDR to hybrid systems. For this adaptation, we extended the logic on which the forward predicate transformer is defined with the continuous reachability predicates $\langle {\mathcal {D}} \mid {\varphi _I}\rangle \varphi$ inspired by the differential dynamic logic $d\mathcal {L}$. The extended forward predicate transformer can precisely express the behavior of hybrid systems. We formalized our procedure $\textsc {HGPDR}$ and proved its soundness. We also implemented it as a semi-automated procedure, which proves the safety of a simple hybrid system in Fig. 2.

On top of the current proof-of-concept implementation, we plan to implement a GPDR-based model checker for hybrid systems. We expect that we need to improve the heuristic used in the application of the rule $\textsc {Induction}$, where we currently check sufficient conditions of the verification condition. We are also looking at automating part of the work currently done by human in verification; this is essential when we apply our method to a system with complex continuous-time dynamics.