---
_id: '3864'
abstract:
- lang: eng
  text: 'Often one has a preference order among the different systems that satisfy
    a 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 tinder the given input assumption, synthesize a system
    that optimizes the measured value. For safety specifications and measures that
    are defined by mean-payoff automata, the optimal-synthesis problem amounts to
    finding a strategy in a Markov decision process (MDP) that is optimal for a long-run
    average reward objective, which can be done in polynomial time. For general omega-regular
    specifications, the solution rests on a new, polynomial-time algorithm for computing
    optimal strategies in MDPs with mean-payoff parity objectives. We present some
    experimental results showing optimal systems that were automatically generated
    in this way.'
acknowledgement: This research was supported by the European Union project COMBEST
  and the European Network of Excellence ArtistDesign.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- 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
- first_name: Rohit
  full_name: Singh, Rohit
  last_name: Singh
citation:
  ama: 'Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing
    systems in probabilistic environments. In: Vol 6174. Springer; 2010:380-395. doi:<a
    href="https://doi.org/10.1007/978-3-642-14295-6_34">10.1007/978-3-642-14295-6_34</a>'
  apa: 'Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Singh, R. (2010). Measuring
    and synthesizing systems in probabilistic environments (Vol. 6174, pp. 380–395).
    Presented at the CAV: Computer Aided Verification, Edinburgh, United Kingdom:
    Springer. <a href="https://doi.org/10.1007/978-3-642-14295-6_34">https://doi.org/10.1007/978-3-642-14295-6_34</a>'
  chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit
    Singh. “Measuring and Synthesizing Systems in Probabilistic Environments,” 6174:380–95.
    Springer, 2010. <a href="https://doi.org/10.1007/978-3-642-14295-6_34">https://doi.org/10.1007/978-3-642-14295-6_34</a>.
  ieee: 'K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “Measuring and
    synthesizing systems in probabilistic environments,” presented at the CAV: Computer
    Aided Verification, Edinburgh, United Kingdom, 2010, vol. 6174, pp. 380–395.'
  ista: 'Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2010. Measuring and synthesizing
    systems in probabilistic environments. CAV: Computer Aided Verification, LNCS,
    vol. 6174, 380–395.'
  mla: Chatterjee, Krishnendu, et al. <i>Measuring and Synthesizing Systems in Probabilistic
    Environments</i>. Vol. 6174, Springer, 2010, pp. 380–95, doi:<a href="https://doi.org/10.1007/978-3-642-14295-6_34">10.1007/978-3-642-14295-6_34</a>.
  short: K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, in:, Springer, 2010,
    pp. 380–395.
conference:
  end_date: 2010-07-19
  location: Edinburgh, United Kingdom
  name: 'CAV: Computer Aided Verification'
  start_date: 201-07-15
corr_author: '1'
date_created: 2018-12-11T12:05:35Z
date_published: 2010-07-09T00:00:00Z
date_updated: 2025-09-23T09:33:01Z
day: '09'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-14295-6_34
external_id:
  arxiv:
  - '1004.0739'
fulldoi: https://doi.org/10.1007/978-3-642-14295-6_34
intvolume: '      6174'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1004.0739
month: '07'
oa: 1
oa_version: Preprint
page: 380 - 395
publication_status: published
publisher: Springer
publist_id: '2313'
quality_controlled: '1'
related_material:
  record:
  - id: '1856'
    relation: later_version
    status: public
scopus_import: '1'
status: public
title: Measuring and synthesizing systems in probabilistic environments
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6174
year: '2010'
...