Model checking for performability
From MaRDI portal
Publication:2843861
DOI10.1017/S0960129512000254zbMath1358.68181WikidataQ57800990 ScholiaQ57800990MaRDI QIDQ2843861
Boudewijn R. Haverkort, Holger Hermanns, Ernst Moritz Hahn, Christel Baier, Joost-Pieter Katoen
Publication date: 26 August 2013
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items (2)
Quantitative Analysis of Concurrent Reversible Computations ⋮ Logical characterization of fluid equivalences
Cites Work
- Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games
- Performability assessment by model checking of Markov reward models
- Mixing logics and rewards for the component-oriented specification of performance measures
- Numerical transient analysis of Markov models
- Bisimulation through probabilistic testing
- On the use of MTBDDs for performability analysis and verification of stochastic systems.
- Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
- A fast algorithm for the transient reward distribution in continuous-time Markov chains
- Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
- Comparative branching-time semantics for Markov chains
- Optimal reachability for multi-priced timed automata
- Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
- Randomization Procedures in the Computation of Cumulative-Time Distributions over Discrete State Markov Processes
- Model Checking Interactive Markov Chains
- Abstraction Refinement for Probabilistic Software
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Analysis of a composite performance reliability measure for fault-tolerant systems
- Performability: a retrospective and some pointers to the future
- Reward model solution methods with impulse and rate rewards: an algorithm and numerical results
- Performability modelling tools and techniques
- Occupation times in markov processes
- Transient analysis of cumulative measures of markov model behavior
- Three-Valued Abstraction for Continuous-Time Markov Chains
- Finite State Continuous Time Markov Decision Processes with a Finite Planning Horizon
- Model-checking continuous-time Markov chains
This page was built for publication: Model checking for performability
