Multiphase until formulas over Markov reward models: an algebraic approach

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

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

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 decomposition; transcendental number; probabilistic model checking; continuous stochastic logic; Markov reward model

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q87: Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Uses Software

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