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

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

11 Citationer (Scopus)

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

Originalsprog	Engelsk
Titel	Dependable Software Engineering : Theories, Tools, and Applications
Redaktører	Martin Fränzle, Deepak Kapur, Naijin Zhan
Antal sider	16
Forlag	Springer
Publikationsdato	2016
Sider	163-178
ISBN (Trykt)	978-3-319-47676-6
ISBN (Elektronisk)	978-3-319-47677-3
DOI	https://doi.org/10.1007/978-3-319-47677-3_11
Status	Udgivet - 2016
Begivenhed	Symposium on Dependable Software Engineering Theories, Tools and Applications - Beijing, China, Beijing, Kina Varighed: 9 nov. 2016 → 10 nov. 2016 http://lcs.ios.ac.cn/setta/

Konference

Konference	Symposium on Dependable Software Engineering Theories, Tools and Applications
Lokation	Beijing, China
Land/Område	Kina
By	Beijing
Periode	09/11/2016 → 10/11/2016
Internetadresse	http://lcs.ios.ac.cn/setta/

Navn	Lecture Notes in Computer Science
Vol/bind	9984
ISSN	0302-9743

Adgang til dokumentet

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

reportAnden version, 915 KB

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Andre filer og links

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

DiCyPS: Center for Data-Intensive Cyber-Physical Systems
Larsen, K. G. (PI (principal investigator)), Skou, A. (CoI (co-investigator)), Pedersen, T. B. (CoI (co-investigator)), Jensen, C. S. (CoI (co-investigator)), Kjeldskov, J. (CoI (co-investigator)), Skov, M. B. (CoI (co-investigator)), Nielsen, B. (CoI (co-investigator)), Lahrmann, H. (CoI (co-investigator)), Bak-Jensen, B. (CoI (co-investigator)), Guerrero, J. M. (CoI (co-investigator)) & Raptis, D. (Projektdeltager)
Innovationsfonden
01/01/2015 → 31/12/2020
Projekter: Projekt › Forskning
CASSTING: Collective Adaptive System SynThesIs using Non-zero-sum Games
Larsen, K. G. (Projektleder), Skou, A. (Projektdeltager), David, A. (Projektdeltager) & Srba, J. (Projektdeltager)
FP7 STREP
01/04/2013 → 31/03/2016
Projekter: Projekt › Forskning
SENSATION: Self Energy-Supporting Autonomous Computation
Larsen, K. G. (Projektleder), Hansen, R. R. (Projektdeltager), Koch, P. (Projektdeltager), Nielsen, B. (Projektdeltager) & Skou, A. (Projektdeltager)
FP7 FET Proactive
01/10/2012 → 30/09/2015
Projekter: Projekt › Forskning

Citationsformater

@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. i M Fränzle, D Kapur & N Zhan (red), Dependable Software Engineering: Theories, Tools, and Applications. Springer, Lecture Notes in Computer Science, bind 9984, s. 163-178, Symposium on Dependable Software Engineering Theories, Tools and Applications, Beijing, Kina, 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. red. / Martin Fränzle; Deepak Kapur; Naijin Zhan. Springer, 2016. s. 163-178 (Lecture Notes in Computer Science, Bind 9984).

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › 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

Konference

Adgang til dokumentet

AUB Link

Andre filer og links

Fingeraftryk

Projekter

DiCyPS: Center for Data-Intensive Cyber-Physical Systems

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

SENSATION: Self Energy-Supporting Autonomous Computation

Citationsformater