@inproceedings{CHJ+10b,
title = {Measuring and Synthesizing Systems in Probabilistic Environments },
author = {Chatterjee, Krishnendu and Henzinger, Thomas A. and Jobstmann, Barbara and Singh, Rohit},
year = {2010},
booktitle = {Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010},
pages = {380-395},
team = {DCS},
abstract = {Often one has a preference order among the different systems that
satisfy a 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 given input assumption,
synthesize a system that optimizes the measured value.
For safety specifications and measures that are defined by mean-payoff
automata, the optimal-synthesis problem amounts to finding a strategy
in a Markov decision process (MDP) that is optimal for a long-run
average reward objective, which can be done in polynomial time. For
general omega-regular specifications, the solution rests on a new,
polynomial-time algorithm for computing optimal strategies in MDPs
with mean-payoff parity objectives. We present some experimental
results showing optimal systems that were automatically generated in
this way.
},
}
