Performability assessment by model checking of Markov reward models

DOI10.1007/S10703-009-0088-7MaRDI QIDQ968359zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Christel Baier, Lucia Cloth, B. R. Haverkort, Holger Hermanns, Joost-Pieter Katoen

Publication date 5 May 2010

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-009-0088-7

zbMATH Keywords

model checkingMarkov reward modelsperformability

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1670870
• Model checking for performability
• scientific article; zbMATH DE number 1946767
• Multiphase until formulas over Markov reward models: an algebraic approach
• Formal Modeling and Analysis of Timed Systems

Cites work

• scientific article; zbMATH DE number 1670788 (Why is no real title available?)
• scientific article; zbMATH DE number 1670870 (Why is no real title available?)
• scientific article; zbMATH DE number 19243 (Why is no real title available?)
• scientific article; zbMATH DE number 1361121 (Why is no real title available?)
• scientific article; zbMATH DE number 1956596 (Why is no real title available?)
• scientific article; zbMATH DE number 1461224 (Why is no real title available?)
• scientific article; zbMATH DE number 1867253 (Why is no real title available?)
• scientific article; zbMATH DE number 763717 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A Compositional Approach to Performance Modelling
• A fast algorithm for the transient reward distribution in continuous-time Markov chains
• A logic for reasoning about time and reliability
• Approximate performability and dependability analysis using generalized stochastic Petri nets
• Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
• Calculating the distribution of a linear combination of uniform order statistics
• Distribution of the minimal completion time of parallel tasks in multi-reward semi-Markov models
• Fluid stochastic Petri nets: Theory, applications, and solution techniques
• Logic in Computer Science
• Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains
• Model-checking continuous-time Markov chains
• Multi-Objective Model Checking of Markov Decision Processes
• Occupation times in markov processes
• On Evaluating the Performability of Degradable Computing Systems
• On Reduction Criteria for Probabilistic Reward Models
• On the numerical analysis of inhomogeneous continuous-time Markov chains
• Performability: a retrospective and some pointers to the future
• Performance-Related Reliability Measures for Computing Systems
• Process algebra for performance evaluation
• RECAL—a new efficient algorithm for the exact analysis of multiple-chain closed queuing networks
• Reward model solution methods with impulse and rate rewards: an algorithm and numerical results
• State-space support for path-based reward variables
• Stochastic model checking
• The Distribution of Linear Combinations of Order Statistics from the Uniform Distribution
• The Randomization Technique as a Modeling Tool and Solution Procedure for Transient Markov Processes
• The exact and approximate distributions of linear combinations of selected order statistics from a uniform distribution
• Tools and Algorithms for the Construction and Analysis of Systems
• Using branching time temporal logic to synthesize synchronization skeletons
• Using probabilistic model checking for dynamic power management

Cited in

(15)

• Multiphase until formulas over Markov reward models: an algebraic approach
• Probabilistic model checking for energy-utility analysis
• Specification techniques for Markov reward models
• scientific article; zbMATH DE number 1946767 (Why is no real title available?)
• Model checking for performability
• Mixing logics and rewards for the component-oriented specification of performance measures
• Performance analysis of Markov regenerative reward models
• scientific article; zbMATH DE number 1670870 (Why is no real title available?)
• Energy-utility analysis for resilient systems using probabilistic model checking
• Model Checking Constrained Markov Reward Models with Uncertainties
• Formal Modeling and Analysis of Timed Systems
• Performability analysis of computer systems: from model specification to solution
• Performability measure for acyclic Markovian models
• Computing quantiles in Markov reward models
• Performance evaluation with temporal rewards

Describes a project that uses

Uses Software

• MRMC

This page was built for publication: Performability assessment by model checking of Markov reward models

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