Measuring and synthesizing systems in probabilistic environments Journal Article


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 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 ε-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 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.
Keywords: synthesis; quantitative verification
Journal Title: Journal of the ACM
Volume: 62
Issue 1
ISSN: 0004-5411
Publisher: ACM  
Date Published: 2015-02-01
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 S11402-N23 (RiSE), FWF Grant No P23499-N23, FWF NFN Grant No S11407-N23 (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)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work