Sciweavers

Share
CAV
2010
Springer

Measuring and Synthesizing Systems in Probabilistic Environments

9 years 4 months ago
Measuring and Synthesizing Systems in Probabilistic Environments
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...
Krishnendu Chatterjee, Thomas A. Henzinger, Barbar
Added 02 Sep 2010
Updated 02 Sep 2010
Type Conference
Year 2010
Where CAV
Authors Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh
Comments (0)
books