Stochastic Model Checking: Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems. International Autumn School, ROCKS 2012, Vahrn, Italy, October 22-26, 2012. Advanced Lectures

Anne Remke (Editor), Mariëlle Stoelinga (Editor)

    Research output: Book/ReportBook editingAcademic

    Abstract

    Stochastic models are widely used in the modeling and analysis of a wide range of phenomena, ranging from psychology, speech recognition, to political coalition forming, particle behavior, and many more applications. Their use in computer science is also wide-spread, for instance, in performance modeling, analysis of randomized algorithms, and communication protocols that form the structure of the Internet. Stochastic model checking is an important field in stochastic analysis. It has rapidly gained popularity, due to its powerful and systematic methods for modeling and analyzing stochastic systems. In order to inform young researchers about the fundamentals and state of the art in stochastic model checking, an Autumn School was organized by the ROCKS project, funded by the Dutch NWO and German DFG. The school was held during Ocotber 22-26, 2012, in Vahrn, Italy. Leading scientists from the field gave lectures on foundations as well as state-of-the-art research. The seven chapters of this tutorial were initiated at the ROCKS Autumn School, summarizing the state of the art in the field, centered around the three areas of stochastic models, abstraction techniques, and stochastic model checking. All submissions were thoroughly reviewed in a two-stage review process by at least three Program Committee members and in the end the committee decided to accept all seven papers. Stochastic model checking is a rich field, which provides powerful and systematic methods for modeling and analyzing stochastic systems. A wide variety of stochastic models exist, depending on probabilistic choices that are used (discrete, continuous, or both), on whether nondeterminism is present (Markov models versus decision models) and the state space of the models (discrete versus continuous). These models allow for a wide variety of analysis methods to investigate their behavior and properties.
    Original languageEnglish
    Place of PublicationLondon
    PublisherSpringer
    Number of pages281
    ISBN (Electronic)978-3-662-45489-3
    ISBN (Print)978-3-662-45488-6
    DOIs
    Publication statusPublished - Oct 2014

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume8453
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Keywords

    • Probabilistic
    • EC Grant Agreement nr.: FP7/2007-2013
    • Mean-field approximation
    • IR-101937
    • Markov reward models
    • EWI-25663
    • Non-deterministic
    • Oscillatory Behavior
    • METIS-309870
    • Interactive Markov chains
    • EC Grant Agreement nr.: FP7/318490
    • EC Grant Agreement nr.: FP7/318003
    • stochastic

    Fingerprint Dive into the research topics of 'Stochastic Model Checking: Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems. International Autumn School, ROCKS 2012, Vahrn, Italy, October 22-26, 2012. Advanced Lectures'. Together they form a unique fingerprint.

  • Cite this