Counterexample-driven synthesis for probabilistic program sketches

DOI10.1007/978-3-030-30942-8_8MaRDI QIDQ6535945zbMATH OpenFDO

Authors Milan Češka, Christian Hensel, Sebastian Junges, Joost-Pieter Katoen

Publication date 14 March 2024

Full work available at URL https://doi.org/10.1007/978-3-030-30942-8_8

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Counterexample-guided inductive synthesis for probabilistic systems
• Inductive synthesis for probabilistic programs reaches new horizons
• Efficient synthesis with probabilistic constraints
• Counterexample guided inductive synthesis modulo theories
• Data-driven synthesis of full probabilistic programs

Cites work

• scientific article; zbMATH DE number 1131474 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• 20 years of modal and mixed specifications.
• 30 years of modal transition systems: survey of extensions and analysis
• A counterexample-guided abstraction-refinement framework for Markov decision processes
• Abstract probabilistic automata
• Composition and behaviors of probabilistic I/O automata
• Counterexample generation for discrete-time Markov models: an introductory survey
• Counterexample guided inductive synthesis modulo theories
• Dual-priced modal transition systems with time durations
• Fast debugging of PRISM models
• Minimal Critical Subsystems for Discrete-Time Markov Models
• Model checking probabilistic systems
• Model repair for probabilistic systems
• More scalable LTL model checking via discovering design-space dependencies \((D^3)\)
• On the Computational Complexity of Stochastic Controller Optimization in POMDPs
• Optimizing synthesis with metasketches
• Parameter synthesis for Markov models: faster than ever
• Planning and acting in partially observable stochastic domains
• Precise parameter synthesis for stochastic biochemical systems
• Probabilistic mobile ambients
• Probability, Markov chains, queues, and simulation. The mathematical basis of performance modeling.
• Refinement checking on parametric modal transition systems
• Safety-aware apprenticeship learning
• Shepherding hordes of Markov chains
• Syntax-guided optimal synthesis for chemical reaction networks

Cited in

(5)

• An oracle-guided approach to constrained policy synthesis under uncertainty
• Efficient synthesis with probabilistic constraints
• Witnessing subsystems for probabilistic systems with low tree width
• Probabilistic program verification via inductive synthesis of inductive invariants
• Probabilistic counterexample guidance for safer reinforcement learning

This page was built for publication: Counterexample-driven synthesis for probabilistic program sketches

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