Learning One-Clock Timed Automata
459
Table 2: Experimental results on random examples for the normal teacher situation.
Case ID |Δ|mean
#Membership
#Equivalence
nmean tmean #Texplored #Learnt
Nmin Nmean Nmax Nmin Nmean Nmax
3 2 10
4.8
43 83.7 167
5 8.8 14
3.0 0.9
149.1
10/10
4 2 10
6.8
67 134.0 345
6 13.3 24
4.0 7.4
563.0
10/10
5 2 10
8.8
75 223.9 375
9 15.2 24
5.0 35.5 2811.6
10/10
6 2 10
11.9
73 348.3 708
10 16.7 30
5.6 59.8 5077.6
7/10
4 4 20
16.3 231 371.0 564
27 30.9 40
4.0 137.5 8590.0
6/10
#Membership & #Equivalence: the number of conducted membership and equivalence queries
with the cached methods, respectively. N min : the minimal, Nmean: the mean, Nmax: the maximum.
#T explored : the average number of the explored table instances.
#Learnt: the number of the learnt DOTAs in the group (learnt/total).
The alternative implementation and experimental results without the accelerating trick
can also be found in the tool page (under the dev branch).
Random examples for a normal teacher. Due to its high, exponential complexity, the
algorithm with a normal teacher failed (out of memory) in identifying DOTAs for almost all the above examples, except 6 cases out of the 10 in group 4 4 20. We therefore
randomly generated 40 extra DOTAs of smaller size classified into 4 groups. With the
accelerating trick, the learner need not guess the resets in elements of E for an entry
in S ∪ R if the querying result of the entry is the sink location. We also omitted the
checking of the evidence-closed condition, since it may add redundant rows in R, leading to more guesses and thereby a larger search space. The omission does not affect the
correctness of the learnt DOTAs. Moreover, as different table instances may generate
repeated queries, we cached the results of membership queries and counterexamples,
such that the numbers of membership and equivalence queries to the teacher can be
significantly reduced. Table 2 shows the performance of the algorithm in this setting.
Results without caching are available in the tool page (under the normal branch).
6 Conclusion
We have presented a polynomial active learning method for deterministic one-clock
timed automata from a smart teacher who can tell information about clock resets in
membership and equivalence queries. Our technique is based on converting the problem to that of learning reset-logical-timed languages. We then extend the method to
learning DOTAs from a normal teacher who receives delay-timed words for membership queries, while the learner guesses the reset information in the observation table.
We evaluate both algorithms on randomly generated examples and, for the former case,
the functional specification of the TCP protocol.
Moving forward, an extension of our active learning method to nondeterministic
OTAs and timed automata involving multiple clocks is of particular interest.
Data Availability Statement The datasets generated and/or analyzed during the current study
are available in the Figshare repository: https://doi.org/10.6084/m9.figshare.11545983.v3.
459
Table 2: Experimental results on random examples for the normal teacher situation.
Case ID |Δ|mean
#Membership
#Equivalence
nmean tmean #Texplored #Learnt
Nmin Nmean Nmax Nmin Nmean Nmax
3 2 10
4.8
43 83.7 167
5 8.8 14
3.0 0.9
149.1
10/10
4 2 10
6.8
67 134.0 345
6 13.3 24
4.0 7.4
563.0
10/10
5 2 10
8.8
75 223.9 375
9 15.2 24
5.0 35.5 2811.6
10/10
6 2 10
11.9
73 348.3 708
10 16.7 30
5.6 59.8 5077.6
7/10
4 4 20
16.3 231 371.0 564
27 30.9 40
4.0 137.5 8590.0
6/10
#Membership & #Equivalence: the number of conducted membership and equivalence queries
with the cached methods, respectively. N min : the minimal, Nmean: the mean, Nmax: the maximum.
#T explored : the average number of the explored table instances.
#Learnt: the number of the learnt DOTAs in the group (learnt/total).
The alternative implementation and experimental results without the accelerating trick
can also be found in the tool page (under the dev branch).
Random examples for a normal teacher. Due to its high, exponential complexity, the
algorithm with a normal teacher failed (out of memory) in identifying DOTAs for almost all the above examples, except 6 cases out of the 10 in group 4 4 20. We therefore
randomly generated 40 extra DOTAs of smaller size classified into 4 groups. With the
accelerating trick, the learner need not guess the resets in elements of E for an entry
in S ∪ R if the querying result of the entry is the sink location. We also omitted the
checking of the evidence-closed condition, since it may add redundant rows in R, leading to more guesses and thereby a larger search space. The omission does not affect the
correctness of the learnt DOTAs. Moreover, as different table instances may generate
repeated queries, we cached the results of membership queries and counterexamples,
such that the numbers of membership and equivalence queries to the teacher can be
significantly reduced. Table 2 shows the performance of the algorithm in this setting.
Results without caching are available in the tool page (under the normal branch).
6 Conclusion
We have presented a polynomial active learning method for deterministic one-clock
timed automata from a smart teacher who can tell information about clock resets in
membership and equivalence queries. Our technique is based on converting the problem to that of learning reset-logical-timed languages. We then extend the method to
learning DOTAs from a normal teacher who receives delay-timed words for membership queries, while the learner guesses the reset information in the observation table.
We evaluate both algorithms on randomly generated examples and, for the former case,
the functional specification of the TCP protocol.
Moving forward, an extension of our active learning method to nondeterministic
OTAs and timed automata involving multiple clocks is of particular interest.
Data Availability Statement The datasets generated and/or analyzed during the current study
are available in the Figshare repository: https://doi.org/10.6084/m9.figshare.11545983.v3.