Model Repair Revamped: On the Automated Synthesis of Markov Chains

TL;DR

This paper presents two novel automated methods, based on CEGAR and CEGIS, for synthesizing finite-state probabilistic models and programs, with applications in probabilistic programming, controller design, and software engineering.

Contribution

It introduces two new synthesis techniques that improve automation and efficiency in creating probabilistic models and programs, expanding their applicability.

Findings

Effective in synthesizing probabilistic programs

Applicable to controller synthesis of POMDPs

Demonstrated on software product lines

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.