Cruise control


# of variables # of modes # of jumps
3 6 11
Type Continuous dynamics Guards & Invariants Resets
hybrid linear polynomial hyperplane & half-space constant



Model description

This cruise control benchmark was already used in [1] 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 [1].

  • v is the difference between the actual and the desired velocity.
  • t is the time.
  • x is an auxiliary variable.

The hybrid automaton of the benchmark:

Reachability settings

As an inital set we use:

  • v \in [15,40]
  • t \in [0, 2.5]
  •  x= 0

The initial location is q_1 and the time horizon T=100 sec.
The bad states are the set of states where v \leq -2.

Alternative initial settings:

  • v = 15 or v = 40
  • t=20
  •  x= 20



[1] J. Oehlerking. Decomposition of Stability Proofs for Hybrid Systems, Dissertation zur Erlangung eines Dr.-Ing., Universit├Ąt Oldenburg, 2011.