Christian von Essen, Barbara Jobstmann, David Parker, and Rahul Varshneya
Semi-Symbolic Computation of Efficient Controllers in Probabilistic Environments (2012)
Semi-Symbolic Computation of Efficient Controllers in Probabilistic Environments (2012)
TR-2012-14.pdf
Keywords:
Abstract: We present a semi-symbolic algorithm for synthesizing efficient controllers in a stochastic environment, implemented as an add-on to the probabilistic model checker PRISM. The user specifies the environment and the controllable actions using a Markov Decision Process (MDP), modeled in the PRISM language. Controller efficiency is defined with respect to a user-specified assignment of costs and rewards to the controllable actions. An optimally efficient strategy minimizes the ratio between the encountered costs and rewards. At the core of the implementation is the first semi-symbolic algorithm based on a recently developed strategy improvement algorithm for MDPs with ratio objectives. We show the effectiveness of our implementation using a set of benchmarks.
