Publication Details
Model Repair Revamped - On the Automated Synthesis of Markov Chains -
model repair, synthesis of Markov chains, counter-examples, abstraction
refinement
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.
@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_-"
}