Publication Details

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

ČEŠKA Milan, HENSE Christian, JANSEN Nils, JUNGES Sebastian and KATOEN Joost-Pieter. Model Repair Revamped - On the Automated Synthesis of Markov Chains -. From Reactive Systems to Cyber-Physical Systems. Lecture Notes of Computer Science. Cham: Springer International Publishing, 2019, pp. 107-125. ISBN 978-3-030-31513-9. Available from: https://www.researchgate.net/publication/335984637_Model_Repair_Revamped_-_On_the_Automated_Synthesis_of_Markov_Chains_-
Czech title
Automatizovaná syntéza pravděpodobnostních modelů
Type
book chapter
Language
english
Authors
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT)
Hense Christian (RWTH Aachen University)
Jansen Nils (RUN)
Junges Sebastian (RWTH Aachen University)
Katoen Joost-Pieter (RWTH)
URL
Keywords

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

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.

Published
2019
Pages
107-125
Book
From Reactive Systems to Cyber-Physical Systems
Series
Lecture Notes of Computer Science
ISBN
978-3-030-31513-9
Publisher
Springer International Publishing
Place
Cham, CH
DOI
10.1007/978-3-030-31514-6_7
EID Scopus
2-s2.0-85073163783
BibTeX 
@INBOOK{FITPUB12150,
   author = "Milan \v{C}e\v{s}ka and Christian Hense and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen",
   title = "Model Repair Revamped - On the Automated Synthesis of Markov Chains -",
   pages = "107--125",
   booktitle = "From Reactive Systems to Cyber-Physical Systems",
   series = "Lecture Notes of Computer Science",
   year = 2019,
   location = "Cham, CH",
   publisher = "Springer International Publishing",
   ISBN = "978-3-030-31513-9",
   doi = "10.1007/978-3-030-31514-6\_7",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12150"
}
Back to top