Counterexample-guided inductive synthesis for probabilistic systems
type: Item
instance of: scholarly article
title: Counterexample-guided inductive synthesis for probabilistic systems
author: Milan Češka
author: Christian Hensel
author: Sebastian Junges
author: Joost-Pieter Katoen
published in: Formal Aspects of Computing
publication date: 2021-09-14T00:00:00Z
Mathematics Subject Classification ID: 68-XX
zbMATH DE Number: 7395147
zbMATH Keywords: program synthesis
zbMATH Keywords: Markov chains
zbMATH Keywords: probabilistic model checking
zbMATH Keywords: counterexamples
zbMATH Keywords: CEGIS
describes a project that uses: Storm
describes a project that uses: PRISM
describes a project that uses: z3
describes a project that uses: POMDP
describes a project that uses: Jani
MaRDI profile type: MaRDI publication profile
full work available at URL: s00165-021-00547-2
OpenAlex ID: W3163311278
Wikidata QID: Q124796813
cites work: Counterexample generation for discrete-time Markov models: an introductory survey
cites work: Counterexample guided inductive synthesis modulo theories
cites work: 20 years of modal and mixed specifications.
cites work: Model checking probabilistic systems
cites work: Model repair for probabilistic systems
cites work: Q5503674
cites work: Q5322945
cites work: Dual-priced modal transition systems with time durations
cites work: Refinement checking on parametric modal transition systems
cites work: Optimizing synthesis with metasketches
cites work: Syntax-guided optimal synthesis for chemical reaction networks
cites work: Bridging Boolean and quantitative synthesis using smoothed proof search
cites work: Precise parameter synthesis for stochastic biochemical systems
cites work: Reachability in augmented interval Markov chains
cites work: Fast debugging of PRISM models
cites work: Abstract probabilistic automata
cites work: More scalable LTL model checking via discovering design-space dependencies \((D^3)\)
cites work: A theory of formal synthesis via inductive learning
cites work: The probabilistic model checking landscape
cites work: Planning and acting in partially observable stochastic domains
cites work: Probabilistic mobile ambients
cites work: 30 years of modal transition systems: survey of extensions and analysis
cites work: Parameter synthesis for Markov models: faster than ever
cites work: Minimal Critical Subsystems for Discrete-Time Markov Models
cites work: Minimal counterexamples for linear-time probabilistic verification
cites work: High-level counterexamples for probabilistic automata
cites work: Safety-aware apprenticeship learning
DOI: 10.1007/S00165-021-00547-2
Recommended article: Inductive synthesis for probabilistic programs reaches new horizons
Recommended article: A Multi-level Refinement Approach for Structural Synthesis of Optimal Probabilistic Models
Recommended article: Counterexample guided inductive synthesis modulo theories
Recommended article: Modular synthesis of sketches using models
Recommended article: Optimizing synthesis with metasketches
description: scientific article; zbMATH DE number 7395147