Counterexamples in Probabilistic LTL Model Checking for Markov Chains

DOI10.1007/978-3-642-04081-8_39zbMath1254.68155OpenAlexW2145002677MaRDI QIDQ3184702

Daniele Varacca, Matthias Schmalz, Hagen Völzer

Publication date: 22 October 2009

Published in: CONCUR 2009 - Concurrency Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04081-8_39

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)

Related Items

Counterexamples in Probabilistic LTL Model Checking for Markov Chains ⋮ Minimal counterexamples for linear-time probabilistic verification

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A logic for reasoning about time and reliability
• Counterexamples in Probabilistic LTL Model Checking for Markov Chains
• Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking
• Extended Directed Search for Probabilistic Timed Reachability
• Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
• The complexity of probabilistic verification
• Counterexamples in Probabilistic Model Checking
• CONCUR 2005 – Concurrency Theory
• Formal Modeling and Analysis of Timed Systems