Information Technology Reference
In-Depth Information
have made the formula false (conversely for negative values). Thus, a formula
defines a function which assigns a numerical value to each simulation run.
Due to this nonstandard interpretation, numerical assessment functions can
be expressed in the logic.
As an example, we use formulas to describe (aspects of) criticality of
simulator runs. With an adequate subformula defining “TimeToCollision”,
computed from distance and relative speed of a leading car, if there is any,
the formula
(1)
expresses that this value never drops below 2.6 seconds (which would be
rather safe). Usually, we want more than one aspect evaluated. As an exam-
ple, also “TimeHeadway” enters criticality, and an acceptable lower bound on
this value in our scenario is
(
TimeToCollision
>
2
.
6
sec
)
seconds. To provide an adequate criticality
criterion in one formula, both observations are transformed into a
risk
val-
uation. The risk is inversely proportional to the respective time values, and
with adequate scaling factors we arrive at the following definitions.
0
.
3
RiskTTC
=
df
2
.
6
/
max(
TimeToCollision
,
0
.
01)
(2)
RiskTHw
=
df
0
.
3
/
max(
TimeHeadway
,
0
.
01)
(3)
These formulas yield
,
seconds, and higher val-
ues (with an upper bound of 100) for tighter situations. A criticality criterion
for our scenario is specified by
1
for the values of
2
.
6
,
resp.,
0
.
3
OnAccelLane
W(
¬
OnAccelLane
∧
RiskTTC
≤
1
∧
RiskThw
≤
1)
,
(4)
with
for “unless”. If this formula evaluates to a positive value for a run, the
driver has performed the manoeuvre with sucient safety margins in every
respect. A value of
W
indicates an already severe criticality with only 4.8
meters distance at a velocity difference of
−
2
20
km/h (
RiskTTC
)or
0
.
1
seconds
headway - only
meters at 80 km/h (
RiskTHw
).
The evaluation of formulas is automated by translating them into monitor
programs [4] observing to which degree the property is satisfied or violated.
These monitors enter the simulation environment as additional federates.
Upon termination of the simulation, each observer provides the numerical
evaluation of the property it stands for on the completed run. Thus, the
run can be classified as good or bad according to the resulting numbers.
Moreover, the observers are capable of computing lower and upper bounds
for the final value while the system is evolving. This allows us to identify and
stop irrelevant runs at an early stage of evolvment in order to save simulation
resources. The evaluation process is presented in more detail in the following
section.
2
.
2
4
Online Evaluation of LTL formulas
Our goal is to evaluate (linear) temporal-logic formulas during simulation, i.e.
over traces while they are evolving. The evaluation has to be performed in
