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

abstractionprobabilistic modelsmodel repair

Mathematics Subject Classification ID

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

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

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

Describes a project that uses

Uses Software

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

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)