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

Fingerprint

Stochastic systems
Model checking
Stochastic models
Speech recognition
Computer science
Internet
Network protocols

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

Cite this

@book{74e34d57065c4fc6ad1a086a9d60a6e3,
title = "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",
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.",
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",
editor = "Anne Remke and Mari{\"e}lle Stoelinga",
note = "International Autumn School, ROCKS 2012, Vahrn, Italy, October 22-26, 2012, Advanced Lectures",
year = "2014",
month = "10",
doi = "10.1007/978-3-662-45489-3",
language = "English",
isbn = "978-3-662-45488-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",

}

TY - BOOK

T1 - Stochastic Model Checking

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

A2 - Remke, Anne

A2 - Stoelinga, Mariëlle

N1 - International Autumn School, ROCKS 2012, Vahrn, Italy, October 22-26, 2012, Advanced Lectures

PY - 2014/10

Y1 - 2014/10

N2 - 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.

AB - 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.

KW - Probabilistic

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - Mean-field approximation

KW - IR-101937

KW - Markov reward models

KW - EWI-25663

KW - Non-deterministic

KW - Oscillatory Behavior

KW - METIS-309870

KW - Interactive Markov chains

KW - EC Grant Agreement nr.: FP7/318490

KW - EC Grant Agreement nr.: FP7/318003

KW - stochastic

U2 - 10.1007/978-3-662-45489-3

DO - 10.1007/978-3-662-45489-3

M3 - Book editing

SN - 978-3-662-45488-6

T3 - Lecture Notes in Computer Science

BT - Stochastic Model Checking

PB - Springer

CY - London

ER -