dReach is a tool for safety verfication of hybrid systems.

It answers questions of the type: Can a hybrid system run into an unsafe region of its state space? This question can be encoded to SMT formulas, and answered by our SMT solver. dReach is able to handle general hyrbid systems with nonlinear differential equations and complex discrete mode-changes.

Since dReal implements a $$\delta$$-complete decision procedure, dReach performs “bounded $$\delta$$-complete reachability analysis”.

### Bounded $$\delta$$-Reachability – a brief explanation

Let $$H = \langle X, Q, \mathsf{flow}, \mathsf{jump}, \mathsf{inv},\mathsf{init}\rangle$$ be a hybrid system, where $$\mathsf{flow}$$, $$\mathsf{jump}$$, $$\mathsf{inv}$$, $$\mathsf{init}$$ are SMT formulas that dReal can handle (first-order formulas over the reals that allow polynomials, trigonometric functions, exponential functions, Lipschitz-continuous ODEs, etc.)

Now specify a numerical error bound $$\delta$$, and recall that for any formula $$\varphi$$ we have defined a notion of $$\delta$$-perturbation of $$\varphi$$ (see the dReal page), written as $$\varphi^{\delta}$$. We can then define the $$\delta$$-perturbation of $$H$$ as:

$$H^{\delta} = \langle X, Q, {\mathsf{flow}}^{\delta}, {\mathsf{jump}}^{\delta}, {\mathsf{inv}}^{\delta}, {\mathsf{init}}^{\delta}\rangle$$,

by simply relaxing the logic formulas in the representation of $$H$$. Choose $$n\in\mathbb{N}$$ to be a bound on the number of discrete mode changes and $$T\in \mathbb{R}^+$$ an upper bound on the time duration. Let $$\mathsf{unsafe}$$ encode a subset of $$X\times Q$$, the state space of $$H$$. The bounded $$\delta$$-reachability problem asks for one of the following answers:

• “safe”: $$H$$ cannot reach $$\mathsf{unsafe}$$ in $$n$$ steps within time $$T$$.
• ”$$\delta$$-unsafe”: $$H^{\delta}$$ can reach $${\mathsf{unsafe}}^{\delta}$$ in $$n$$ steps within time $$T$$. Note that these answers are not weaker than the precise ones. When “safe” is the answer, we know for certain that $$H$$ does not reach the unsafe region; when “$$\delta$$-unsafe” is the answer, there exists some $$\delta$$-bounded perturbation in the system that would render it unsafe. The error-bound $$\delta$$ can be chosen to be sufficiently small so that the “$$\delta$$-unsafe” answer discovers robustness problem in the system, which should consequently be regarded as “unsafe” indeed.

### Input Format

Consider the following standard bouncing-ball example with the following assumptions:

1. Air Friction acts on the ball, which is proportional to $$D \cdot v$$.

2. The ball is partially elastic. Whenever it hits the wall, it loses its velocity ($$v’ = K \times v$$).

We model this example as the following hybrid system model (bouncing_ball_with_drag.drh):

1. In the first part, we declare variables ($$x$$ and $$v$$), constants g = 9.8, drag = 0.45, elasticity = 0.9, and special variable time which is a bounded variable representing time in each mode.

2. Then, we describe each mode of this hybrid system. Mode 1 represents the status where a ball is falling down toward a floor, while mode 2 describes a ball bouncing back from a floor.

1. invt describes the invariant of each mode. In this example, we have simple invariants – velocity of the ball in mode 1 should be negative since it’s falling and the velocity of a ball should be positive in mode 2 because it’s bouncing back from the floor.

2. Dynamics of variables in each mode is described by flow, which is a set of differential equations. Here, we have simple dynamics: $$\dot{x} = v$$ and $$\dot{v} = -g \pm (D \times v)$$.

3. jump describes the conditions to switch mode, the destination mode, and changes of values. Note that when it jumps from mode 1 to mode 2, the velocity of the ball reduces due to the partial elasticity, $$v’ = K \times v$$.

3. In the end, we describe the initial condition, and the goal which we want to check its satisfiability. In this example, we start with $$x \ge 5$$ and $$v = 0$$ and check whether it is possible to reach the mode 1 while $$x >= 0.45$$.

### Bounded Model Checking

Our tool dReach takes in a hybrid system description (.drh) and unrolling bound $$k$$, and performs bounded model-checking.

\$ dReach -k 10 -l 10 bouncing_ball.drh --visualize --precision=0.1


The command-line argument -k 10 specifies the upper bound on the unrolling depth of bounded model checking, and the optional -l 10 specifies the lower bound. The options --visualize and --precision=0.1 will be passed to dReal.

• The first option --visualize enables dReal to store additional information to visualize the witness of $$\delta$$-sat result (bouncing_ball_with_drag_10_0.smt2.json).
• The second option --precision specifies the value of numerical perturbation $$\delta$$ we allow.

Running the above command, it first generates following .smt2 file (bouncing_ball_with_drag_10_0.smt2):

dReach uses dReal to check $$\delta$$-satisfiability of the generated smt2 file.

### Result

Using the generated bouncing_ball_with_drag_10_0.smt2.json file, we can visualize a witness of $$\delta$$-sat case as follows:

It shows that if the ball starts at a height between $$[8.720703125 , 8.73046875]$$ , it can reach the height 0.45 after bouncing five times. Note that we only specify the initial condition $$x \ge 5$$ and dReal found out the satisfying solution $$[8.720703125 , 8.73046875]$$ by solving the encoded constraints.