Better Quality in Synthesis through Quantitative Objectives

Details Better Quality in Synthesis through Quantitative Objectives Better Quality in Synthesis through Quantitative Objectives

2009-04-17

arxiv.org/abs/0904.2638v1

Computer Science

Logic in Computer Science

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Better Quality in Synthesis through Quantitative Objectives 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 Better Quality in Synthesis through Quantitative Objectives, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Better Quality in Synthesis through Quantitative Objectives will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-140911