Learning One-Clock Timed Automata
457
R which, when converted to a delay-timed word, agrees with a prefix of ω. The remainder of ω, however, needs to be converted to a reset-logical-timed word by guessing
reset information. The corresponding prefixes are then added to R. Hence, at most
2
|ω| unfilled table instances are generated. For each unfilled table instance, at most
2
(
e i ∈E\{ (|ei|−1))×|ω| filled tables are produced and inserted into ToExplore.
Throughout the learning process, the learner adds a finite number of table instances
to ToExplore at every iteration. Hence, the search tree is finite-branching. Moreover, if
all guesses are correct, the resulting table instance will be identical to the observation
table in the learning process with a smart teacher (apart from the guessing processes,
the basic table operations are the same as those in Section 3.1). This means, with an
appropriate search order, for example, taking the table instance that requires the least
number of guesses in ToExplore at every iteration, the algorithm terminates and returns the same table as in the learning process with a smart teacher, which is a COTA
that recognizes the target language L. In conformity to Theorem 1, the algorithm may
terminate even if the corresponding reset-logical-timed languages are not equivalent,
while yielding correct COTAs recognizing the same delay-timed language.
Theorem 6. Algorithm 2 terminates and returns a COTA H which recognizes the target
timed language L.
Complexity analysis. If T = (Σ, Σ, Σ r , S, R, E, f) is the final observation table for
the correct candidate COTA, the number of guessed resets in S ∪R is |S|+|R|, and the
number of guessed resets for entries in each row of the table is
ei∈E\{ (|e i | − 1).
Hence, the total number of guessed resets is (|S| + |R|) × (1 +
ei∈E\{ (|e i | − 1)).
Assuming an appropriate search order (for example according to the number of guesses
in each table), this yields the number of table instances considered before termination
as O(2
(|S|+|R|)×(1+
e i ∈E\{ (|ei|−1)) ).
5 Implementation and Experimental Results
To investigate the efficiency and scalability of the proposed methods, we implemented
a prototype
3 in PYTHON for learning deterministic one-clock timed automata. The examples include a practical case concerning the functional specification of the TCP protocol [26] and a set of randomly generated DOTAs to be learnt. All of the evaluations
have been carried out on a 3.6GHz Intel Core-i7 processor with 8GB RAM running
64-bit Ubuntu 16.04.
Functional specification of the TCP protocol. In [26], a state diagram on page 23 specifies state changes during a TCP connection triggered by causing events while leading
to resulting actions. As observed by Ouaknine and Worrell in [31], such a functional
specification of the protocol can be represented as a one-clock timed automaton. In our
setting, the corresponding DOTA A to be learnt is configured to have |Q| = 11 states
with the two CLOSED states collapsed, |Σ| = 10 after abstracting the causing events
and the resulting actions, |F | = 2, and |Δ| = 19 with appropriately specified timing
constraints including guards and resets. Using the algorithm with the smart teacher, a
3 Available at https://github.com/Leslieaj/OTALearning. The evaluated artifact is archived in [8].
457
R which, when converted to a delay-timed word, agrees with a prefix of ω. The remainder of ω, however, needs to be converted to a reset-logical-timed word by guessing
reset information. The corresponding prefixes are then added to R. Hence, at most
2
|ω| unfilled table instances are generated. For each unfilled table instance, at most
2
(
e i ∈E\{ (|ei|−1))×|ω| filled tables are produced and inserted into ToExplore.
Throughout the learning process, the learner adds a finite number of table instances
to ToExplore at every iteration. Hence, the search tree is finite-branching. Moreover, if
all guesses are correct, the resulting table instance will be identical to the observation
table in the learning process with a smart teacher (apart from the guessing processes,
the basic table operations are the same as those in Section 3.1). This means, with an
appropriate search order, for example, taking the table instance that requires the least
number of guesses in ToExplore at every iteration, the algorithm terminates and returns the same table as in the learning process with a smart teacher, which is a COTA
that recognizes the target language L. In conformity to Theorem 1, the algorithm may
terminate even if the corresponding reset-logical-timed languages are not equivalent,
while yielding correct COTAs recognizing the same delay-timed language.
Theorem 6. Algorithm 2 terminates and returns a COTA H which recognizes the target
timed language L.
Complexity analysis. If T = (Σ, Σ, Σ r , S, R, E, f) is the final observation table for
the correct candidate COTA, the number of guessed resets in S ∪R is |S|+|R|, and the
number of guessed resets for entries in each row of the table is
ei∈E\{ (|e i | − 1).
Hence, the total number of guessed resets is (|S| + |R|) × (1 +
ei∈E\{ (|e i | − 1)).
Assuming an appropriate search order (for example according to the number of guesses
in each table), this yields the number of table instances considered before termination
as O(2
(|S|+|R|)×(1+
e i ∈E\{ (|ei|−1)) ).
5 Implementation and Experimental Results
To investigate the efficiency and scalability of the proposed methods, we implemented
a prototype
3 in PYTHON for learning deterministic one-clock timed automata. The examples include a practical case concerning the functional specification of the TCP protocol [26] and a set of randomly generated DOTAs to be learnt. All of the evaluations
have been carried out on a 3.6GHz Intel Core-i7 processor with 8GB RAM running
64-bit Ubuntu 16.04.
Functional specification of the TCP protocol. In [26], a state diagram on page 23 specifies state changes during a TCP connection triggered by causing events while leading
to resulting actions. As observed by Ouaknine and Worrell in [31], such a functional
specification of the protocol can be represented as a one-clock timed automaton. In our
setting, the corresponding DOTA A to be learnt is configured to have |Q| = 11 states
with the two CLOSED states collapsed, |Σ| = 10 after abstracting the causing events
and the resulting actions, |F | = 2, and |Δ| = 19 with appropriately specified timing
constraints including guards and resets. Using the algorithm with the smart teacher, a
3 Available at https://github.com/Leslieaj/OTALearning. The evaluated artifact is archived in [8].