Counterexamples in Probabilistic LTL Model Checking for Markov Chains

DOI10.1007/978-3-642-04081-8_39MaRDI QIDQ3184702zbMATH OpenOpenAlexFDO

Authors Matthias Schmalz, Daniele Varacca, H. 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)

Recommendations

• Counterexamples in Probabilistic Model Checking
• High-level counterexamples for probabilistic automata
• Counterexample generation for discrete-time Markov models: an introductory survey
• Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking
• Hierarchical counterexamples for discrete-time Markov chains

Cites work

• A logic for reasoning about time and reliability
• CONCUR 2005 – Concurrency Theory
• Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
• Counterexamples in Probabilistic LTL Model Checking for Markov Chains
• Counterexamples in Probabilistic Model Checking
• Extended Directed Search for Probabilistic Timed Reachability
• Formal Modeling and Analysis of Timed Systems
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 3240812 (Why is no real title available?)
• scientific article; zbMATH DE number 3278887 (Why is no real title available?)
• Introduction to algorithms
• Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking
• The complexity of probabilistic verification

Cited in

(10)

• 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
• Minimal counterexamples for linear-time probabilistic verification
• scientific article; zbMATH DE number 1884415 (Why is no real title available?)
• Counterexample generation for discrete-time Markov models: an introductory survey
• High-level counterexamples for probabilistic automata
• Counterexamples in Probabilistic Model Checking
• Formal Modeling and Analysis of Timed Systems
• A Debugging Game for Probabilistic Models

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

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