TY - JOUR
T1 - Active model learning of stochastic reactive systems (extended version)
AU - Muškardin, Edi
AU - Tappler, Martin
AU - Aichernig, Bernhard K.
AU - Pill, Ingo
N1 - Publisher Copyright:
© The Author(s) 2024.
PY - 2024
Y1 - 2024
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 toward industrial applications. Most research, however, has been focusing on deterministic systems. In this article, 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. When compared with previous work, our evaluation demonstrates that the proposed optimizations and adaptations to stochastic Mealy machines can reduce learning costs by an order of magnitude while improving the accuracy of learned models.
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 toward industrial applications. Most research, however, has been focusing on deterministic systems. In this article, 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. When compared with previous work, our evaluation demonstrates that the proposed optimizations and adaptations to stochastic Mealy machines can reduce learning costs by an order of magnitude while improving the accuracy of learned models.
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=85188518785&partnerID=8YFLogxK
U2 - 10.1007/s10270-024-01158-0
DO - 10.1007/s10270-024-01158-0
M3 - Article
AN - SCOPUS:85188518785
SN - 1619-1366
JO - Software and Systems Modeling
JF - Software and Systems Modeling
ER -