Multiphase until formulas over Markov reward models: an algebraic approach

DOI10.1016/j.tcs.2015.07.047zbMath1332.68143OpenAlexW1014907731MaRDI QIDQ896909

Ming Xu, David N. Jansen, Huibiao Zhu, Zongyuan Yang, Li-jun Zhang

Publication date: 15 December 2015

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2015.07.047

zbMATH Keywords

cylindrical algebraic decompositiontranscendental numberprobabilistic model checkingcontinuous stochastic logicMarkov reward model

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 (3)

Measuring the constrained reachability in quantum Markov chains ⋮ Time-bounded termination analysis for probabilistic programs with delays ⋮ An algebraic method to fidelity-based model checking over quantum Markov chains

Uses Software

• PRISM
• MRMC
• REDLOG
• z3
• REACH
• iscasMc

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Performability assessment by model checking of Markov reward models
• Model checking conditional CSL for continuous-time Markov chains
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
• Some decidable results on reachability of solvable systems
• Efficient CSL Model Checking Using Stratification
• Model checking of probabilistic and nondeterministic systems
• Automata-Based CSL Model Checking
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Performance-Related Reliability Measures for Computing Systems
• Nineteen Dubious Ways to Compute the Exponential of a Matrix, Twenty-Five Years Later
• Cylindrical Algebraic Decomposition I: The Basic Algorithm
• Conditional Probabilities over Probabilistic and Nondeterministic Systems
• Formal Modeling and Analysis of Timed Systems

This page was built for publication: Multiphase until formulas over Markov reward models: an algebraic approach