Importance Sampling for Stochastic Timed Automata

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

5 Citations (Scopus)
130 Downloads (Pure)

Abstract

We present an importance sampling framework that combines symbolic analysis and simulation to estimate the probability of rare reachability properties in stochastic timed automata. By means of symbolic exploration, our framework first identifies states that cannot reach the goal. A state-wise change of measure is then applied on-the-fly during simulations, ensuring that dead ends are never reached. The change of measure is guaranteed by construction to reduce the variance of the estimator with respect to crude Monte Carlo, while experimental results demonstrate that we can achieve substantial computational gains.
Original languageEnglish
Title of host publicationDependable Software Engineering : Theories, Tools, and Applications
EditorsMartin Fränzle, Deepak Kapur, Naijin Zhan
Number of pages16
PublisherSpringer
Publication date2016
Pages163-178
ISBN (Print)978-3-319-47676-6
ISBN (Electronic)978-3-319-47677-3
DOIs
Publication statusPublished - 2016
EventSymposium on Dependable Software Engineering Theories, Tools and Applications - Beijing, China, Beijing, China
Duration: 9 Nov 201610 Nov 2016
http://lcs.ios.ac.cn/setta/

Conference

ConferenceSymposium on Dependable Software Engineering Theories, Tools and Applications
LocationBeijing, China
CountryChina
CityBeijing
Period09/11/201610/11/2016
Internet address
SeriesLecture Notes in Computer Science
Volume9984
ISSN0302-9743

Fingerprint

Importance sampling

Keywords

  • importance sampling
  • rare events
  • stochastic timed automata
  • verification
  • model checking

Cite this

Jegourel, C., Larsen, K. G., Legay, A., Mikučionis, M., Poulsen, D. B., & Sedwards, S. (2016). Importance Sampling for Stochastic Timed Automata. In M. Fränzle, D. Kapur, & N. Zhan (Eds.), Dependable Software Engineering: Theories, Tools, and Applications (pp. 163-178). Springer. Lecture Notes in Computer Science, Vol.. 9984 https://doi.org/10.1007/978-3-319-47677-3_11
Jegourel, Cyrille ; Larsen, Kim Guldstrand ; Legay, Axel ; Mikučionis, Marius ; Poulsen, Danny Bøgsted ; Sedwards, Sean. / Importance Sampling for Stochastic Timed Automata. Dependable Software Engineering: Theories, Tools, and Applications. editor / Martin Fränzle ; Deepak Kapur ; Naijin Zhan. Springer, 2016. pp. 163-178 (Lecture Notes in Computer Science, Vol. 9984).
@inproceedings{b980856eef094af89851df0fb5ac2528,
title = "Importance Sampling for Stochastic Timed Automata",
abstract = "We present an importance sampling framework that combines symbolic analysis and simulation to estimate the probability of rare reachability properties in stochastic timed automata. By means of symbolic exploration, our framework first identifies states that cannot reach the goal. A state-wise change of measure is then applied on-the-fly during simulations, ensuring that dead ends are never reached. The change of measure is guaranteed by construction to reduce the variance of the estimator with respect to crude Monte Carlo, while experimental results demonstrate that we can achieve substantial computational gains.",
keywords = "importance sampling, rare events, stochastic timed automata, verification, model checking",
author = "Cyrille Jegourel and Larsen, {Kim Guldstrand} and Axel Legay and Marius Mikučionis and Poulsen, {Danny B{\o}gsted} and Sean Sedwards",
year = "2016",
doi = "10.1007/978-3-319-47677-3_11",
language = "English",
isbn = "978-3-319-47676-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "163--178",
editor = "Martin Fr{\"a}nzle and Deepak Kapur and Naijin Zhan",
booktitle = "Dependable Software Engineering",
address = "Germany",

}

Jegourel, C, Larsen, KG, Legay, A, Mikučionis, M, Poulsen, DB & Sedwards, S 2016, Importance Sampling for Stochastic Timed Automata. in M Fränzle, D Kapur & N Zhan (eds), Dependable Software Engineering: Theories, Tools, and Applications. Springer, Lecture Notes in Computer Science, vol. 9984, pp. 163-178, Symposium on Dependable Software Engineering Theories, Tools and Applications, Beijing, China, 09/11/2016. https://doi.org/10.1007/978-3-319-47677-3_11

Importance Sampling for Stochastic Timed Automata. / Jegourel, Cyrille; Larsen, Kim Guldstrand; Legay, Axel; Mikučionis, Marius; Poulsen, Danny Bøgsted; Sedwards, Sean.

Dependable Software Engineering: Theories, Tools, and Applications. ed. / Martin Fränzle; Deepak Kapur; Naijin Zhan. Springer, 2016. p. 163-178 (Lecture Notes in Computer Science, Vol. 9984).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

TY - GEN

T1 - Importance Sampling for Stochastic Timed Automata

AU - Jegourel, Cyrille

AU - Larsen, Kim Guldstrand

AU - Legay, Axel

AU - Mikučionis, Marius

AU - Poulsen, Danny Bøgsted

AU - Sedwards, Sean

PY - 2016

Y1 - 2016

N2 - We present an importance sampling framework that combines symbolic analysis and simulation to estimate the probability of rare reachability properties in stochastic timed automata. By means of symbolic exploration, our framework first identifies states that cannot reach the goal. A state-wise change of measure is then applied on-the-fly during simulations, ensuring that dead ends are never reached. The change of measure is guaranteed by construction to reduce the variance of the estimator with respect to crude Monte Carlo, while experimental results demonstrate that we can achieve substantial computational gains.

AB - We present an importance sampling framework that combines symbolic analysis and simulation to estimate the probability of rare reachability properties in stochastic timed automata. By means of symbolic exploration, our framework first identifies states that cannot reach the goal. A state-wise change of measure is then applied on-the-fly during simulations, ensuring that dead ends are never reached. The change of measure is guaranteed by construction to reduce the variance of the estimator with respect to crude Monte Carlo, while experimental results demonstrate that we can achieve substantial computational gains.

KW - importance sampling

KW - rare events

KW - stochastic timed automata

KW - verification

KW - model checking

UR - http://people.cs.aau.dk/~marius/stratego/rare.html

U2 - 10.1007/978-3-319-47677-3_11

DO - 10.1007/978-3-319-47677-3_11

M3 - Article in proceeding

SN - 978-3-319-47676-6

T3 - Lecture Notes in Computer Science

SP - 163

EP - 178

BT - Dependable Software Engineering

A2 - Fränzle, Martin

A2 - Kapur, Deepak

A2 - Zhan, Naijin

PB - Springer

ER -

Jegourel C, Larsen KG, Legay A, Mikučionis M, Poulsen DB, Sedwards S. Importance Sampling for Stochastic Timed Automata. In Fränzle M, Kapur D, Zhan N, editors, Dependable Software Engineering: Theories, Tools, and Applications. Springer. 2016. p. 163-178. (Lecture Notes in Computer Science, Vol. 9984). https://doi.org/10.1007/978-3-319-47677-3_11