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. Synthesizing efficient systems in probabilistic environments
 
research article

Synthesizing efficient systems in probabilistic environments

Von Essen, Christian
•
Jobstmann, Barbara
•
Parker, David
Show more
2016
Acta Informatica

We present a formalism, algorithms and tools to synthesise reactive systems that behave efficiently, i.e., which achieve an optimal trade-off between a given cost and reward model. Synthesis aims to automatically generate a program from a specification. Most research in this area focuses on qualitative specifications, i.e., those that define a system as either correct or incorrect. The result can be a system that is correct, but still shows undesired behaviour, e.g., because it is too slow, inefficient or resource-intensive. Quantitative synthesis aims to use additional information to guide the synthesizer towards a desired implementation. Trade-offs between costs and rewards provide a natural source of information in order to guarantee efficiency. The systems we want to synthesize are open, i.e., they react to input signals from their environment. So, we have to specify how to combine the trade-offs the system decides to make for each input. There are several possible ways, e.g., worst or best case, or average case. In this paper we focus on the average case, i.e., we focus on the expected trade-off achieved by a system. We define the problem of finding the system with the best expected behaviour according to a quantitative specification. This specification associates costs and rewards with each decision the system makes and defines a probabilistic environment that the system operates in. We analyze the feasibility of this task (i.e., prove that such systems exist and are computable) and present three algorithms to compute an optimal system for a given specification. We compare a prototypical implementation of these algorithms against each other and, based on the best-performing algorithm, develop a novel symbolic implementation and integrate it into the probabilistic model checker PRISM. We report on experiments showing that our algorithm can analyze models with several million states.

  • Details
  • Metrics
Type
research article
DOI
10.1007/s00236-015-0237-y
Web of Science ID

WOS:000376978100005

Author(s)
Von Essen, Christian
Jobstmann, Barbara
Parker, David
Varshneya, Rahul
Date Issued

2016

Publisher

Springer

Published in
Acta Informatica
Volume

53

Issue

4

Start page

425

End page

457

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
IC  
Available on Infoscience
July 19, 2016
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/127643
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