Probabilistic Model Checking for Energy-Utility Analysis

DOI10.1007/978-3-319-06880-0_5zbMath1407.68279OpenAlexW103082649MaRDI QIDQ5418957

Sascha Wunderlich, Clemens Dubslaff, Sascha Klüppelholz, Joachim Klein, Christel Baier

Publication date: 2 June 2014

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

Full work available at URL: https://doi.org/10.1007/978-3-319-06880-0_5

Mathematics Subject Classification ID

Continuous-time Markov processes on general state spaces (60J25) Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (6)

Ratio and Weight Quantiles ⋮ Probabilistic verification of hierarchical leader election protocol in dynamic systems ⋮ Maximizing the Conditional Expected Reward for Reaching the Goal ⋮ Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies ⋮ Energy-Utility Analysis for Resilient Systems Using Probabilistic Model Checking ⋮ Nearly Optimal Verifiable Data Streaming

Uses Software

• PRISM
• MRMC
• ProbDiVinE
• CADP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Performability assessment by model checking of Markov reward models
• Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
• Measure and probability for concurrency theorists
• Energy parity games
• Automata, logics, and infinite games. A guide to current research
• Model checking conditional CSL for continuous-time Markov chains
• Approximating the termination value of one-counter MDPs and stochastic games
• Synthesizing Efficient Controllers
• One-Counter Stochastic Games
• Temporal Specifications with Accumulative Values
• Model checking of probabilistic and nondeterministic systems
• Quantitative Multi-objective Verification for Probabilistic Systems
• CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Energy and Mean-Payoff Parity Markov Decision Processes
• Multi-Objective Model Checking of Markov Decision Processes
• Computing Quantiles in Markov Reward Models
• Energy-Utility Analysis for Resilient Systems Using Probabilistic Model Checking
• Markov Decision Processes with Multiple Objectives
• Conditional Probabilities over Probabilistic and Nondeterministic Systems
• Foundations of Software Science and Computational Structures

This page was built for publication: Probabilistic Model Checking for Energy-Utility Analysis