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

f(v,s,v0)<max_acc

f(v,s,v0)<max_acc

and g(v,s,v0)>f(v,s,v0)

Max_acceleration and f(v,s,v0)>g(v,s,v0)

v'=max_acc
s'=v−v0

f(v,s,v0)>max_acc

f(v,s,v0)>max_acc

Motor_1 Motor_2

f(v,s,v0)>g(v,s,v0)

v'=f(v,s,v0) v'=g(v,s,v0)

s'=v−v0

g(v,s,v0)>f(v,s,v0)

s'=v−v0

Brake

v−v0>k1*v0

v−v0>k1*v0

v'=brake_dec

s'=v−v0

v−v0<k2*v0 and v−v0<k2*v0 and

f(v,s,v0)>g(v,s,v0) g(v,s,v0)>f(v,s,v0)

f(v,s,v0)=−1.679*(v−v0)
−0.0008*s−0.307*v0

g(v,s,v0)=−0.1995*(v−v0)

−0.000024*s−0.0015*v0

Fig. 14. Hybrid automaton of drive train subsystem

6.2 Synthesizing Lyapunov Functions

To compute a function V that fulfills the conditions in Definition 5, we use a
fixed parameterized function template: quadratic functions of the form V ( x )=
x T Px , P

n × n . In this representation, the parameters are isolated in the
symmetric matrix P . This means we have to compute matrix entries for P ,such
that conditions a) to d) are satisfied.
As detailed in [28,42], this can be done with the help of linear matrix in-
equalities [8], as long as the differential equations for all modes are ane. Linear
matrix inequalities are optimization problems with constraints given as definite-
ness constraints on matrices. They will be formally defined in the following.
Phrasing the problem to find an adequate P as a linear matrix inequality allows
the use of convex optimization software like CSDP [7] to identify suitable matrix
entries.

∈ R

n × n

is called positive semidefinite if x T Px

Definition 6. AmatrixP ∈ R ≥ 0

n . This is also denoted P

for all x ∈ R 0 . For given matrices M 1 ,..., M j ∈

R

n × n ,a linear matrix inequality is a problem of the form:
Find x 1 ,..., x j ∈ R such that x 1 M 1 + ... + x j M j 0 .

Define I as the n n identity matrix. The problem of finding a Lyapunov function

as in Definition 5 corresponds to the following linear matrix inequality [42]. Find
P ,μ i
m

×

such that: