[vEJPV16]
Christian von Essen, Barbara Jobstmann, David Parker and Rahul Varshneya.
Synthesizing Efficient Systems in Probabilistic Environments.
Acta Informatica, 53(4), pages 425–457, Springer.
June 2016.
[pdf]
[bib]
[Proposes efficient techniques for synthesising strategies in Markov decision processes against ratio objectives, implemented in an extension of PRISM.]

Notes:
The original publication is available at link.springer.com.

Abstract.
We present a formalism, algorithms and tools to synthesise reactive systems that behave efficiently, i.e., which achieve an optimal tradeoff between a given cost and reward model.
Synthesis aims to automatically generate a program from a specification. Most research in this area focuses on qualitative specifications, i.e., those that define a system as either correct or incorrect. The result can be a system that is correct, but still shows undesired behaviour, e.g., because it is too slow, inefficient or resourceintensive. Quantitative synthesis aims to use additional information to guide the synthesizer towards a desired implementation. Tradeoffs between costs and rewards provide a natural source of information in order to guarantee efficiency. The systems we want to synthesize are open, i.e., they react to input signals from their environment. So, we have to specify how to combine the tradeoffs the system decides to make for each input. There are several possible ways, e.g., worst or best case, or average case. In this paper we focus on the average case, i.e., we focus on the expected tradeoff achieved by a system. We define the problem of finding the system with the best expected behaviour according to a quantitative specification. This specification associates costs and rewards with each decision the system makes and defines a probabilistic environment that the system operates in. We analyze the feasibility of this task (i.e., prove that such systems exist and are computable) and present three algorithms to compute an optimal system for a given specification. We compare a prototypical implementation of these algorithms against each other and, based on the bestperforming algorithm, develop a novel symbolic implementation and integrate it into the probabilistic model checker PRISM. We report on experiments showing that our algorithm can analyze models with several million states. 