TY - EJOUR
DO - 10.1145/2699430
AB - The traditional synthesis question given a specification asks for the automatic construction of a system that satisfies the specification, whereas often there exists a preference order among the different systems that satisfy the given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the input assumption, synthesize a system that optimizes the measured value. For safety specifications and quantitative measures that are defined by mean-payoff automata, the optimal synthesis problem reduces to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be achieved in polynomial time. For general omega-regular specifications along with mean-payoff automata, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. Our algorithm constructs optimal strategies that consist of two memoryless strategies and a counter. The counter is in general not bounded. To obtain a finite-state system, we show how to construct an epsilon-optimal strategy with a bounded counter, for all epsilon > 0. Furthermore, we show how to decide in polynomial time if it is possible to construct an optimal finite-state system (i.e., a system without a counter) for a given specification. We have implemented our approach and the underlying algorithms in a tool that takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. We present some experimental results showing optimal systems that were automatically generated in this way.
T1 - Measuring and Synthesizing Systems in Probabilistic Environments
IS - 1
DA - 2015
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A.
AU - Jobstmann, Barbara
AU - Singh, Rohit
JF - Journal Of The Acm
SP - 9
VL - 62
EP - 9
PB - Assoc Computing Machinery
PP - New York
ID - 207365
KW - Verification
KW - Languages
KW - Design
KW - Synthesis
KW - quantitative verification
SN - 0004-5411
ER -