Information Technology Reference
In-Depth Information
n
n
,a
Lyapunov-like boundary
S
⊆
R
and a set of unsafe state vectors U
⊆
R
n
function
of the hybrid system is a function V
:
R
→
R
, such that:
-
for all runs of the system and all reachable states x
∈
R
n
:
V
•
(
x
):=
d
dx
dx
dt
≤
0
-
∃
k
∈
R
:(
x
∈
S
⇒
V
(
x
)
<
k
)
∧
(
x
∈
U
⇒
V
(
x
)
>
k
)
The function
V
has Lyapunov-like properties, as it will never increase through-
out the evolution of any trajectory due to the condition
V
•
(
x
)
0, which forces
the function's time derivative to be non-positive. Furthermore, there exists a
contour line, given by the points
x
with
V
(
x
)=
k
, such that the possible initial
states
S
lie on one side of this line, while the unsafe states
U
lie on the other (see
Fig. 11). Due to the Lyapunov-like property it is then impossible for a trajectory
beginning in the set of initial states to cross into the unsafe region, as this would
require an increase of
V
(
x
).
≤
V(x)>k
V(x)<k
U
S
Fig. 11. Criticality function contour line with initial set
S
and unsafe set
U
Since such a Lyapunov-like criticality function is a variant of a Lyapunov func-
tion, computational approaches for Lyapunov function synthesis can be adapted
for this case. For instance, linear matrix inequalities can be employed to
auto-
matically
compute a suitable quadratic
V
, and then the maximal
k
such that
x
V
(
x
)
>
k
. The computation procedure is very similar to the one that
will be described in detail in Section 6.
Such a Lyapunov-like boundary function is a special case of a criticality func-
tion as described in Subsection 4.1. The function
V
can be used as criticality
function
cr
and the contour line value
k
represents the maximal admissible crit-
icality value
c
safe
. Setting
cr
=
V
and
c
safe
∈
⇒
U
=
k
, the verification condition
(VC 1) is fulfilled since (
x
k
),
which is equivalent to (VC 1) by contraposition. For condition (VC 5),in
the case of
δ
=0,theset
S
assumes the role of
pre
(0
,Φ
start
). The condition
x
∈
U
⇒
V
(
x
)
>
k
) implies (
x
∈
U
⇒
V
(
x
)
≥
S
means that
x
is an admissible state vector for initiating the maneuver,
which is equivalent to the requirement that the variables at time of initiation
fulfill
pre
(0
,Φ
start
).If
δ>
0, a backward reachability computation is needed to
show that
V
(
x
)
<
k
for the entire negotiation period. Since verification condi-
tion (VC 5) requires an acceleration of zero during negotiation, this simplifies
∈
Search WWH ::
Custom Search