Counterexample generation for discrete-time Markov models: an introductory survey
From MaRDI portal
Publication:5175773
Recommendations
- Hierarchical counterexamples for discrete-time Markov chains
- Counterexamples in Probabilistic Model Checking
- Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking
- Counterexamples in Probabilistic LTL Model Checking for Markov Chains
- Minimal counterexamples for linear-time probabilistic verification
Cites work
- A counterexample-guided abstraction-refinement framework for Markov decision processes
- A linear process-algebraic format with data for probabilistic automata
- A note on two problems in connexion with graphs
- Causes and Explanations: A Structural-Model Approach. Part I: Causes
- Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
- Counterexample-guided abstraction refinement for symbolic model checking
- Counterexamples in Probabilistic Model Checking
- Counterexamples revisited: principles, algorithms, applications
- Extended Directed Search for Probabilistic Timed Reachability
- Finding the k Shortest Paths
- Formal methods for performance evaluation. 7th international school on formal methods for the design of computer, communication, and software systems, SFM 2007, Bertinoro, Italy, May 28 -- June 2, 2007. Advanced lectures
- Hierarchical counterexamples for discrete-time Markov chains
- scientific article; zbMATH DE number 4089320 (Why is no real title available?)
- scientific article; zbMATH DE number 794262 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- scientific article; zbMATH DE number 2243367 (Why is no real title available?)
- K\(^{\ast}\): A heuristic search algorithm for finding the \(k\) shortest paths
- Minimal Critical Subsystems for Discrete-Time Markov Models
- Obtaining shorter regular expressions from finite-state automata
- Probabilistic CEGAR
- SCIP: solving constraint integer programs
- Stochastic model checking
- Symbolic model checking for probabilistic processes
- The Birth of Model Checking
- Theoretical Aspects of Computing - ICTAC 2004
Cited in
(14)- On relative and probabilistic finite counterability
- Counterexample-guided inductive synthesis for probabilistic systems
- Inductive synthesis for probabilistic programs reaches new horizons
- Hierarchical counterexamples for discrete-time Markov chains
- Counterexamples in Probabilistic LTL Model Checking for Markov Chains
- Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking
- Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
- Minimal counterexamples for linear-time probabilistic verification
- Farkas certificates and minimal witnesses for probabilistic reachability constraints
- Counterexamples revisited: principles, algorithms, applications
- Counterexample-driven synthesis for probabilistic program sketches
- Witnessing subsystems for probabilistic systems with low tree width
- Tracy, traces, and transducers: computable counterexamples and explanations for HyperLTL model-checking
- Analysis of faults in cyber-physical systems by finite discrete-time Markov chains
This page was built for publication: Counterexample generation for discrete-time Markov models: an introductory survey
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5175773)
