Automating Verification of Cooperation, Control, and Design in Traffic Applications - Formal Methods and Hybrid Real-Time Systems - page 149

A Lyapunov function maps each state of the system onto a nonnegative real
number, such that the value of the function is decreasing at all times for all
possible trajectories , eventually converging to zero at the origin of the state
space. Condition a) enforces a global minimum of V at 0. Conditions b) and
c) imply that V is decreasing over time in every mode, whenever its invariant
is true, except at the equilibrium, where V m (0) = 0 for all applicable modes.
Condition d) is needed to enforce the stability property a) in Definition 4.

Theorem 2 ([9]). Consider a hybrid system as in Definition 5. The existence of
a common Lyapunov function for such a system implies local asymptotic stability
for all initial hybrid states that are covered by at least one invariant.

There are also refinements to the common Lyapunov function approach, using
piecewise continuous functions instead [9,28,42,16]. This allows the use of dif-
ferent functions for each mode. However, for the train controller application in
this paper, this extension was not necessary. Lyapunov functions can be found
automatically via numerical optimization [28,42,16]. We will demonstrate this
on the following example from the train control context.

6.1 The Drive Train Subsystem

The proof techniques outlined above will now be applied to the drive train part
of the train model from Section 2. The drive train is generally active in the
Far phase of the system when no full braking action is imminent. In this part
of the system, the actual velocity of the train should be kept in line with the
desired velocity, in the presence of outside disturbances. Furthermore, a change
of desired velocity should result in an adequate convergence of the actual velocity
towards this new value.
This is achieved by closed-loop control of the drive train via a PI-Controller,
i.e. a linear controller with proportional and integral part. This controller takes
the difference between current and desired velocity as an input and outputs a
current that is used to accelerate/decelerate the train.
In Equations 2-8, all constants and parameters have been instantiated with
sensible values, to represent a concrete drive train system. Braking force is as-
sumed constant, as is the environment force F e . All these equations have then
been collapsed into a set of two differential equations per mode, through elim-
ination of superfluous variables and exploitation of variable dependency. The
functions f an g are therefore the representation of Equations 2-8 for these fixed
values. The three relevant unknowns that remain in the drive train model given
in Fig. 14 are the desired speed v 0 , the actual speed v and the integral value
in Equation 2, denoted as s . Since Equation 2 describes dynamics modelled as
the minimum of two ane functions (Equation 1), there are two correspond-
ing modes, Motor 1 and Motor 2 , in the closed-loop hybrid system, each with
ane dynamics. The mode Max acceleration is used to model the cutoff at max-
imum acceleration in Equation 3. If the current speed is far beyond the desired
speed, we activate the brakes, which are assumed to produce constant negative
acceleration. This is represented by mode Brake .