Publication detail

Model Repair Revamped - On the Automated Synthesis of Markov Chains -

ČEŠKA, M. HENSE, C. JANSEN, N. JUNGES, S. KATOEN, J.

Original Title

Model Repair Revamped - On the Automated Synthesis of Markov Chains -

Type

book chapter

Language

English

Original Abstract

This paper outlines two approaches-based on counterexample-guided abstraction refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS), respectively-to the automated synthesis of finite-state probabilistic models and programs. Our CEGAR approach iteratively partitions the design space starting from an abstraction of this space and refines this by a light-weight analysis of verification results. The CEGIS technique exploits critical subsystems as counterexamples to prune all programs behaving incorrectly on that input. We show the applicability of these synthesis techniques to sketching of probabilistic programs, controller synthesis of POMDPs, and software product lines.

Keywords

model repair, synthesis of Markov chains, counter-examples, abstraction refinement 

Authors

ČEŠKA, M.; HENSE, C.; JANSEN, N.; JUNGES, S.; KATOEN, J.

Released

23. 9. 2019

Publisher

Springer International Publishing

Location

Cham

ISBN

978-3-030-31513-9

Book

From Reactive Systems to Cyber-Physical Systems

Edition

Lecture Notes of Computer Science

Pages from

107

Pages to

125

Pages count

19

URL

BibTex

@inbook{BUT161474,
  author="ČEŠKA, M. and HENSE, C. and JANSEN, N. and JUNGES, S. and KATOEN, J.",
  title="Model Repair Revamped - On the Automated Synthesis of Markov Chains -",
  booktitle="From Reactive Systems to Cyber-Physical Systems",
  year="2019",
  publisher="Springer International Publishing",
  address="Cham",
  series="Lecture Notes of Computer Science",
  pages="107--125",
  doi="10.1007/978-3-030-31514-6\{_}7",
  isbn="978-3-030-31513-9",
  url="https://www.researchgate.net/publication/335984637_Model_Repair_Revamped_-_On_the_Automated_Synthesis_of_Markov_Chains_-"
}