From verification to synthesis under cost-utility constraints

Research output: Contribution to journalResearch articleContributedpeer-review


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.


Original languageEnglish
Pages (from-to)26–46
JournalACM SIGLOG News
Issue number4
Publication statusPublished - 12 Nov 2018