Active Learning of One-Clock Timed Automata using Constraint Solving

TL;DR

This paper presents a new active learning algorithm for deterministic one-clock timed automata that uses constraint solving to determine resets, enabling learning of larger models efficiently.

Contribution

It introduces a novel active learning algorithm that employs constraint solving for reset determination in one-clock timed automata and timed Mealy machines.

Findings

Applicable to larger models

Competitive with existing methods

Effective on practical case studies

Abstract

Active automata learning in the framework of Angluin's $L^*$ algorithm has been applied to learning many kinds of automata models. In applications to timed models such as timed automata, the main challenge is to determine guards on the clock value in transitions as well as which transitions reset the clock. In this paper, we introduce a new algorithm for active learning of deterministic one-clock timed automata and timed Mealy machines. The algorithm uses observation tables that do not commit to specific choices of reset, but instead rely on constraint solving to determine reset choices that satisfy readiness conditions. We evaluate our algorithm on randomly-generated examples as well as practical case studies, showing that it is applicable to larger models, and competitive with existing work for learning other forms of timed models.