Energy-Utility Analysis for Resilient Systems Using Probabilistic Model Checking

DOI10.1007/978-3-319-07734-5_2zbMATH Open1407.68280OpenAlexW18579693MaRDI QIDQ5166754FDOQ5166754

Sascha Klüppelholz, Linda Leuschner, Christel Baier, Clemens Dubslaff

Publication date: 8 July 2014

Published in: Application and Theory of Petri Nets and Concurrency (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-07734-5_2

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) 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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Approximation Theorems of Mathematical Statistics
• The complexity of probabilistic verification
• A logic for reasoning about time and reliability
• Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
• Automata, logics, and infinite games. A guide to current research
• Model checking of probabilistic and nondeterministic systems
• Formal Modeling and Analysis of Timed Systems
• Conditional Probabilities over Probabilistic and Nondeterministic Systems
• Model checking conditional CSL for continuous-time Markov chains
• Performability assessment by model checking of Markov reward models
• Measure and probability for concurrency theorists
• Markov ratio decision processes
• Probabilistic Model Checking for Energy-Utility Analysis
• Weight monitoring with linear temporal logic
• Computing Quantiles in Markov Reward Models

Cited In (2)

• Compositional strategy synthesis for stochastic games with multiple objectives
• Probabilistic Model Checking for Energy-Utility Analysis

Uses Software

• PRISM
• MRMC

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

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