Produced Output

After every refinement step, the procedure prints the number of boxes used for representing the abstraction of the hybrid system. For example,

***3 s: *** 5 ***

means that after the third refinement step, the abstraction consists of five boxes.

In recent versions, HSolver additionally prints the currently known upper bound on the volume of all starting points of error trajectories (initvol: ), and the currently known upper bound on the volume of all endpoints of error trajectories (unsafevol: ). Naturally, as soon as one of these values turns zero, the property has been proven, and HSolver terminates. Note however, that for computing these values, volumes of boxes are added in floating point arithmetic—without conservative rounding. Hence, these values should be considered as approximations.

Upon termination, HSolver outputs some statistics, and ”INPUT SAFE” if the verification succeeded, or ”SAFETY UNKNOWN” if it did not succeed. Our precise definition of safety of a hybrid system can be found in our publications [3].

If some boxes are left in the abstraction, they are printed, with some additional information. For example:

7: (1[ [ 4.875, 5.3125][ 1.5, 1.75] ]) L: 1 -> 21 13 <- 19 15 11

This means that the abstract state with id 7 represents the above box in mode 1. Numbers directly after the string “L: ” represent labels of this abstract state (currently label 0 means that the abstract state is labeled as being initial, and label 1 means that the abstract state is labeled as being unsafe). After the string -> follows a list of ids to which there is a transition from the current id, and after the string <- follows a list of ids from which there is a transition to the current one. These lists might contain some ids twice, denoting that there is both a flow and a jump transition.

In forward checking mode (command-line option -f) this list is an over-approximation of the set of state reachable from an initial state (i.e., the forward reach set), and in backward checking mode (command-line option -b) it is an over-approximation of the set of states that might lead to an unsafe state (i.e., the backward reach set).