From Verification to Synthesis under Cost-Utility Constraints

Christel BaierChristel Baier, Clemens DubslaffClemens Dubslaff

DOI Link

Christel Baier, Clemens Dubslaff
From Verification to Synthesis under Cost-Utility Constraints
ACM SIGLOG News, 5(4):26--46, 2018

Details
Bibtex

KurzfassungAbstract
Various algorithms and tools for the formal verification of systems with respect to their quantitative behavior have been developed in the past decades. Many of these techniques inherently support the automated synthesis of strategies that guarantee the satisfaction of performance or reliability constraints by resolving controllable nondeterministic choices in an adequate way. More recently, such techniques have been further developed towards the analysis or strategy synthesis under multiple cost and utility constraints. This article deals with Markov decision processes (MDPs) for modeling systems and their environment and provides an overview of recent directions for different types of synthesis problems in MDPs that aim to achieve an acceptable cost-utility tradeoff.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{BD2018,
  author  = {Christel Baier and Clemens Dubslaff},
  title   = {From Verification to Synthesis under Cost-Utility Constraints},
  journal = {ACM {SIGLOG} News},
  volume  = {5},
  number  = {4},
  year    = {2018},
  pages   = {26--46},
  doi     = {10.1145/3292048.3292052}
}