Overview
HARE is a framework for carrying out counterexample guided abstraction-refinement (CEGAR) for systems modelled as rectangular hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we consider the abstractions to be hybrid automata as well. This CEGAR scheme is semi-complete for the class of rectangular hybrid automata and complete for the subclass of initialized rectangular automata. Hare makes calls to the HyTech model checker to analyze the abstract models and validate the counterexamples.
Compared to the traditional finite state abstraction of hybrid automata, which involve computing unbounded time successor computation, construction hybrid automata abstractions only involves making local checks about flow equations. Further, when validating counterexamples in a hybrid CEGAR scheme, one is only required to compute time-bounded successors which is often computationally easier than computing time-unbounded successors. Our algorithm of computing abstractions involves the following operations: Collapsing the control states and transitions, dropping the continuous variables and scaling the variables. The refinement algorithm involves splitting control states/transitions, and/or adding variables that many have new dynamics and varying the scaling of each of the variables.
The advantage of considering hybrid automata based abstractions is that this procedure is complete/semi-complete for rectangular hybrid systems. In other words, if the hybrid automata is rectangular and is faulty (i.e. violates the safety specification), then our procedure will terminate by demonstrating the counter example for the safety specification. On the other hand, if the hybrid system is initialized rectangular, then our procedure will always terminate.
Software
HARE is a tool that is developed using C++, Lex and Yacc. Its background model checker is HyTech and it interacts with HyTech using system calls. HyTech can be downloaded from here, some of the libraries used in HyTech are no longer supported and hence we have the fix here for HyTech to work on latest versions of operating systems (Ubuntu 11.04 and 12.04). HARE can be downloaded here and the installation instructions are in the README file.
Experiments
HARE has been tested on various benchmark examples and the results are formulated below.
| Benchmark | Conc.Size (locs,var) |
Abst.Size (locs,var) |
Iter. | Val. (sec) | Abs. Ref. (sec) | HARE (sec) |
| BILL_2_A | (6,2) | (4,1) | 1 | 0.02 | 0.04 | 0.06 |
| BILL_3_A | (8,3) | (4,1) | 1 | 0.04 | 0.06 | 0.1 |
| NAV_10_A | (100,2) | (6,2) | 4 | 0.64 | 0.16 | 0.8 |
| NAV_15_A | (225,2) | (6,2) | 4 | 1.07 | 0.18 | 1.25 |
| NAV_10_B | (100,2) | (5,1) | 4 | 0.67 | 0.16 | 0.83 |
| NAV_15_B | (225,2) | (5,1) | 4 | 1.84 | 0.29 | 2.13 |
| NAV_8_C | (642,2) | (72,4) | 5 | 1.45 | 1.39 | 2.84 |
| NAV_10_C | (1002,2) | (72,4) | 5 | 2.41 | 1.51 | 3.92 |
| NAV_14_C | (1962,2) | (72,4) | 5 | 5.38 | 1.74 | 7.12 |
| SATS_3_S | (512,3) | (320,2) | 4 | 0.48 | 1.92 | 2.40 |
| SATS_4_S | (4096,4) | (1600,2) | 4 | 5.25 | 15.38 | 20.63 |
| SATS_5_S | (32786,5) | (8000,2) | 4 | 45.79 | 106.58 | 154.17 |
| SATS_3_C | (1000,4) | (500,2) | 5 | 2.04 | 3.82 | 5.86 |
| SATS_4_C | (10000,5) | (2500,2) | 5 | 22.25 | 41.37 | 63.98 |
| FISME_2 | (42,4) | (9,4) | 4 | 0.03 | 0.07 | 0.1 |
| FISME_3 | (43,5) | (36,4) | 4 | 0.44 | 1.34 | 1.78 |
| FISME_4 | (44,6) | (144,4) | 4 | 28.27 | 22.21 | 50.48 |
| ZENO_BOX | (7,2) | (5,1) | 1 | 0.04 | 0.04 | 0.08 |
People Involved
- Pavithra Prabhakar
- Parasara Sridhar Duggirala (email) (PhD student, CS)
- Sayan Mitra
- Mahesh Viswanathan
Publications
- Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra and Mahesh Viswanathan, Hybrid Automata-based CEGAR for Rectangular Hybrid Systems, VMCAI 2013. .pdf .source