Correct probabilistic model checking with floating-point arithmetic

DOI10.1007/978-3-030-99527-0_3MaRDI QIDQ6535604zbMATH OpenFDO

Authors Arnd Hartmanns

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-99527-0_3

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• The demand for reliability in probabilistic verification
• Model checking probabilistic systems
• Verification, Model Checking, and Abstract Interpretation
• Ensuring the reliability of your model checker: interval iteration for Markov decision processes
• Abstraction of Probabilistic Systems

Cites work

• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A compositional modelling and analysis framework for stochastic hybrid systems
• A logic for reasoning about time and reliability
• Automatic verification of real-time systems with discrete probability distributions.
• Ensuring the reliability of your model checker: interval iteration for Markov decision processes
• Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification
• Interval iteration algorithm for MDPs and IMDPs
• Model checking of probabilistic and nondeterministic systems
• Optimistic value iteration
• Performance analysis of probabilistic timed automata using digital clocks
• Quantitative multi-objective verification for probabilistic systems
• Reachability in MDPs: refining convergence of value iteration
• Sound value iteration
• Tools and algorithms for the construction and analysis of systems. 20th international conference, TACAS 2014, held as part of the European joint conferences on theory and practice of software, ETAPS 2014, Grenoble, France, April 5--13, 2014. Proceedings
• Value Iteration
• Verification of Markov decision processes using learning algorithms

Cited in

(4)

• Computing expected visiting times and stationary distributions in Markov chains: fast and accurate
• Model checking linear dynamical systems under floating-point rounding
• A practitioner's guide to MDP model checking algorithms
• Certificates for probabilistic pushdown automata via optimistic value iteration

This page was built for publication: Correct probabilistic model checking with floating-point arithmetic

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