Learning Mealy machines with local timers

Complex real-time systems, including autonomous vehicles, advanced robots, and smart power systems, are set to transform every aspect of daily life. To deploy these systems safely, it is essential to ensure that they behave correctly. However, understanding and verifying their behavior often requires accurate and up-to-date behavioral models, which are not available for many applications. Active automata learning could close this gap, as it enables the automated inference of automaton models through interactions with a black-box system. Yet existing active learning methods for real-time systems often struggle to learn models in reasonable time. This thesis introduces a new method for the efficient active learning of automata from real-time systems. Our method is based on Mealy machines with local timers (MMLTs), a new model class that extends standard Mealy machines with multiple timers. We design MMLTs to be learned efficiently while being sufficiently expressive to model applications from different domains. We present an active learning algorithm for MMLTs and extend it with imprecise symbol filtering, an optimization that leverages fallible prior knowledge of transitions without an effect to reduce runtime. Most critically, our method learns accurate models even if the supplied knowledge is incorrect. We further reduce runtime through two MMLT-specific optimizations for behavioral equivalence testing, a frequent bottleneck in active automata learning. We formally prove the correctness of our method and evaluate its performance across 11 cases studies, ranging from network protocols to automotive systems. Our results show that our method drastically outperforms the state of the art across all models. Furthermore, our optimizations often enable significant runtime reductions. We thereby take active automata learning for real-time systems a significant step closer to an application in practice, and thus help easing the access to up-to-date models for the safe deployment of current and future real-time systems.

Author dc:creator

• Kogel, Paul Werner

Advisor dc:contributor.advisor

• Glesner, Sabine

Licence dc:rights.uri

• https://creativecommons.org/licenses/by/4.0/

Language dc:language.iso

en

Identifier URI

https://doi.org/10.14279/depositonce-24731

OAI identifier oai:identifier

oai:depositonce.tu-berlin.de:11303/25906