Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey
From MaRDI portal
Publication:5175773
DOI10.1007/978-3-319-07317-0_3zbMath1445.68130OpenAlexW103774727WikidataQ57800793 ScholiaQ57800793MaRDI QIDQ5175773
Nils Jansen, Bernd Becker, Erika Ábrahám, Christian Dehnert, Ralf Wimmer, Joost-Pieter Katoen
Publication date: 25 February 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-07317-0_3
Computational methods in Markov chains (60J22) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items
Analysis of faults in cyber-physical systems by finite discrete-time Markov chains ⋮ Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints ⋮ Counterexample-guided inductive synthesis for probabilistic systems ⋮ On relative and probabilistic finite counterability ⋮ Inductive synthesis for probabilistic programs reaches new horizons
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A note on two problems in connexion with graphs
- K\(^{\ast}\): A heuristic search algorithm for finding the \(k\) shortest paths
- SCIP: solving constraint integer programs
- A linear process-algebraic format with data for probabilistic automata
- Obtaining shorter regular expressions from finite-state automata
- 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
- Minimal Critical Subsystems for Discrete-Time Markov Models
- A counterexample-guided abstraction-refinement framework for markov decision processes
- Stochastic Model Checking
- Hierarchical Counterexamples for Discrete-Time Markov Chains
- Counterexample-guided abstraction refinement for symbolic model checking
- Extended Directed Search for Probabilistic Timed Reachability
- The Birth of Model Checking
- Probabilistic CEGAR
- Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
- Finding the k Shortest Paths
- Symbolic model checking for probabilistic processes
- Causes and Explanations: A Structural-Model Approach. Part I: Causes
- Verification: Theory and Practice
- Theoretical Aspects of Computing - ICTAC 2004
- Counterexamples in Probabilistic Model Checking
