Measuring and Synthesizing Systems in Probabilistic Environments

Details Measuring and Synthesizing Systems in Probabilistic Environments Measuring and Synthesizing Systems in Probabilistic Environments

2010-04-05

arxiv.org/abs/1004.0739v2

Computer Science

Logic in Computer Science

29 pages

Scientific paper

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 given 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. Our algorithm generates optimal strategies consisting of two memoryless strategies and a counter. This 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 any \epsilon>0. We also show how to decide in polynomial time if we can construct an optimal finite-state system (i.e., a system without a counter) for a given specification. We have implemented our approach 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 experimental results showing optimal systems that were generated in this way.

Affiliated with

Also associated with

No associations

Rating

Measuring and Synthesizing Systems in Probabilistic Environments does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Measuring and Synthesizing Systems in Probabilistic Environments, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Measuring and Synthesizing Systems in Probabilistic Environments will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-56676