Correct probabilistic model checking with floating-point arithmetic

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

Arnd Hartmanns

Publication date: 1 February 2024

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A logic for reasoning about time and reliability
• Model checking of probabilistic and nondeterministic systems
• Automatic verification of real-time systems with discrete probability distributions.
• Value Iteration
• Quantitative Multi-objective Verification for Probabilistic Systems
• Performance analysis of probabilistic timed automata using digital clocks
• 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
• Reachability in MDPs: Refining Convergence of Value Iteration
• 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
• Interval iteration algorithm for MDPs and IMDPs
• Verification of Markov Decision Processes Using Learning Algorithms
• Sound value iteration

Cited In (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

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