Model checking for performability

DOI10.1017/S0960129512000254MaRDI QIDQ2843861zbMATH OpenDBLPWikidataFDO

Authors Ernst Moritz Hahn, B. R. Haverkort, Holger Hermanns, Christel Baier, Joost-Pieter Katoen

Publication date 26 August 2013

Published in MSCS. Mathematical Structures in Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Performability assessment by model checking of Markov reward models
• scientific article; zbMATH DE number 1670870
• scientific article; zbMATH DE number 1946767
• scientific article; zbMATH DE number 2155192
• Model checking functional and performability properties of stochastic fluid models

Cites work

• A fast algorithm for the transient reward distribution in continuous-time Markov chains
• Abstraction Refinement for Probabilistic Software
• Analysis of a composite performance reliability measure for fault-tolerant systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Bisimulation through probabilistic testing
• Comparative branching-time semantics for Markov chains
• Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
• Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
• Finite State Continuous Time Markov Decision Processes with a Finite Planning Horizon
• Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games
• Mixing logics and rewards for the component-oriented specification of performance measures
• Model Checking Interactive Markov Chains
• Model-checking continuous-time Markov chains
• Numerical transient analysis of Markov models
• Occupation times in markov processes
• On the use of MTBDDs for performability analysis and verification of stochastic systems.
• Optimal reachability for multi-priced timed automata
• Performability assessment by model checking of Markov reward models
• Performability modelling tools and techniques
• Performability: a retrospective and some pointers to the future
• Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
• Randomization Procedures in the Computation of Cumulative-Time Distributions over Discrete State Markov Processes
• Reward model solution methods with impulse and rate rewards: an algorithm and numerical results
• Three-Valued Abstraction for Continuous-Time Markov Chains
• Transient analysis of cumulative measures of markov model behavior

Cited in

(15)

• Logical characterization of fluid equivalences
• scientific article; zbMATH DE number 749807 (Why is no real title available?)
• scientific article; zbMATH DE number 1946767 (Why is no real title available?)
• Construction and verification of performance and reliability models
• Model checking functional and performability properties of stochastic fluid models
• scientific article; zbMATH DE number 1890701 (Why is no real title available?)
• scientific article; zbMATH DE number 1670870 (Why is no real title available?)
• Quantitative Analysis of Concurrent Reversible Computations
• Performability assessment by model checking of Markov reward models
• Performability: a retrospective and some pointers to the future
• scientific article; zbMATH DE number 1786471 (Why is no real title available?)
• scientific article; zbMATH DE number 644287 (Why is no real title available?)
• scientific article; zbMATH DE number 1744972 (Why is no real title available?)
• scientific article; zbMATH DE number 1629928 (Why is no real title available?)
• scientific article; zbMATH DE number 2155192 (Why is no real title available?)

This page was built for publication: Model checking for performability

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