Counterexamples in Probabilistic Model Checking

DOI10.1007/978-3-540-71209-1_8MaRDI QIDQ5758104zbMATH OpenOpenAlexFDO

Authors Tingting Han, Joost-Pieter Katoen

Publication date 3 September 2007

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71209-1_8

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

• Counterexamples in Probabilistic LTL Model Checking for Markov Chains
• The probabilistic model checking landscape
• Bounded model checking for probabilistic programs
• Model checking probabilistic systems against pushdown specifications
• Model checking probabilistic systems
• Model checking of recursive probabilistic systems
• Model checking of probabilistic and nondeterministic systems
• Formal Modeling and Analysis of Timed Systems

Cited in

(19)

• On Abstraction of Probabilistic Systems
• Counterexamples in Probabilistic LTL Model Checking for Markov Chains
• Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking
• Probabilistic CEGAR
• Survey on Directed Model Checking
• Minimal counterexamples for linear-time probabilistic verification
• K\(^{\ast}\): A heuristic search algorithm for finding the \(k\) shortest paths
• Zero-reachability in probabilistic multi-counter automata
• Farkas certificates and minimal witnesses for probabilistic reachability constraints
• Model checking linear-time properties of probabilistic systems
• Counterexample generation for discrete-time Markov models: an introductory survey
• High-level counterexamples for probabilistic automata
• Counterexamples revisited: principles, algorithms, applications
• Model Checking Software
• Conditional Probabilities over Probabilistic and Nondeterministic Systems
• Formal Modeling and Analysis of Timed Systems
• Generating counterexamples for quantitative safety specifications in probabilistic B
• How hard is finding shortest counter-example lassos in model checking?
• Tracy, traces, and transducers: computable counterexamples and explanations for HyperLTL model-checking

This page was built for publication: Counterexamples in Probabilistic Model Checking

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