207365
20181203023835.0
0004-5411
10.1145/2699430
doi
000350563000009
ISI
ARTICLE
Measuring and Synthesizing Systems in Probabilistic Environments
New York
2015
Assoc Computing Machinery
2015
34
Journal Articles
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.
Verification
Languages
Design
Synthesis
quantitative verification
Chatterjee, Krishnendu
Inst Sci & Technol Austria IST Austria, A-3400 Klosterneuburg, Austria
Henzinger, Thomas A.
Inst Sci & Technol Austria IST Austria, A-3400 Klosterneuburg, Austria
162366
243550
Jobstmann, Barbara
Ecole Polytech Fed Lausanne, CH-1015 Lausanne, Switzerland
Singh, Rohit
1
Journal Of The Acm
62
MTC
252230
U10969
oai:infoscience.tind.io:207365
article
EPFL-ARTICLE-207365
EPFL
PUBLISHED
REVIEWED
ARTICLE