|# of variables||# of modes||# of jumps|
|Type||Continuous dynamics||Guards & Invariants||Resets|
|hybrid||linear polynomial||hyperplane & half-space||constant|
This cruise control benchmark was already used in  for testing the decompositional stability verification approach. We suggest it here as a benchmark for testing verification tools. It has in particular a service and emergency brakes. The proposed hybrid model takes in addition the braking behavior of the engine under consideration. A detailed description can be found on pages 128, 129 and 130 of .
- is the difference between the actual and the desired velocity.
- is the time.
- is an auxiliary variable.
The hybrid automaton of the benchmark:
As an inital set we use:
The initial location is and the time horizon .
The bad states are the set of states where .
Alternative initial settings: