Inductive synthesis for probabilistic programs reaches new horizons

DOI10.1007/978-3-030-72016-2_11MaRDI QIDQ2044199zbMATH OpenOpenAlexFDO

Authors Roman Andriushchenko, Milan Češka, Sebastian Junges, Joost-Pieter Katoen

Publication date 4 August 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2101.12683

Mathematics Subject Classification ID

Computational methods in Markov chains (60J22) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Abstract: This paper presents a novel method for the automated synthesis of probabilistic programs. The starting point is a program sketch representing a finite family of finite-state Markov chains with related but distinct topologies, and a PCTL specification. The method builds on a novel inductive oracle that greedily generates counter-examples (CEs) for violating programs and uses them to prune the family. These CEs leverage the semantics of the family in the form of bounds on its best- and worst-case behaviour provided by a deductive oracle using an MDP abstraction. The method further monitors the performance of the synthesis and adaptively switches between the inductive and deductive reasoning. Our experiments demonstrate that the novel CE construction provides a significantly faster and more effective pruning strategy leading to acceleration of the synthesis process on a wide range of benchmarks. For challenging problems, such as the synthesis of decentralized partially-observable controllers, we reduce the run-time from a day to minutes.

Recommendations

• Counterexample-guided inductive synthesis for probabilistic systems
• Data-driven synthesis of full probabilistic programs
• A theory of formal synthesis via inductive learning
• From program verification to program synthesis
• Counterexample guided inductive synthesis modulo theories

Cites work

• A concise introduction to decentralized POMDPs
• Abstract model repair for probabilistic systems
• Counterexample generation for discrete-time Markov models: an introductory survey
• Farkas certificates and minimal witnesses for probabilistic reachability constraints
• Fast debugging of PRISM models
• High-level counterexamples for probabilistic automata
• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 1131474 (Why is no real title available?)
• Model checking probabilistic systems
• Model repair for probabilistic systems
• Optimizing synthesis with metasketches
• Parameter synthesis for Markov models: faster than ever
• Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
• Precise parameter synthesis for stochastic biochemical systems
• Probabilistic self-stabilization
• Probabilistic verification of Herman's self-stabilisation algorithm
• Reachability in augmented interval Markov chains
• Theoretical Aspects of Computing - ICTAC 2004

Cited in

(14)

• Counterexample-guided inductive synthesis for probabilistic systems
• Data-driven synthesis of full probabilistic programs
• Gradient-descent for randomized controllers under partial observability
• Parameter synthesis in Markov models: a gentle survey
• Efficient synthesis with probabilistic constraints
• Abstraction-Refinement for Hierarchical Probabilistic Models
• Robust almost-sure reachability in multi-environment MDPs
• Search and explore: symbiotic policy synthesis in POMDPs
• Counterexample-driven synthesis for probabilistic program sketches
• Probabilistic program verification via inductive synthesis of inductive invariants
• Deductive controller synthesis for probabilistic hyperproperties
• Witnessing subsystems for probabilistic systems with low tree width
• Search and explore: symbiotic policy synthesis in POMDPs
• An oracle-guided approach to constrained policy synthesis under uncertainty

This page was built for publication: Inductive synthesis for probabilistic programs reaches new horizons

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2044199)