Learning Deterministic Multi-Clock Timed Automata
Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要