Learning Deterministic Probabilistic Automata from a Model Checking Perspective
Learning Deterministic Probabilistic Automata from a Model Checking Perspective
复制标题
从模型检查的角度学习确定性概率自动机
DOI：
10.1007/s10994-016-5565-9
复制
发表时间：
2016-11
期刊：
影响因子：
7.5
通讯作者：
Brian Nielsen
中科院分区：
文献类型：
--
作者：
Hua Mao;Yingke Chen;Manfred Jaeger;Thomas D. Nielsen;Kim G. Larsen;Brian Nielsen
Probabilistic automata models play an important role in the formal design and analysis of hard- and software systems. In this area of applications, one is often interested in formal model-checking procedures for verifying critical system properties. Since adequate system models are often difficult to design manually, we are interested in learning models from observed system behaviors. To this end we adopt techniques for learning finite probabilistic automata, notably theAlergiaalgorithm. In this paper we show how to extend the basic algorithm to also learn automata models for both reactive and timed systems. A key question of our investigation is to what extent one can expect a learned model to be a good approximation for the kind of probabilistic properties one wants to verify by model checking. We establish theoretical convergence properties for the learning algorithm as well as for probability estimates of system properties expressed in linear time temporal logic and linear continuous stochastic logic. We empirically compare the learning algorithm with statistical model checking and demonstrate the feasibility of the approach for practical system verification.
登录
查看更多内容
DOI：
10.1007/978-3-540-45257-7_12
发表时间：
2000-09
期刊：
--
影响因子：
--
作者：
C. D. L. Higuera;F. Thollard
通讯作者：
C. D. L. Higuera;F. Thollard
影响因子：
7.4
作者：
Baier, C;Haverkort, B;Katoen, JP
通讯作者：
Katoen, JP
DOI：
10.1007/3-540-48320-9_19
发表时间：
1999-08
期刊：
--
影响因子：
--
作者：
Josée Desharnais;Vineet Gupta;R. Jagadeesan;P. Panangaden
通讯作者：
Josée Desharnais;Vineet Gupta;R. Jagadeesan;P. Panangaden
DOI：
10.1007/3-540-47813-2
发表时间：
2002
期刊：
--
影响因子：
--
作者：
J. Leeuwen;J. Leeuwen
通讯作者：
J. Leeuwen;J. Leeuwen
DOI：
--
发表时间：
2008-04
期刊：
--
影响因子：
--
作者：
C. Baier;J. Katoen
通讯作者：
C. Baier;J. Katoen