TY - GEN
T1 - Active Model Learning of Stochastic Reactive Systems
AU - Tappler, Martin
AU - Muskardin, Edi
AU - Aichernig, Bernhard K.
AU - Pill, Ingo
N1 - DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.
PY - 2021
Y1 - 2021
N2 - Black-box systems are inherently hard to verify. Many verification techniques, like model checking, require formal models as a basis. However, such models often do not exist, or they might be outdated. Active automata learning helps to address this issue by offering to automatically infer formal models from system interactions. Hence, automata learning has been receiving much attention in the verification community in recent years. This led to various efficiency improvements, paving the way towards industrial applications. Most research, however, has been focusing on deterministic systems. Here, we present an approach to efficiently learn models of stochastic reactive systems. Our approach adapts L
∗ -based learning for Markov decision processes, which we improve and extend to stochastic Mealy machines. Our evaluation demonstrates that we can reduce learning costs by a factor of up to 8.7 in comparison to previous work.
AB - Black-box systems are inherently hard to verify. Many verification techniques, like model checking, require formal models as a basis. However, such models often do not exist, or they might be outdated. Active automata learning helps to address this issue by offering to automatically infer formal models from system interactions. Hence, automata learning has been receiving much attention in the verification community in recent years. This led to various efficiency improvements, paving the way towards industrial applications. Most research, however, has been focusing on deterministic systems. Here, we present an approach to efficiently learn models of stochastic reactive systems. Our approach adapts L
∗ -based learning for Markov decision processes, which we improve and extend to stochastic Mealy machines. Our evaluation demonstrates that we can reduce learning costs by a factor of up to 8.7 in comparison to previous work.
KW - Active automata learning
KW - Markov decision processes
KW - Model mining
KW - Probabilistic verification
KW - Stochastic mealy machines
UR - http://www.scopus.com/inward/record.url?scp=85121907031&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-92124-8_27
DO - 10.1007/978-3-030-92124-8_27
M3 - Conference paper
SN - 9783030921231
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 481
EP - 500
BT - Software Engineering and Formal Methods - 19th International Conference, SEFM 2021, Proceedings
A2 - Calinescu, Radu
A2 - Pasareanu, Corina S.
PB - Springer
T2 - 19th International Conference on Software Engineering and Formal Methods
Y2 - 6 December 2021 through 10 December 2021
ER -