Learning One-Clock Timed Automata
Jie An
1( , Mingshuai Chen
2,3,4 , Bohua Zhan
3,4 ,
Naijun Zhan
3,4( , and Miaomiao Zhang
1(
1 School of Software Engineering, Tongji University, Shanghai, China
{1510796,miaomiao}@tongji.edu.cn
2 Lehrstuhl f¨ ur Informatik 2, RWTH Aachen University, Aachen, Germany
chenms@cs.rwth-aachen.de
3 State Key Lab. of Computer Science, Institute of Software, CAS, Beijing, China
{bzhan,znj}@ios.ac.cn
4 University of Chinese Academy of Sciences, Beijing, China
Abstract. We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework of Angluin’s
L
∗ algorithm and inspired by existing work on the active learning of symbolic
automata. Due to the need of guessing for each transition whether it resets the
clock, the algorithm is of exponential complexity in the size of the learned automata. Before presenting this algorithm, we propose a simpler version where the
teacher is assumed to be smart in the sense of being able to provide the reset
information. We show that this simpler setting yields a polynomial complexity of
the learning process. Both of the algorithms are implemented and evaluated on
a collection of randomly generated examples. We furthermore demonstrate the
simpler algorithm on the functional specification of the TCP protocol.
Keywords: Automaton learning · Active learning · One-clock timed automata ·
Timed language · Reset-logical-timed language.
1 Introduction
In her seminal work [10], Angluin introduced the L
∗ algorithm for learning a regular language from queries and counterexamples within a query-answering framework.
The Angluin-style learning therefore is also termed active learning or query learning,
which is distinguished from passive learning, i.e., generating a model from a given data
set. Following this line of research, an increasing number of efficient active learning
methods (cf. [38]) have been proposed to learn, e.g., Mealy machines [34,30], I/O automata [2], register automata [25,1,15], nondeterministic finite automata [12], B¨ uchi
automata [19,28], symbolic automata [29,18,11] and Markov decision processes [36],
to name just a few. Full-fledged libraries, tools and applications are also available for
automata-learning tasks [13,27,20,21].
This work has been partially funded by NSFC under grant No. 61625206, 61972284, 61732001
and 61872341, by the ERC Advanced Project FRAPPANT under grant No. 787914, and by
the CAS Pioneer Hundred Talents Program under grant No. Y9RC585036.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 444–462, 2020.
https://doi.org/10.1007/978-3-030-45190-5 25
TACAS
Evaluation
Artifact
2020
Accepted
Jie An
1( , Mingshuai Chen
2,3,4 , Bohua Zhan
3,4 ,
Naijun Zhan
3,4( , and Miaomiao Zhang
1(
1 School of Software Engineering, Tongji University, Shanghai, China
{1510796,miaomiao}@tongji.edu.cn
2 Lehrstuhl f¨ ur Informatik 2, RWTH Aachen University, Aachen, Germany
chenms@cs.rwth-aachen.de
3 State Key Lab. of Computer Science, Institute of Software, CAS, Beijing, China
{bzhan,znj}@ios.ac.cn
4 University of Chinese Academy of Sciences, Beijing, China
Abstract. We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework of Angluin’s
L
∗ algorithm and inspired by existing work on the active learning of symbolic
automata. Due to the need of guessing for each transition whether it resets the
clock, the algorithm is of exponential complexity in the size of the learned automata. Before presenting this algorithm, we propose a simpler version where the
teacher is assumed to be smart in the sense of being able to provide the reset
information. We show that this simpler setting yields a polynomial complexity of
the learning process. Both of the algorithms are implemented and evaluated on
a collection of randomly generated examples. We furthermore demonstrate the
simpler algorithm on the functional specification of the TCP protocol.
Keywords: Automaton learning · Active learning · One-clock timed automata ·
Timed language · Reset-logical-timed language.
1 Introduction
In her seminal work [10], Angluin introduced the L
∗ algorithm for learning a regular language from queries and counterexamples within a query-answering framework.
The Angluin-style learning therefore is also termed active learning or query learning,
which is distinguished from passive learning, i.e., generating a model from a given data
set. Following this line of research, an increasing number of efficient active learning
methods (cf. [38]) have been proposed to learn, e.g., Mealy machines [34,30], I/O automata [2], register automata [25,1,15], nondeterministic finite automata [12], B¨ uchi
automata [19,28], symbolic automata [29,18,11] and Markov decision processes [36],
to name just a few. Full-fledged libraries, tools and applications are also available for
automata-learning tasks [13,27,20,21].
This work has been partially funded by NSFC under grant No. 61625206, 61972284, 61732001
and 61872341, by the ERC Advanced Project FRAPPANT under grant No. 787914, and by
the CAS Pioneer Hundred Talents Program under grant No. Y9RC585036.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 444–462, 2020.
https://doi.org/10.1007/978-3-030-45190-5 25
TACAS
Evaluation
Artifact
2020
Accepted