Active learning of one-clock timed automata using constraint solving
From MaRDI portal
Abstract: Active automata learning in the framework of Angluin's 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.
Recommendations
- Learning one-clock timed automata
- Learning deterministic one-clock timed automata via mutation testing
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Time to learn -- learning timed automata from tests
- One-Clock Deterministic Timed Automata Are Efficiently Identifiable in the Limit
Cites work
- A theory of timed automata
- Active learning of timed automata with unobservable resets
- Efficiently identifying deterministic real-time automata from labeled data
- Event-clock automata: a determinizable class of timed automata
- Inference of Event-Recording Automata Using Timed Decision Trees
- Learning Mealy machines with one timer
- Learning of event-recording automata
- Learning one-clock timed automata
- Learning regular sets from queries and counterexamples
- Learning symbolic automata
- Model learning as a satisfiability modulo theories problem
- One-Clock Deterministic Timed Automata Are Efficiently Identifiable in the Limit
- Real-time automata
- The efficiency of identifying timed automata and the power of clocks
- Time to learn -- learning timed automata from tests
Cited in
(11)- Model learning as a satisfiability modulo theories problem
- Time to learn -- learning timed automata from tests
- Learning one-clock timed automata
- Efficient learning of real time one-counter automata
- Learning deterministic one-clock timed automata via mutation testing
- A new approach for active automata learning based on apartness
- Learning realtime one-counter automata
- Active learning of deterministic timed automata with Myhill-Nerode style characterization
- Timed automata verification and synthesis via finite automata learning
- Learning deterministic multi-clock timed automata
- A Myhill-Nerode style characterization for timed automata with integer resets
This page was built for publication: Active learning of one-clock timed automata using constraint solving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6160915)
