Importance Sampling for Stochastic Timed Automata

Cyrille Jegourel; Kim Guldstrand Larsen; Axel Legay; Marius Mikučionis; Danny Bøgsted Poulsen; Sean Sedwards

doi:10.1007/978-3-319-47677-3_11

Importance Sampling for Stochastic Timed Automata

Cyrille Jegourel, Kim Guldstrand Larsen, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen, Sean Sedwards

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

8 Citations (Scopus)

362 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 language	English
Title of host publication	Dependable Software Engineering : Theories, Tools, and Applications
Editors	Martin Fränzle, Deepak Kapur, Naijin Zhan
Number of pages	16
Publisher	Springer
Publication date	2016
Pages	163-178
ISBN (Print)	978-3-319-47676-6
ISBN (Electronic)	978-3-319-47677-3
DOIs	https://doi.org/10.1007/978-3-319-47677-3_11
Publication status	Published - 2016
Event	Symposium on Dependable Software Engineering Theories, Tools and Applications - Beijing, China, Beijing, China Duration: 9 Nov 2016 → 10 Nov 2016 http://lcs.ios.ac.cn/setta/

Conference

Conference	Symposium on Dependable Software Engineering Theories, Tools and Applications
Location	Beijing, China
Country/Territory	China
City	Beijing
Period	09/11/2016 → 10/11/2016
Internet address	http://lcs.ios.ac.cn/setta/

Series	Lecture Notes in Computer Science
Volume	9984
ISSN	0302-9743

Keywords

importance sampling
rare events
stochastic timed automata
verification
model checking

Access to Document

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

reportOther version, 915 KB

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

@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{\v c}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",

note = "Symposium on Dependable Software Engineering Theories, Tools and Applications, SETTA ; Conference date: 09-11-2016 Through 10-11-2016",

url = "http://lcs.ios.ac.cn/setta/",

}

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 et al.
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 proceeding › Article in proceeding › Research › peer-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

T2 - Symposium on Dependable Software Engineering Theories, Tools and Applications

Y2 - 9 November 2016 through 10 November 2016

ER -

Importance Sampling for Stochastic Timed Automata

Abstract

Conference

Keywords

Access to Document

AUB Link

Other files and links

Fingerprint

DiCyPS: Center for Data-Intensive Cyber-Physical Systems

CASSTING: Collective Adaptive System SynThesIs using Non-zero-sum Games

SENSATION: Self Energy-Supporting Autonomous Computation

Cite this

Importance Sampling for Stochastic Timed Automata

Abstract

Conference

Keywords

Access to Document

AUB Link

Other files and links

Fingerprint

Projects

DiCyPS: Center for Data-Intensive Cyber-Physical Systems

CASSTING: Collective Adaptive System SynThesIs using Non-zero-sum Games

SENSATION: Self Energy-Supporting Autonomous Computation

Cite this