A hybrid system is a dynamical system that exhibits both continuous and discrete dynamic behavior – a system that can both flow (described by a differential equation) and jump (described by a state machine, automaton, or a difference equation).
In general, the state of a hybrid system is defined by the values of the continuous variables and a discrete mode.
The state changes either continuously, according to a flow condition, or discretely according to a control graph.
Continuous flow is permitted as long as so-called invariants hold, while discrete transitions can occur as soon as given jump conditions are satisfied.
The ball exhibits continuous dynamics between each bounce; however, as the ball impacts the ground, its velocity undergoes a discrete change modeled after an inelastic collision.
This is saying that when the height of the ball is zero (it has impacted the ground), its velocity is reversed and decreased by a factor of
The bouncing ball is an especially interesting hybrid system, as it exhibits Zeno behavior.
Zeno behavior has a strict mathematical definition, but can be described informally as the system making an infinite number of jumps in a finite amount of time.
It is noteworthy that the dynamical model is complete if and only if one adds the contact force between the ground and the ball.
Indeed, without forces, one cannot properly define the bouncing ball and the model is, from a mechanical point of view, meaningless.
The simplest contact model that represents the interactions between the ball and the ground, is the complementarity relation between the force and the distance (the gap) between the ball and the ground.
Such a contact model does not incorporate magnetic forces, nor gluing effects.
When the complementarity relations are in, one can continue to integrate the system after the impacts have accumulated and vanished: the equilibrium of the system is well-defined as the static equilibrium of the ball on the ground, under the action of gravity compensated by the contact force
One also notices from basic convex analysis that the complementarity relation can equivalently be rewritten as the inclusion into a normal cone, so that the bouncing ball dynamics is a differential inclusion into a normal cone to a convex set.
See Chapters 1, 2 and 3 in Acary-Brogliato's book cited below (Springer LNACM 35, 2008).
There are approaches to automatically proving properties of hybrid systems (e.g., some of the tools mentioned below).
Common techniques for proving safety of hybrid systems are computation of reachable sets, abstraction refinement, and barrier certificates.
A possible theoretical characterization of this is algorithms that succeed with hybrid systems verification in all robust cases[3] implying that many problems for hybrid systems, while undecidable, are at least quasi-decidable.
[4] Two basic hybrid system modeling approaches can be classified, an implicit and an explicit one.
As a unified simulation approach for hybrid system analysis, there is a method based on DEVS formalism in which integrators for differential equations are quantized into atomic DEVS models.
Detailed of this approach can be found in references [Kofman2004] [CF2006] [Nutaro2010] and the software tool PowerDEVS.