Learning One-Clock Timed Automata
445
For real-time systems where timing constraints play a key role, however, learning
a formal model is much more complicated. As a classical model for real-time systems,
timed automata [4] have an infinite set of timed actions. This yields a fundamental
difference to finite automata featuring finite alphabets. Moreover, it is difficult to detect
resets of clock variables from observable behaviors of the system. This makes learning
formal models of timed systems a challenging yet interesting problem.
Various attempts have been carried out in the literature on learning timed models,
which can be classified into two tracks. The first track pursues active learning methods,
e.g. [22] for learning event-recording automata (ERA) [5] and [9] for learning real-time
automata (RTA) [17]. ERA are time automata where, for every untimed action a, a clock
is used to record the time of the last occurrence of a. The underlying learning algorithm
[22], however, is prohibitively complex due to too many degrees of freedom and multiple clocks for recording events. RTA are a class of special timed automata with one
clock to record the execution time of each action by resetting at the starting. The other
track pursues passive learning. In [42,41], an algorithm was proposed to learn deterministic RTA. The basic idea is that the learner organizes a tree sketching traces of the data
set while merging nodes of the tree following a certain heuristic function. A passive
learning algorithm for timed automata with one clock was further proposed in [39,40].
A common weakness of passive learning methods is that the generated model merely
accepts all positive traces while it rejects all negative ones for the given set of traces,
without guaranteeing that it is a correct model of the target system. A theoretical result
was established in [40] showing it is possible to obtain the target system by continuously enriching the data set, however the number of iterations is unknown. In addition,
the passive learning methods cited above concern only discrete-time semantics of the
underlying timed models, i.e., the clock takes values from non-negative integers. We
furthermore refer the readers to [14,32] for learning specialized forms of practical timed
systems in a passive manner, [37] for passively learning timed automata using genetic
programming which scales to automata of large sizes, [33] for learning probabilistic
real-time automata incorporating clustering techniques in machine learning, and [36]
for L ∗ -based learning of Markov decision processes with testing and sampling.
In this paper, we present the first active learning method for deterministic one-clock
timed automata (DOTAs) under continuous-time semantics
1 . Such timed automata provide simple models while preserving adequate expressiveness, and therefore have been
widely used in practical real-time systems [35,3,16]. We present our approach in two
steps. First, we describe a simpler algorithm, under the assumption that the teacher is
smart in the sense of being able to provide information about clock resets in membership and equivalence queries. The basic idea is as follows. We define the reset-logicaltimed language of a DOTA and show that the timed languages of two DOTAs are equivalent if their reset-logical-timed languages are equivalent, which reduces the learning
problem to that of learning a reset-logical-timed language.Then we show how to learn
the reset-logical-timed language following Maler and D’Antoni’s learning algorithms
for symbolic automata [29,18]. We claim the correctness, termination and polynomial
complexity of this learning algorithm. Next, we extend this algorithm to the case of a
normal teacher. The main difference is that the learner now needs to guess the reset
1 The proposed learning method applies trivially to discrete-time semantics too.
445
For real-time systems where timing constraints play a key role, however, learning
a formal model is much more complicated. As a classical model for real-time systems,
timed automata [4] have an infinite set of timed actions. This yields a fundamental
difference to finite automata featuring finite alphabets. Moreover, it is difficult to detect
resets of clock variables from observable behaviors of the system. This makes learning
formal models of timed systems a challenging yet interesting problem.
Various attempts have been carried out in the literature on learning timed models,
which can be classified into two tracks. The first track pursues active learning methods,
e.g. [22] for learning event-recording automata (ERA) [5] and [9] for learning real-time
automata (RTA) [17]. ERA are time automata where, for every untimed action a, a clock
is used to record the time of the last occurrence of a. The underlying learning algorithm
[22], however, is prohibitively complex due to too many degrees of freedom and multiple clocks for recording events. RTA are a class of special timed automata with one
clock to record the execution time of each action by resetting at the starting. The other
track pursues passive learning. In [42,41], an algorithm was proposed to learn deterministic RTA. The basic idea is that the learner organizes a tree sketching traces of the data
set while merging nodes of the tree following a certain heuristic function. A passive
learning algorithm for timed automata with one clock was further proposed in [39,40].
A common weakness of passive learning methods is that the generated model merely
accepts all positive traces while it rejects all negative ones for the given set of traces,
without guaranteeing that it is a correct model of the target system. A theoretical result
was established in [40] showing it is possible to obtain the target system by continuously enriching the data set, however the number of iterations is unknown. In addition,
the passive learning methods cited above concern only discrete-time semantics of the
underlying timed models, i.e., the clock takes values from non-negative integers. We
furthermore refer the readers to [14,32] for learning specialized forms of practical timed
systems in a passive manner, [37] for passively learning timed automata using genetic
programming which scales to automata of large sizes, [33] for learning probabilistic
real-time automata incorporating clustering techniques in machine learning, and [36]
for L ∗ -based learning of Markov decision processes with testing and sampling.
In this paper, we present the first active learning method for deterministic one-clock
timed automata (DOTAs) under continuous-time semantics
1 . Such timed automata provide simple models while preserving adequate expressiveness, and therefore have been
widely used in practical real-time systems [35,3,16]. We present our approach in two
steps. First, we describe a simpler algorithm, under the assumption that the teacher is
smart in the sense of being able to provide information about clock resets in membership and equivalence queries. The basic idea is as follows. We define the reset-logicaltimed language of a DOTA and show that the timed languages of two DOTAs are equivalent if their reset-logical-timed languages are equivalent, which reduces the learning
problem to that of learning a reset-logical-timed language.Then we show how to learn
the reset-logical-timed language following Maler and D’Antoni’s learning algorithms
for symbolic automata [29,18]. We claim the correctness, termination and polynomial
complexity of this learning algorithm. Next, we extend this algorithm to the case of a
normal teacher. The main difference is that the learner now needs to guess the reset
1 The proposed learning method applies trivially to discrete-time semantics too.