Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
Č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
https://www.researchgate.net/publication/335984637_Model_Repair_Revamped_-_On_the_Automated_Synthesis_of_Markov_Chains_-
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_-" }