|# of variables||# of modes||# of jumps|
|Type||Continuous dynamics||Guards & Invariants||Resets|
Note: The class of the benchmarks is determined by the input .
We study a non-linear resistor circuit which is shown in the figure below.
The circuit is composed of non-linear resistors and the same number of capacitors. Each non-linear resistor consists of a diode and a unit resistor (). For simplicity, we assume that all capacitors have unit capacitance . For each diode, the I-V characteristic is given by . The value of is in the original model, but we set it as to relieve the stiffness of the behavior. The current source in the figure is the input, and is the single output of the circuit. Therefore, the whole circuit system can be described by the following ODE.
Scalable continuous and hybrid benchmarks can be built based on the circuit according to the size and various types of the input. Here, we consider a discontinuous input which is defined by
The initial set under consideration is defined by for .
The following figure shows an overapproximation of the reachable set for the case over the time horizon computed by Flow*: