---
_id: '4569'
abstract:
- lang: eng
  text: "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.\r\nIn
    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."
acknowledgement: 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.
alternative_title:
- LNCS
arxiv: 1
author:
- first_name: Roderick
  full_name: Bloem, Roderick
  last_name: Bloem
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Barbara
  full_name: Jobstmann, Barbara
  last_name: Jobstmann
citation:
  ama: 'Bloem R, Chatterjee K, Henzinger TA, Jobstmann B. Better quality in synthesis
    through quantitative objectives. In: Vol 5643. Springer; 2009:140-156. doi:<a
    href="https://doi.org/10.1007/978-3-642-02658-4_14">10.1007/978-3-642-02658-4_14</a>'
  apa: 'Bloem, R., Chatterjee, K., Henzinger, T. A., &#38; Jobstmann, B. (2009). Better
    quality in synthesis through quantitative objectives (Vol. 5643, pp. 140–156).
    Presented at the CAV: Computer Aided Verification, Grenoble, France: Springer.
    <a href="https://doi.org/10.1007/978-3-642-02658-4_14">https://doi.org/10.1007/978-3-642-02658-4_14</a>'
  chicago: Bloem, Roderick, Krishnendu Chatterjee, Thomas A Henzinger, and Barbara
    Jobstmann. “Better Quality in Synthesis through Quantitative Objectives,” 5643:140–56.
    Springer, 2009. <a href="https://doi.org/10.1007/978-3-642-02658-4_14">https://doi.org/10.1007/978-3-642-02658-4_14</a>.
  ieee: 'R. Bloem, K. Chatterjee, T. A. Henzinger, and B. Jobstmann, “Better quality
    in synthesis through quantitative objectives,” presented at the CAV: Computer
    Aided Verification, Grenoble, France, 2009, vol. 5643, pp. 140–156.'
  ista: 'Bloem R, Chatterjee K, Henzinger TA, Jobstmann B. 2009. Better quality in
    synthesis through quantitative objectives. CAV: Computer Aided Verification, LNCS,
    vol. 5643, 140–156.'
  mla: Bloem, Roderick, et al. <i>Better Quality in Synthesis through Quantitative
    Objectives</i>. Vol. 5643, Springer, 2009, pp. 140–56, doi:<a href="https://doi.org/10.1007/978-3-642-02658-4_14">10.1007/978-3-642-02658-4_14</a>.
  short: R. Bloem, K. Chatterjee, T.A. Henzinger, B. Jobstmann, in:, Springer, 2009,
    pp. 140–156.
conference:
  end_date: 2009-07-02
  location: Grenoble, France
  name: 'CAV: Computer Aided Verification'
  start_date: 2009-06-26
date_created: 2018-12-11T12:09:31Z
date_published: 2009-06-19T00:00:00Z
date_updated: 2024-10-21T06:03:07Z
day: '19'
department:
- _id: KrCh
doi: 10.1007/978-3-642-02658-4_14
ec_funded: 1
external_id:
  arxiv:
  - '0904.2638'
intvolume: '      5643'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/0904.2638
month: '06'
oa: 1
oa_version: Preprint
page: 140 - 156
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '215543'
  name: COMponent-Based Embedded Systems design Techniques
publication_status: published
publisher: Springer
publist_id: '141'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Better quality in synthesis through quantitative objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5643
year: '2009'
...
---
_id: '517'
article_processing_charge: No
article_type: comment
author:
- first_name: Nicholas H
  full_name: Barton, Nicholas H
  id: 4880FE40-F248-11E8-B48F-1D18A9856A87
  last_name: Barton
  orcid: 0000-0002-8548-5240
citation:
  ama: 'Barton NH. Identity and coalescence in structured populations: A commentary
    on “Inbreeding coefficients and coalescence times” by Montgomery Slatkin. <i>Genetics
    Research</i>. 2008;89(5-6):475-477. doi:<a href="https://doi.org/10.1017/S0016672308009683">10.1017/S0016672308009683</a>'
  apa: 'Barton, N. H. (2008). Identity and coalescence in structured populations:
    A commentary on “Inbreeding coefficients and coalescence times” by Montgomery
    Slatkin. <i>Genetics Research</i>. Cambridge University Press. <a href="https://doi.org/10.1017/S0016672308009683">https://doi.org/10.1017/S0016672308009683</a>'
  chicago: 'Barton, Nicholas H. “Identity and Coalescence in Structured Populations:
    A Commentary on ‘Inbreeding Coefficients and Coalescence Times’ by Montgomery
    Slatkin.” <i>Genetics Research</i>. Cambridge University Press, 2008. <a href="https://doi.org/10.1017/S0016672308009683">https://doi.org/10.1017/S0016672308009683</a>.'
  ieee: 'N. H. Barton, “Identity and coalescence in structured populations: A commentary
    on ‘Inbreeding coefficients and coalescence times’ by Montgomery Slatkin,” <i>Genetics
    Research</i>, vol. 89, no. 5–6. Cambridge University Press, pp. 475–477, 2008.'
  ista: 'Barton NH. 2008. Identity and coalescence in structured populations: A commentary
    on ‘Inbreeding coefficients and coalescence times’ by Montgomery Slatkin. Genetics
    Research. 89(5–6), 475–477.'
  mla: 'Barton, Nicholas H. “Identity and Coalescence in Structured Populations: A
    Commentary on ‘Inbreeding Coefficients and Coalescence Times’ by Montgomery Slatkin.”
    <i>Genetics Research</i>, vol. 89, no. 5–6, Cambridge University Press, 2008,
    pp. 475–77, doi:<a href="https://doi.org/10.1017/S0016672308009683">10.1017/S0016672308009683</a>.'
  short: N.H. Barton, Genetics Research 89 (2008) 475–477.
date_created: 2018-12-11T11:46:55Z
date_published: 2008-10-29T00:00:00Z
date_updated: 2026-04-29T07:15:43Z
day: '29'
department:
- _id: NiBa
doi: 10.1017/S0016672308009683
external_id:
  isi:
  - '000207048900023'
intvolume: '        89'
isi: 1
issue: 5-6
language:
- iso: eng
month: '10'
oa_version: None
page: 475 - 477
publication: Genetics Research
publication_status: published
publisher: Cambridge University Press
publist_id: '7302'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Identity and coalescence in structured populations: A commentary on ''Inbreeding
  coefficients and coalescence times'' by Montgomery Slatkin'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 89
year: '2008'
...