Energy-utility analysis for resilient systems using probabilistic model checking

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

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

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)

Recommendations

• Trade-off analysis meets probabilistic model checking
• Probabilistic model checking for energy-utility analysis
• Resilience analysis of multi-state systems with time-dependent behaviors
• An SRN-based resiliency quantification approach
• Model checking probabilistic systems

Cites work

• scientific article; zbMATH DE number 1361118 (Why is no real title available?)
• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 846904 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A logic for reasoning about time and reliability
• Approximation Theorems of Mathematical Statistics
• Automata, logics, and infinite games. A guide to current research
• Computing quantiles in Markov reward models
• Conditional Probabilities over Probabilistic and Nondeterministic Systems
• Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
• Formal Modeling and Analysis of Timed Systems
• Markov ratio decision processes
• Measure and probability for concurrency theorists
• Model checking conditional CSL for continuous-time Markov chains
• Model checking of probabilistic and nondeterministic systems
• Performability assessment by model checking of Markov reward models
• Probabilistic model checking for energy-utility analysis
• The complexity of probabilistic verification
• Weight monitoring with linear temporal logic

Cited in

(4)

• An SRN-based resiliency quantification approach
• Probabilistic model checking for energy-utility analysis
• Resilience analysis of multi-state systems with time-dependent behaviors
• Compositional strategy synthesis for stochastic games with multiple objectives

Describes a project that uses

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)