Scenario-Based Verification of Uncertain MDPs
301
1
3
5
7
9
1
3
5
7
9
1
3
5
7
9
x
y
z
Fig. 2. An example of a 3D UAV benchmark with obstacles and a target area.
can efficiently compute a high confidence in the satisfaction probability. In
particular, for the same number of samples, the obtained confidence probabilities
are consistent for varying number of states and parameters of the underlying
models. Therefore, no dependence on the size of models is shown (see Remark 4).
5.2 UAV Motion Planning
In our second benchmark, we consider the previously mentioned UAV motion
planning example to model a realistic problem with a high number of random
parameters. We model the problem as a uMDP, where the parameters represent
how the weather conditions affect the movement of the UAV, and how the weather
may change. In particular, different wind conditions induce specific satisfaction
probabilities. We assume that the planning area is a certain valley where we
have historic weather data which provide distributions over parameter values.
The mission of the UAV is to transport a payload to a specific location and
return safely to its initial position. The problem is to compute the satisfaction
probability, that is, the probability that for any sampled MDP for this scenario
we are able to synthesize a UAV policy that satisfies the specification.
We model the problem as follows: States encode the position of the UAV, the
current weather situation, and the general wind direction in the valley. Parameters
describe how the weather affects the position of the UAV for different zones in
the valley, and how the weather/wind may change during the day. Fig. 2 shows
an example environment with zones to avoid (red) and a target zone (green).
We define four different weather conditions that each induce certain probability
distributions over the eight different wind directions. The parameters of the
model determine the probabilities of transitioning between different weather and
wind conditions at each time step. The specification is to reach the target zone
safely with a probability of at least 0.9. The number of states in our example is
266 880, and the number of parameters is 2 500.
301
1
3
5
7
9
1
3
5
7
9
1
3
5
7
9
x
y
z
Fig. 2. An example of a 3D UAV benchmark with obstacles and a target area.
can efficiently compute a high confidence in the satisfaction probability. In
particular, for the same number of samples, the obtained confidence probabilities
are consistent for varying number of states and parameters of the underlying
models. Therefore, no dependence on the size of models is shown (see Remark 4).
5.2 UAV Motion Planning
In our second benchmark, we consider the previously mentioned UAV motion
planning example to model a realistic problem with a high number of random
parameters. We model the problem as a uMDP, where the parameters represent
how the weather conditions affect the movement of the UAV, and how the weather
may change. In particular, different wind conditions induce specific satisfaction
probabilities. We assume that the planning area is a certain valley where we
have historic weather data which provide distributions over parameter values.
The mission of the UAV is to transport a payload to a specific location and
return safely to its initial position. The problem is to compute the satisfaction
probability, that is, the probability that for any sampled MDP for this scenario
we are able to synthesize a UAV policy that satisfies the specification.
We model the problem as follows: States encode the position of the UAV, the
current weather situation, and the general wind direction in the valley. Parameters
describe how the weather affects the position of the UAV for different zones in
the valley, and how the weather/wind may change during the day. Fig. 2 shows
an example environment with zones to avoid (red) and a target zone (green).
We define four different weather conditions that each induce certain probability
distributions over the eight different wind directions. The parameters of the
model determine the probabilities of transitioning between different weather and
wind conditions at each time step. The specification is to reach the target zone
safely with a probability of at least 0.9. The number of states in our example is
266 880, and the number of parameters is 2 500.