Model checking expected time and expected reward formulae with random time bounds

DOI10.1016/j.camwa.2005.11.016zbMath1104.68067OpenAlexW2047473202WikidataQ59323919 ScholiaQ59323919MaRDI QIDQ2494794

Yanyan Li

Publication date: 30 June 2006

Published in: Computers \& Mathematics with Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.camwa.2005.11.016

zbMATH Keywords

Markov reward processesContinuous time Markov chainsContinuous stochastic logicExpected reward operatorExpected time operatorMixed Poisson expected sojourn timesUniformisation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Continuous-time Markov processes on discrete state spaces (60J27)

Related Items (8)

Analyzing Oscillatory Behavior with Formal Methods ⋮ Precise parameter synthesis for stochastic biochemical systems ⋮ Modelling the variation and uncertainty problem of right-turn-on-red queue in a variety of conflicting environments ⋮ Consecutive customer losses in regular and oscillating \(M^{X}/ G /1/ n\) systems ⋮ Analysis of \(GI^{X}/ M(n)// N\) systems with stochastic customer acceptance policy ⋮ Mixing logics and rewards for the component-oriented specification of performance measures ⋮ Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata ⋮ Computing Cumulative Rewards Using Fast Adaptive Uniformization

Uses Software

• PRISM

Cites Work

• An effective numerical method to compute the moments of the completion time of Markov reward models
• A logic for reasoning about time and reliability
• The Randomization Technique as a Modeling Tool and Solution Procedure for Transient Markov Processes
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Model-checking continuous-time Markov chains
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Model checking expected time and expected reward formulae with random time bounds