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
cylindrical algebraic decompositiontranscendental numberprobabilistic model checkingcontinuous stochastic logicMarkov reward model
Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items (3)
Uses Software
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
