302
M. Cubuktepe et al.
For the distributions over parameter values, that is, over weather conditions,
we consider the following cases. First, we assume a uniform distribution over the
different weather conditions in each zone. Second, the probability for a weather
condition inducing a wind direction that pushes the UAV into the positive ydirection is five times more likely than others. Similarly, in the third case, it is
five times more likely to push the UAV into the negative x-direction. We depict
some example trajectories of the UAV for three different conditions in Fig. 2.
The trajectory given by the blue dashed line represents the expected trajectory
for the first case, taking a direct route to reach the target area. Similarly, the
trajectories given by the black dotted and solid green lines represent the expected
trajectories for the second and third cases. For the second case, we observe that
the UAV tries to avoid to get closer to the obstacles in x direction as the wind
may push the UAV to the obstacles. For the third case, the UAV avoids the
obstacle at the bottom and then reaches the target area.
We sample 1 000 parameters for each case and approximate the maximal
satisfaction probability with a confidence probability of at least 1 − α ν , with
α ν = 10
−6 . The highest satisfaction probability is given by the first weather
condition with 0.86, and the other conditions have a satisfaction probability of
0.78 and 0.75, showing that it may be harder to navigate around the obstacles
with non-uniform probability distributions. The average time to compute the
satisfaction probabilities is 1 341 seconds.
Finally, we introduce costs to a 2-dimensional example, where hitting an
obstacle causes (1) a cost of 100 and (2) the UAV to return to the initial position.
Specifically, we introduce cost parameters for transitions that steer the UAV
towards x or y-directions. We minimize the maximal possible expected cost
(under all parameter values) to reach the target location. The specification asserts
that the resulting expected cost should be less than 20.
We uniformly sample 1 000 parameter values for weather conditions and note
that the UAV policies favor on average transitioning to y-direction more compared
to the x-direction to minimize the cost while ensuring that the probability of
hitting an obstacle is minimized. The average expected cost of the induced MDPs
is 7.41 and the satisfaction probability is 0.71. The solving time for this example
is 2 274 seconds.
6 Conclusion
We presented a new sampling-based approach to uncertain Markov models. Theoretically, we showed how to effectively and efficiently approximate the probability
that any randomly drawn sample satisfies a temporal logic specification. Furthermore, we showed the computational tractability of our approaches by means of
well-known benchmarks and a new, dedicated case study.
In the future, we plan to exploit our approaches for more involved models
such as parametric extensions to continuous-time Markov chains [9] or Markov
automata [22]. Another line of future work will be a closer integration with a
parameter synthesis framework.
M. Cubuktepe et al.
For the distributions over parameter values, that is, over weather conditions,
we consider the following cases. First, we assume a uniform distribution over the
different weather conditions in each zone. Second, the probability for a weather
condition inducing a wind direction that pushes the UAV into the positive ydirection is five times more likely than others. Similarly, in the third case, it is
five times more likely to push the UAV into the negative x-direction. We depict
some example trajectories of the UAV for three different conditions in Fig. 2.
The trajectory given by the blue dashed line represents the expected trajectory
for the first case, taking a direct route to reach the target area. Similarly, the
trajectories given by the black dotted and solid green lines represent the expected
trajectories for the second and third cases. For the second case, we observe that
the UAV tries to avoid to get closer to the obstacles in x direction as the wind
may push the UAV to the obstacles. For the third case, the UAV avoids the
obstacle at the bottom and then reaches the target area.
We sample 1 000 parameters for each case and approximate the maximal
satisfaction probability with a confidence probability of at least 1 − α ν , with
α ν = 10
−6 . The highest satisfaction probability is given by the first weather
condition with 0.86, and the other conditions have a satisfaction probability of
0.78 and 0.75, showing that it may be harder to navigate around the obstacles
with non-uniform probability distributions. The average time to compute the
satisfaction probabilities is 1 341 seconds.
Finally, we introduce costs to a 2-dimensional example, where hitting an
obstacle causes (1) a cost of 100 and (2) the UAV to return to the initial position.
Specifically, we introduce cost parameters for transitions that steer the UAV
towards x or y-directions. We minimize the maximal possible expected cost
(under all parameter values) to reach the target location. The specification asserts
that the resulting expected cost should be less than 20.
We uniformly sample 1 000 parameter values for weather conditions and note
that the UAV policies favor on average transitioning to y-direction more compared
to the x-direction to minimize the cost while ensuring that the probability of
hitting an obstacle is minimized. The average expected cost of the induced MDPs
is 7.41 and the satisfaction probability is 0.71. The solving time for this example
is 2 274 seconds.
6 Conclusion
We presented a new sampling-based approach to uncertain Markov models. Theoretically, we showed how to effectively and efficiently approximate the probability
that any randomly drawn sample satisfies a temporal logic specification. Furthermore, we showed the computational tractability of our approaches by means of
well-known benchmarks and a new, dedicated case study.
In the future, we plan to exploit our approaches for more involved models
such as parametric extensions to continuous-time Markov chains [9] or Markov
automata [22]. Another line of future work will be a closer integration with a
parameter synthesis framework.