Synthesizing efficient systems in probabilistic environments

We present a formalism, algorithms and tools to synthesise reactive systems that behave efficiently, i.e., which achieve an optimal trade-off 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 resource-intensive. Quantitative synthesis aims to use additional information to guide the synthesizer towards a desired implementation. Trade-offs 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 trade-offs 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 trade-off 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 best-performing 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.