Abstract model repair for probabilistic systems

DOI10.1016/J.IC.2018.02.019MaRDI QIDQ1706149zbMATH OpenOpenAlexFDO

Authors G. Chatzieleftheriou, Panagiotis Katsaros

Publication date 21 March 2018

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2018.02.019

zbMATH Keywords

abstractionmodel repairprobabilistic models

Mathematics Subject Classification ID

Temporal logic (03B44) Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Recommendations

• Model repair for probabilistic systems
• Abstract Model Repair
• The Complexity of Linear-Time Temporal Logic Model Repair
• Model checking probabilistic systems
• Model Checking Software

Cites work

• A computationally efficient feasible sequential quadratic programming algorithm
• A counterexample-guided abstraction-refinement framework for Markov decision processes
• A game-based abstraction-refinement framework for Markov decision processes
• Abstract Model Repair
• Abstraction Refinement for Probabilistic Software
• Enhancing model checking in verification by AI techniques
• scientific article; zbMATH DE number 1863177 (Why is no real title available?)
• scientific article; zbMATH DE number 1884411 (Why is no real title available?)
• scientific article; zbMATH DE number 780774 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Model repair for probabilistic systems
• On Abstraction of Probabilistic Systems
• On the metric-based approximate minimization of Markov chains
• Optimal state-space lumping in Markov chains
• Performance analysis of probabilistic timed automata using digital clocks
• Probabilistic CEGAR
• Property preserving abstractions for the verification of concurrent systems
• Quadratic programming is in NP
• Stochastic model checking
• System design of stochastic models using robustness of temporal properties
• Three-valued abstraction for probabilistic systems
• Understanding Maple

Cited in

(11)

• Inductive synthesis for probabilistic programs reaches new horizons
• Synthesizing optimal bias in randomized self-stabilization
• Solving systems of bilinear equations for transition rate reconstruction
• Model repair for probabilistic systems
• Abstract Model Repair
• Are parametric Markov chains monotonic?
• It Sometimes Works: A Lifting Algorithm for Repair of Stochastic Process Algebra Models
• The Complexity of Linear-Time Temporal Logic Model Repair
• Parameter synthesis in Markov models: a gentle survey
• Constraint-based debugging in probabilistic model checking
• Parameter synthesis for Markov models: covering the parameter space

Describes a project that uses

Uses Software

• PRISM
• CEGAR
• PRISM-PSY
• PROPhESY
• Maple
• Storm

This page was built for publication: Abstract model repair for probabilistic systems

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