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

DOI10.1016/J.CAMWA.2005.11.016MaRDI QIDQ2494794zbMATH OpenOpenAlexWikidataFDO

Authors 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

Continuous stochastic logicContinuous time Markov chainsExpected reward operatorExpected time operatorMarkov reward processesMixed Poisson expected sojourn timesUniformisation

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2090708
• scientific article; zbMATH DE number 1670870
• Formal Modeling and Analysis of Timed Systems
• scientific article; zbMATH DE number 1670788
• Model checking conditional CSL for continuous-time Markov chains

Cites work

• A logic for reasoning about time and reliability
• An effective numerical method to compute the moments of the completion time of Markov reward models
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• scientific article; zbMATH DE number 1670788 (Why is no real title available?)
• scientific article; zbMATH DE number 431650 (Why is no real title available?)
• scientific article; zbMATH DE number 1243444 (Why is no real title available?)
• scientific article; zbMATH DE number 1361121 (Why is no real title available?)
• scientific article; zbMATH DE number 1461224 (Why is no real title available?)
• scientific article; zbMATH DE number 2087806 (Why is no real title available?)
• scientific article; zbMATH DE number 1884410 (Why is no real title available?)
• scientific article; zbMATH DE number 1884412 (Why is no real title available?)
• scientific article; zbMATH DE number 2090708 (Why is no real title available?)
• scientific article; zbMATH DE number 846904 (Why is no real title available?)
• scientific article; zbMATH DE number 3082073 (Why is no real title available?)
• Model-checking continuous-time Markov chains
• The Randomization Technique as a Modeling Tool and Solution Procedure for Transient Markov Processes

Cited in

(9)

• Precise parameter synthesis for stochastic biochemical systems
• 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
• Analyzing oscillatory behavior with formal methods
• Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata
• scientific article; zbMATH DE number 2090708 (Why is no real title available?)
• Computing cumulative rewards using fast adaptive uniformization
• Modelling the variation and uncertainty problem of right-turn-on-red queue in a variety of conflicting environments
• Mixing logics and rewards for the component-oriented specification of performance measures

Describes a project that uses

Uses Software

• PRISM

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

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