Detail publikace

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

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

Originální název

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

Typ

kapitola v knize

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

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

Vydáno

23. 9. 2019

Nakladatel

Springer International Publishing

Místo

Cham

ISBN

978-3-030-31513-9

Kniha

From Reactive Systems to Cyber-Physical Systems

Edice

Lecture Notes of Computer Science

Strany od

107

Strany do

125

Strany počet

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_-"
}