Multiphase until formulas over Markov reward models: an algebraic approach

DOI10.1016/J.TCS.2015.07.047zbMATH Open1332.68143OpenAlexW1014907731MaRDI QIDQ896909FDOQ896909

Ming Xu, David N. Jansen, Huibiao Zhu, Zongyuan Yang, Lijun 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

transcendental numbercylindrical algebraic decompositionprobabilistic model checkingcontinuous stochastic logicMarkov reward model

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

• Nineteen Dubious Ways to Compute the Exponential of a Matrix, Twenty-Five Years Later
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Model checking of probabilistic and nondeterministic systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Title not available (Why is that?)
• Cylindrical Algebraic Decomposition I: The Basic Algorithm
• Formal Modeling and Analysis of Timed Systems
• 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
• Performance-Related Reliability Measures for Computing Systems
• Title not available (Why is that?)
• Automata-Based CSL Model Checking
• Conditional Probabilities over Probabilistic and Nondeterministic Systems
• Model checking conditional CSL for continuous-time Markov chains
• Title not available (Why is that?)
• Some decidable results on reachability of solvable systems
• Efficient CSL model checking using stratification
• Performability assessment by model checking of Markov reward models

Cited In (4)

• 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
• Title not available (Why is that?)

Uses Software

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

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

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