Loading...
Please wait, while we are loading the content...
Similar Documents
Aalborg Universitet Learning Probabilistic Automata for Model Checking
| Content Provider | Semantic Scholar |
|---|---|
| Author | Chen, Yingke Jaeger, Manfred Nielsen, Thomas D. Larsen, K. J. Nielsen, Brian |
| Copyright Year | 2011 |
| 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 modeldriven development techniques and tools. In this paper we pu rsue an alternative approach where an accurate high-level model can be automatically constructed from observations of a giv en black-box embedded system. We adapt algorithms for learnin g finite probabilistic automata from observed system behavio rs. We prove that in the limit of large sample sizes the learned mode l will be an accurate representation of the data-generating s ystem. In particular, in the large sample limit, the learned model and the original system will define the same probabilities for li near temporal logic (LTL) properties. Thus, we can perform PLTL model-checking on the learned model to infer properties of t he system. We perform experiments learning models from system observations at different levels of abstraction. The exper imental results show the learned models provide very good approxima tions for relevant properties of the original system. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://vbn.aau.dk/files/60877200/qest11_final_version.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
