Constraint-based debugging in probabilistic model checking

DOI10.1007/S00607-022-01130-0MaRDI QIDQ6488104zbMATH OpenFDO

Authors

Publication date 24 March 2023

Published in Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/S00607-022-01130-0

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Recommendations

• Bounded model checking for probabilistic programs
• The probabilistic model checking landscape
• Model checking probabilistic systems against pushdown specifications
• Constraint-based deductive model checking
• On-the-fly probabilistic model checking
• Towards light-weight probabilistic model checking
• Debugging unsatisfiable constraint models
• scientific article; zbMATH DE number 2090706
• Model checking of probabilistic and nondeterministic systems

Cites work

• A logic for reasoning about time and reliability
• Abstract model repair for probabilistic systems
• Automated debugging based on a constraint model of the program and a test case
• Causality checking for complex system models
• Counterexample guided inductive synthesis modulo theories
• Explaining counterexamples using causality
• scientific article; zbMATH DE number 2243367 (Why is no real title available?)
• Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation
• K\(^{\ast}\): A heuristic search algorithm for finding the \(k\) shortest paths
• Minimal Critical Subsystems for Discrete-Time Markov Models
• Model-based diagnosis of hardware designs
• Model-checking continuous-time Markov chains
• On the relationship between model-based debugging and program slicing
• The Birth of Model Checking
• The program dependence graph and its use in optimization
• Whodunit? Causal Analysis for Counterexamples

Cited in

(8)

• Debugging of concurrent systems using counterexample analysis
• Fast debugging of PRISM models
• Extended Directed Search for Probabilistic Timed Reachability
• scientific article; zbMATH DE number 5353387 (Why is no real title available?)
• scientific article; zbMATH DE number 5706177 (Why is no real title available?)
• Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
• High-level counterexamples for probabilistic automata
• A Debugging Game for Probabilistic Models

This page was built for publication: Constraint-based debugging in probabilistic model checking

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