Author(s):

Chatterjee, Krishnendu; Henzinger, Thomas A; Jobstmann, Barbara; Singh, Rohit R

Article Title: 
Measuring and synthesizing systems in probabilistic environments

Affiliation 
IST Austria 
Abstract: 
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 omegaregular 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 meanpayoff automata, the optimal synthesis problem reduces to finding a strategy in a Markov decision process (MDP) that is optimal for a longrun average reward objective, which can be achieved in polynomial time. For general omegaregular specifications along with meanpayoff automata, the solution rests on a new, polynomialtime algorithm for computing optimal strategies in MDPs with meanpayoff 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 finitestate system, we show how to construct an εoptimal strategy with a bounded counter, for all ε > 0. Furthermore, we show how to decide in polynomial time if it is possible to construct an optimal finitestate 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.

Keywords: 
synthesis; quantitative verification

Journal Title:

Journal of the ACM

Volume: 
62

Issue 
1

ISSN:

00045411

Publisher:

ACM

Date Published:

20150201

Start Page: 
Article number: 9

URL: 

DOI: 
10.1145/2699430

Notes: 
This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) project S11402N23 (RiSE), FWF Grant No P23499N23, FWF NFN Grant No S11407N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award. We thank the anonymous reviewers for many valuable suggestions that helped us to significantly improve the presentation and the experimental result section.

Open access: 
yes (repository) 