Better quality in synthesis through quantitative objectives Conference Paper


Author(s): Bloem, Roderick; Chatterjee, Krishnendu; Henzinger, Thomas A; Jobstmann, Barbara
Title: Better quality in synthesis through quantitative objectives
Title Series: LNCS
Affiliation IST Austria
Abstract: Most specification languages express only qualitative constraints. However, among two implementations that satisfy a given specification, one may be preferred to another. For example, if a specification asks that every request is followed by a response, one may prefer an implementation that generates responses quickly but does not generate unnecessary responses. We use quantitative properties to measure the “goodness” of an implementation. Using games with corresponding quantitative objectives, we can synthesize “optimal” implementations, which are preferred among the set of possible implementations that satisfy a given specification. In particular, we show how automata with lexicographic mean-payoff conditions can be used to express many interesting quantitative properties for reactive systems. In this framework, the synthesis of optimal implementations requires the solution of lexicographic mean-payoff games (for safety requirements), and the solution of games with both lexicographic mean-payoff and parity objectives (for liveness requirements). We present algorithms for solving both kinds of novel graph games.
Conference Title: CAV: Computer Aided Verification
Volume: 5643
Conference Dates: June 26 - July 2, 2009
Conference Location: Grenoble, France
Publisher: Springer  
Location: Berlin, Heidelberg
Date Published: 2009-06-19
Start Page: 140
End Page: 156
Sponsor: This research was supported by the Swiss National Science Foundation (Indo-Swiss Research Program and NCCR MICS) and the European Union projects COMBEST and COCONUT.
URL:
DOI: 10.1007/978-3-642-02658-4
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work