Learning Deterministic Multi-Clock Timed Automata
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916251010334720 |
|---|---|
| author | Teng, Yu Zhang, Miaomiao An, Jie |
| author_facet | Teng, Yu Zhang, Miaomiao An, Jie |
| contents | We present an algorithm for active learning of deterministic timed automata with multiple clocks. The algorithm is within the querying framework of Angluin's $L^*$ algorithm and follows the idea proposed in existing work on the active learning of deterministic one-clock timed automata. We introduce an equivalence relation over the reset-clocked language of a timed automaton and then transform the learning problem into learning the corresponding reset-clocked language of the target automaton. Since a reset-clocked language includes the clock reset information which is not observable, we first present the approach of learning from a powerful teacher who can provide reset information by answering reset information queries from the learner. Then we extend the algorithm in a normal teacher situation in which the learner can only ask standard membership query and equivalence query while the learner guesses the reset information. We prove that the learning algorithm terminates and returns a correct deterministic timed automaton. Due to the need of guessing whether the clocks reset at the transitions, the algorithm is of exponential complexity in the size of the target automaton. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_07823 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Learning Deterministic Multi-Clock Timed Automata Teng, Yu Zhang, Miaomiao An, Jie Formal Languages and Automata Theory We present an algorithm for active learning of deterministic timed automata with multiple clocks. The algorithm is within the querying framework of Angluin's $L^*$ algorithm and follows the idea proposed in existing work on the active learning of deterministic one-clock timed automata. We introduce an equivalence relation over the reset-clocked language of a timed automaton and then transform the learning problem into learning the corresponding reset-clocked language of the target automaton. Since a reset-clocked language includes the clock reset information which is not observable, we first present the approach of learning from a powerful teacher who can provide reset information by answering reset information queries from the learner. Then we extend the algorithm in a normal teacher situation in which the learner can only ask standard membership query and equivalence query while the learner guesses the reset information. We prove that the learning algorithm terminates and returns a correct deterministic timed automaton. Due to the need of guessing whether the clocks reset at the transitions, the algorithm is of exponential complexity in the size of the target automaton. |
| title | Learning Deterministic Multi-Clock Timed Automata |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2404.07823 |