Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Journal articles
  4. Measuring and Synthesizing Systems in Probabilistic Environments
 
research article

Measuring and Synthesizing Systems in Probabilistic Environments

Chatterjee, Krishnendu
•
Henzinger, Thomas A.  
•
Jobstmann, Barbara
Show more
2015
Journal Of The Acm

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 epsilon-optimal strategy with a bounded counter, for all epsilon > 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.

  • Details
  • Metrics
Type
research article
DOI
10.1145/2699430
Web of Science ID

WOS:000350563000009

Author(s)
Chatterjee, Krishnendu
Henzinger, Thomas A.  
Jobstmann, Barbara
Singh, Rohit
Date Issued

2015

Publisher

Assoc Computing Machinery

Published in
Journal Of The Acm
Volume

62

Issue

1

Start page

9

Subjects

Verification

•

Languages

•

Design

•

Synthesis

•

quantitative verification

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
MTC  
Available on Infoscience
April 13, 2015
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/113248
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés