Probabilistic Least-violating Control Strategy Synthesis with Safety Rules

Sammanfattning: We consider the problem of automatic control strategy synthesis for discrete models of robotic systems, where the goal is to travel from some region to another while obeying a given set of safety rules in an environment with uncertain properties. This is a probabilistic extension of the work by Jana Tumová et al.  that is able to handle uncertainty by modifying the least-violating strategy synthesis algorithm. The first novel contribution is a way of modelling uncertain events in a map as a Markov decision process with a specific structure, using what we call "Ghost States". We then introduce a way of constructing a Product Automaton analogous to the original work, on which a modified probabilistic version of Dijkstra's algorithm can be run to synthesize the least-violating plan. The result is a synthesis algorithm that works similarly to the original, but can handle probabilistic uncertainty. It could be used in cases where e.g. uncertain weather conditions or the behaviour of external actors can be modelled as stochastic variables.