Learning Markov models for stationary system behaviors

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

10 Citationer (Scopus)
286 Downloads (Pure)

Resumé

Establishing an accurate model for formal verification of an existing hardware or software system is often a manual process that is both time consuming and resource demanding. In order to ease the model construction phase,
methods have recently been proposed for automatically learning accurate system models from data in the form of observations of the target system. Common for these approaches is that they assume the data to consist of multiple independent observation sequences. However, for certain types of systems, in particular many running embedded systems, one would only have access to a single long observation sequence, and in these situations existing automatic learning methods cannot be applied. In this paper, we adapt algorithms for learning variable order Markov chains from a single observation sequence of a target system, so that stationary system properties can be verified using the learned model. Experiments demonstrate that system properties (formulated as stationary probabilities of LTL formulas) can be reliably identified using the learned model.
OriginalsprogEngelsk
TitelNASA Formal Methods : 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings
RedaktørerAlwyn E. Goodloe, Suzette Person
Antal sider15
ForlagSpringer
Publikationsdato2012
Sider216-230
ISBN (Trykt)978-3-642-28890-6
ISBN (Elektronisk)978-3-642-28891-3
DOI
StatusUdgivet - 2012
BegivenhedNASA Formal Methods Symposium - Norfolk, USA
Varighed: 3 apr. 20115 apr. 2012
Konferencens nummer: 4

Konference

KonferenceNASA Formal Methods Symposium
Nummer4
LandUSA
ByNorfolk
Periode03/04/201105/04/2012
NavnLecture Notes in Computer Science
Vol/bind7226
ISSN0302-9743

Fingerprint

Embedded systems
Markov processes
Learning systems
Hardware
Experiments
Formal verification

Citer dette

Chen, Y., Mao, H., Jaeger, M., Nielsen, T. D., Larsen, K. G., & Nielsen, B. (2012). Learning Markov models for stationary system behaviors. I A. E. Goodloe, & S. Person (red.), NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings (s. 216-230). Springer. Lecture Notes in Computer Science, Bind. 7226 https://doi.org/10.1007/978-3-642-28891-3_22
Chen, Yingke ; Mao, Hua ; Jaeger, Manfred ; Nielsen, Thomas Dyhre ; Larsen, Kim Guldstrand ; Nielsen, Brian. / Learning Markov models for stationary system behaviors. NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. red. / Alwyn E. Goodloe ; Suzette Person. Springer, 2012. s. 216-230 (Lecture Notes in Computer Science, Bind 7226).
@inproceedings{f4cf0f4bfcc74c70acd191c9db41c98b,
title = "Learning Markov models for stationary system behaviors",
abstract = "Establishing an accurate model for formal verification of an existing hardware or software system is often a manual process that is both time consuming and resource demanding. In order to ease the model construction phase, methods have recently been proposed for automatically learning accurate system models from data in the form of observations of the target system. Common for these approaches is that they assume the data to consist of multiple independent observation sequences. However, for certain types of systems, in particular many running embedded systems, one would only have access to a single long observation sequence, and in these situations existing automatic learning methods cannot be applied. In this paper, we adapt algorithms for learning variable order Markov chains from a single observation sequence of a target system, so that stationary system properties can be verified using the learned model. Experiments demonstrate that system properties (formulated as stationary probabilities of LTL formulas) can be reliably identified using the learned model.",
author = "Yingke Chen and Hua Mao and Manfred Jaeger and Nielsen, {Thomas Dyhre} and Larsen, {Kim Guldstrand} and Brian Nielsen",
year = "2012",
doi = "10.1007/978-3-642-28891-3_22",
language = "English",
isbn = "978-3-642-28890-6",
pages = "216--230",
editor = "Goodloe, {Alwyn E.} and Suzette Person",
booktitle = "NASA Formal Methods",
publisher = "Springer",
address = "Germany",

}

Chen, Y, Mao, H, Jaeger, M, Nielsen, TD, Larsen, KG & Nielsen, B 2012, Learning Markov models for stationary system behaviors. i AE Goodloe & S Person (red), NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. Springer, Lecture Notes in Computer Science, bind 7226, s. 216-230, Norfolk, USA, 03/04/2011. https://doi.org/10.1007/978-3-642-28891-3_22

Learning Markov models for stationary system behaviors. / Chen, Yingke; Mao, Hua; Jaeger, Manfred; Nielsen, Thomas Dyhre; Larsen, Kim Guldstrand; Nielsen, Brian.

NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. red. / Alwyn E. Goodloe; Suzette Person. Springer, 2012. s. 216-230 (Lecture Notes in Computer Science, Bind 7226).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

TY - GEN

T1 - Learning Markov models for stationary system behaviors

AU - Chen, Yingke

AU - Mao, Hua

AU - Jaeger, Manfred

AU - Nielsen, Thomas Dyhre

AU - Larsen, Kim Guldstrand

AU - Nielsen, Brian

PY - 2012

Y1 - 2012

N2 - Establishing an accurate model for formal verification of an existing hardware or software system is often a manual process that is both time consuming and resource demanding. In order to ease the model construction phase, methods have recently been proposed for automatically learning accurate system models from data in the form of observations of the target system. Common for these approaches is that they assume the data to consist of multiple independent observation sequences. However, for certain types of systems, in particular many running embedded systems, one would only have access to a single long observation sequence, and in these situations existing automatic learning methods cannot be applied. In this paper, we adapt algorithms for learning variable order Markov chains from a single observation sequence of a target system, so that stationary system properties can be verified using the learned model. Experiments demonstrate that system properties (formulated as stationary probabilities of LTL formulas) can be reliably identified using the learned model.

AB - Establishing an accurate model for formal verification of an existing hardware or software system is often a manual process that is both time consuming and resource demanding. In order to ease the model construction phase, methods have recently been proposed for automatically learning accurate system models from data in the form of observations of the target system. Common for these approaches is that they assume the data to consist of multiple independent observation sequences. However, for certain types of systems, in particular many running embedded systems, one would only have access to a single long observation sequence, and in these situations existing automatic learning methods cannot be applied. In this paper, we adapt algorithms for learning variable order Markov chains from a single observation sequence of a target system, so that stationary system properties can be verified using the learned model. Experiments demonstrate that system properties (formulated as stationary probabilities of LTL formulas) can be reliably identified using the learned model.

UR - http://www.scopus.com/inward/record.url?scp=84859453785&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-28891-3_22

DO - 10.1007/978-3-642-28891-3_22

M3 - Article in proceeding

SN - 978-3-642-28890-6

SP - 216

EP - 230

BT - NASA Formal Methods

A2 - Goodloe, Alwyn E.

A2 - Person, Suzette

PB - Springer

ER -

Chen Y, Mao H, Jaeger M, Nielsen TD, Larsen KG, Nielsen B. Learning Markov models for stationary system behaviors. I Goodloe AE, Person S, red., NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. Springer. 2012. s. 216-230. (Lecture Notes in Computer Science, Bind 7226). https://doi.org/10.1007/978-3-642-28891-3_22