Correct probabilistic model checking with floating-point arithmetic

DOI10.1007/978-3-030-99527-0_3zbMATH Open1547.68429MaRDI QIDQ6535604

Arnd Hartmanns

Publication date: 1 February 2024

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)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Performance analysis of probabilistic timed automata using digital clocks
• 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
• Optimistic value iteration
• A compositional modelling and analysis framework for stochastic hybrid systems
• 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
• Interval iteration algorithm for MDPs and IMDPs
• Model checking of probabilistic and nondeterministic systems
• Quantitative Multi-objective Verification for Probabilistic Systems
• Reachability in MDPs: Refining Convergence of Value Iteration
• Verification of Markov Decision Processes Using Learning Algorithms
• Value Iteration
• Sound value iteration

Related Items (2)

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