Discrete-time rewards model-checked

DOI10.1007/978-3-540-40903-8_8MaRDI QIDQ5717503zbMATH OpenOpenAlexFDO

Authors Holger Hermanns, S. Andova, Joost-Pieter Katoen

Publication date 10 January 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b12025

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Performability assessment by model checking of Markov reward models
• Stochastic model checking
• Model-checking for probabilistic real-time systems
• Modelling and analysis of Markov reward automata
• Probabilistic model checking: Formalisms and algorithms for discrete and real-time systems

Cited in

(25)

• A comparison of time- and reward-bounded probabilistic model checking techniques
• Symbolic dependency graphs for \(\mathrm {PCTL}^{>}_{\leq}\) model-checking
• Computation tree measurement language (CTML)
• Verification of multiplayer stochastic games via abstract dependency graphs
• Multi-cost bounded tradeoff analysis in MDP
• Automatic verification of competitive stochastic systems
• Cost vs. time in stochastic games and Markov automata
• Model checking expected time and expected reward formulae with random time bounds
• Ratio and weight quantiles
• Model Checking Exact Cost for Attack Scenarios
• Modelling and analysis of Markov reward automata
• Weighted versus Probabilistic Logics
• Architecture-based resilience evaluation for self-adaptive systems
• Computing quantiles in Markov reward models
• Quantitative model-checking of controlled discrete-time Markov processes
• Energy-utility analysis for resilient systems using probabilistic model checking
• On Reduction Criteria for Probabilistic Reward Models
• Model Checking Constrained Markov Reward Models with Uncertainties
• On the use of model and logical embeddings for model checking of probabilistic systems
• Parameter synthesis for Markov models: covering the parameter space
• A no-go theorem for coalgebraic product construction
• Runtime monitors for Markov decision processes
• Performance analysis of probabilistic timed automata using digital clocks
• Multiphase until formulas over Markov reward models: an algebraic approach
• Performability assessment by model checking of Markov reward models

This page was built for publication: Discrete-time rewards model-checked

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