Abstract
Probabilistic programs are key to deal with uncertainty in e.g. controller synthesis. They are typically small but intricate. Their development is complex and error prone requiring quantitative reasoning over a myriad of alternative designs. To mitigate this complexity, we adopt counterexample-guided inductive synthesis (CEGIS) to automatically synthesise finite-state probabilistic programs. Our approach leverages efficient model checking, modern SMT solving, and counterexample generation at program level. Experiments on practically relevant case studies show that design spaces with millions of candidate designs can be fully explored using a few thousand verification queries.
Abstract (translated)
概率程序是处理控制器综合等不确定性的关键。它们通常很小但很复杂。它们的开发是复杂的，容易出错，需要对各种备选设计进行定量推理。为了降低这种复杂性，我们采用反例引导归纳综合（CEGIS）来自动综合有限状态概率程序。我们的方法利用了高效的模型检查、现代SMT解决方案和程序级的反例生成。对实际相关案例研究的实验表明，使用几千个验证查询可以充分探索具有数百万个候选设计的设计空间。
URL
https://arxiv.org/abs/1904.12371
