Multiphase until formulas over Markov reward models: an algebraic approach

DOI10.1016/J.TCS.2015.07.047MaRDI QIDQ896909zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Performability assessment by model checking of Markov reward models
• Formal Modeling and Analysis of Timed Systems
• scientific article; zbMATH DE number 1670870
• Model-checking continuous-time Markov chains
• Computing quantiles in Markov reward models

Cites work

• scientific article; zbMATH DE number 1670870 (Why is no real title available?)
• scientific article; zbMATH DE number 3465382 (Why is no real title available?)
• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 1361121 (Why is no real title available?)
• scientific article; zbMATH DE number 729460 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• Automata-based CSL model checking
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Conditional Probabilities over Probabilistic and Nondeterministic Systems
• Cylindrical Algebraic Decomposition I: The Basic Algorithm
• Efficient CSL model checking using stratification
• Formal Modeling and Analysis of Timed Systems
• Model checking conditional CSL for continuous-time Markov chains
• Model checking of probabilistic and nondeterministic systems
• Nineteen Dubious Ways to Compute the Exponential of a Matrix, Twenty-Five Years Later
• Performability assessment by model checking of Markov reward models
• Performance-Related Reliability Measures for Computing Systems
• Some decidable results on reachability of solvable 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. Procee

Cited in

(6)

• 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
• scientific article; zbMATH DE number 1670870 (Why is no real title available?)
• Performability assessment by model checking of Markov reward models
• Computing quantiles in Markov reward models

Describes a project that uses

Uses Software

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

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)