Active Model Learning of Stochastic Reactive Systems

Martin Tappler, Edi Muskardin, Bernhard K. Aichernig, Ingo Pill

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods - 19th International Conference, SEFM 2021, Proceedings
EditorsRadu Calinescu, Corina S. Pasareanu
PublisherSpringer
Pages481-500
Number of pages20
ISBN (Print)9783030921231
DOIs
Publication statusPublished - 2021
Event19th International Conference on Software Engineering and Formal Methods: SEFM 2021 - Virtual Online
Duration: 6 Dec 202110 Dec 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13085 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference19th International Conference on Software Engineering and Formal Methods
CityVirtual Online
Period6/12/2110/12/21

Keywords

  • Active automata learning
  • Markov decision processes
  • Model mining
  • Probabilistic verification
  • Stochastic mealy machines

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fields of Expertise

  • Information, Communication & Computing

Fingerprint

Dive into the research topics of 'Active Model Learning of Stochastic Reactive Systems'. Together they form a unique fingerprint.

Cite this