@inproceedings{c0bb18d397ac4c2abe9384f62db4eea9,

title = "Learning probabilistic automata for model checking",

abstract = "Obtaining accurate system models for verification is a hard and time consuming process, which is seen by industry as a hindrance to adopt otherwise powerful model driven development techniques and tools. In this paper we pursue an alternative approach where an accurate high-level model can be automatically constructed from observations of a given black-box embedded system. We adapt algorithms for learning finite probabilistic automata from observed system behaviors. We prove that in the limit of large sample sizes the learned model will be an accurate representation of the data-generating system. In particular, in the large sample limit, the learned model and the original system will define the same probabilities for linear temporal logic (LTL) properties. Thus, we can perform PLTL model-checking on the learned model to infer properties of the system. We perform experiments learning models from system observations at different levels of abstraction. The experimental results show the learned models provide very good approximations for relevant properties of the original system.",

keywords = "Learning, Model Checking, Probabilistic Automata, Probabilistic Linear Time Temporal Logic",

author = "Hua Mao and Yingke Chen and Manfred Jaeger and Nielsen, {Thomas D.} and Larsen, {Kim G.} and Brian Nielsen",

year = "2011",

doi = "10.1109/QEST.2011.21",

language = "English",

isbn = "9780769544915",

series = "Proceedings of the 2011 8th International Conference on Quantitative Evaluation of Systems, QEST 2011",

pages = "111--120",

booktitle = "Proceedings of the 2011 8th International Conference on Quantitative Evaluation of Systems, QEST 2011",

note = "2011 8th International Conference on Quantitative Evaluation of Systems, QEST 2011 ; Conference date: 05-09-2011 Through 08-09-2011",

}