Timed Automata Learning via SMT Solving

Martin Tappler*, Bernhard K. Aichernig, Florian Lorber

*Corresponding author for this work

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


Automata learning is a technique for automatically inferring models of existing systems, that enables formal verification of black-box systems. In this paper we propose a way of learning timed automata, extended final state machines that can measure the progress of time. We make use of SMT solving to learn timed automata consistent with the observations in a set of timed traces, which can be gathered via active testing or passive monitoring. By imposing a set of restrictions to the learnt models, we ensure that our solutions are not overly general. The presented SMT encoding of the problem allows for two ways of incremental solving and different search orders. We present a prototype implementation with results from case studies and randomly generated timed automata of varying size and complexity. We perform an extensive evaluation over six SMT solvers, using different theories and exploration strategies, as well as incremental and non-incremental solving.

Original languageEnglish
Title of host publicationNASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings
EditorsJyotirmoy V. Deshmukh, Klaus Havelund, Ivan Perez
PublisherSpringer Science and Business Media Deutschland GmbH
Number of pages19
ISBN (Print)9783031067723
Publication statusPublished - 2022
Event14th International Symposium on NASA Formal Methods: NFM 2022 - Caltech, Pasadena, United States
Duration: 24 May 202227 May 2022

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference14th International Symposium on NASA Formal Methods
Abbreviated titleNFM 2022
Country/TerritoryUnited States

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Timed Automata Learning via SMT Solving'. Together they form a unique fingerprint.

Cite this