TY - GEN

T1 - Learning Markov models for stationary system behaviors

AU - Chen, Yingke

AU - Mao, Hua

AU - Jaeger, Manfred

AU - Nielsen, Thomas Dyhre

AU - Guldstrand Larsen, Kim

AU - Nielsen, Brian

PY - 2012/3/27

Y1 - 2012/3/27

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 - Conference contribution

AN - SCOPUS:84859453785

SN - 9783642288906

T3 - Lecture Notes in Computer Science

SP - 216

EP - 230

BT - NASA Formal Methods

A2 - Goodloe, Alwyn E.

A2 - Person, Suzette

PB - Springer

CY - Berlin, Germany

T2 - 4th NASA Formal Methods Symposium, NFM 2012

Y2 - 3 April 2012 through 5 April 2012

ER -