446
J. An et al.
information on transitions discovered in the observation table. Due to these guesses,
the latter algorithm features exponential complexity in the size of the learned automata.
The proposed learning methods are implemented and evaluated on randomly generated
examples. We also demonstrate the simpler, polynomial algorithm on a practical case
study concerning the functional specification of the TCP protocol. Detailed proofs for
theorems and lemmas in this paper can be found in Appendix A of the full version [7].
In what follows, Sect. 2 provides preliminary definitions on one-clock timed automata. The learning algorithm with a smart teacher is presented and analyzed in Sect. 3.
We then present the situation with a normal teacher in Sect. 4. The experimental results
are reported in Sect. 5. Finally, Sect. 6 concludes this paper.
2 Preliminaries
Let R ≥0 and N be the set of non-negative reals and natural numbers, respectively, and B
the Boolean set. We use to stand for true and ⊥ for false. The projection of an n-tuple
x onto its first two components is denoted by Π {1,2} x, which extends to a sequence of
tuples as Π {1,2} (x 1 , . . . , x k ) =
Π {1,2} x 1 , . . . , Π {1,2} x k
.
Timed automata [4], a kind of finite automata extended with a finite set of realvalued clocks, are widely used to model real-time systems. In this paper, we consider
a subclass of timed automata with a single clock, termed one-clock timed automata
(OTAs). Let c be the clock variable, denote by Φ c the set of clock constraints of the
form φ ::= | c cc m | φ ∧ φ, where m ∈ N and ∈ {=, <, >, ≤, ≥}.
Definition 1 (One-clock timed automata). A one-clock timed automaton A = (Σ, Q,
q 0 , F, c, Δ), where Σ is a finite set of actions, called the alphabet; Q is a finite set of
locations; q 0 ∈ Q is the initial location; F ⊆ Q is a set of accepting locations; c is the
unique clock; and Δ ⊆ Q × Σ × Φ c × B × Q is a finite set of transitions.
A transition δ = (q, σ, φ, b, q
) allows a jump from the source location q to the
target location q
by performing the action σ ∈ Σ if the constraint φ ∈ Φ c is satisfied.
Meanwhile, clock c is reset to zero if b = , and remains unchanged otherwise.
A clock valuation is a function ν : c → R ≥0 that assigns a non-negative real number
to the clock. For t ∈ R ≥0 , let ν + t be the clock valuation with (ν + t)(c) = ν(c) + t.
According to the definitions of clock valuation and clock constraint, a transition guard
can be represented as an interval whose endpoints are in N∪{∞}. For example, φ 1 : c <
5 ∧ c ≥ 3 is represented as [3, 5), φ 2 : c = 6 as [6, 6], and φ 3 : as [0, ∞). We will use
the inequality- and interval-representation interchangeably in this paper.
A state s of A is a pair (q, ν), where q ∈ Q and ν is a clock valuation. A run
ρ of A is a finite sequence ρ = (q 0 , ν 0 )
t1,σ1
− −− → (q 1 , ν 1 )
t2,σ2
− −− → · · ·
tn,σn
−−−→ (q n , ν n ),
where ν 0 (c) = 0, t i ∈ R ≥0 stands for the time delay spending on q i−1 before δ i =
(q i−1 , σ i , φ i , b i , q i ) ∈ Δ is taken, only if (1) ν i−1 +t i satisfies φ i , (2) ν i (c) = ν i−1 (c)+
t i if b i = ⊥, otherwise ν i (c) = 0, for all 1 ≤ i ≤ n. A run ρ is accepting if q n ∈ F .
The trace of a run ρ is a timed word, denoted by trace(ρ). trace(ρ) = if ρ =
(q 0 , ν 0 ), and trace(ρ) = (σ 1 , t 1 )(σ 2 , t 2 ) · · · (σ n , t n ) if ρ = (q 0 , ν 0 )
t1,σ1
− −− → (q 1 , ν 1 )
t2,σ2
− −− →
· · ·
tn,σn
−−−→ (q n , ν n ). Since t i is the time delay on q i−1 , for 1 ≤ i ≤ n, such a timed
J. An et al.
information on transitions discovered in the observation table. Due to these guesses,
the latter algorithm features exponential complexity in the size of the learned automata.
The proposed learning methods are implemented and evaluated on randomly generated
examples. We also demonstrate the simpler, polynomial algorithm on a practical case
study concerning the functional specification of the TCP protocol. Detailed proofs for
theorems and lemmas in this paper can be found in Appendix A of the full version [7].
In what follows, Sect. 2 provides preliminary definitions on one-clock timed automata. The learning algorithm with a smart teacher is presented and analyzed in Sect. 3.
We then present the situation with a normal teacher in Sect. 4. The experimental results
are reported in Sect. 5. Finally, Sect. 6 concludes this paper.
2 Preliminaries
Let R ≥0 and N be the set of non-negative reals and natural numbers, respectively, and B
the Boolean set. We use to stand for true and ⊥ for false. The projection of an n-tuple
x onto its first two components is denoted by Π {1,2} x, which extends to a sequence of
tuples as Π {1,2} (x 1 , . . . , x k ) =
Π {1,2} x 1 , . . . , Π {1,2} x k
.
Timed automata [4], a kind of finite automata extended with a finite set of realvalued clocks, are widely used to model real-time systems. In this paper, we consider
a subclass of timed automata with a single clock, termed one-clock timed automata
(OTAs). Let c be the clock variable, denote by Φ c the set of clock constraints of the
form φ ::= | c cc m | φ ∧ φ, where m ∈ N and ∈ {=, <, >, ≤, ≥}.
Definition 1 (One-clock timed automata). A one-clock timed automaton A = (Σ, Q,
q 0 , F, c, Δ), where Σ is a finite set of actions, called the alphabet; Q is a finite set of
locations; q 0 ∈ Q is the initial location; F ⊆ Q is a set of accepting locations; c is the
unique clock; and Δ ⊆ Q × Σ × Φ c × B × Q is a finite set of transitions.
A transition δ = (q, σ, φ, b, q
) allows a jump from the source location q to the
target location q
by performing the action σ ∈ Σ if the constraint φ ∈ Φ c is satisfied.
Meanwhile, clock c is reset to zero if b = , and remains unchanged otherwise.
A clock valuation is a function ν : c → R ≥0 that assigns a non-negative real number
to the clock. For t ∈ R ≥0 , let ν + t be the clock valuation with (ν + t)(c) = ν(c) + t.
According to the definitions of clock valuation and clock constraint, a transition guard
can be represented as an interval whose endpoints are in N∪{∞}. For example, φ 1 : c <
5 ∧ c ≥ 3 is represented as [3, 5), φ 2 : c = 6 as [6, 6], and φ 3 : as [0, ∞). We will use
the inequality- and interval-representation interchangeably in this paper.
A state s of A is a pair (q, ν), where q ∈ Q and ν is a clock valuation. A run
ρ of A is a finite sequence ρ = (q 0 , ν 0 )
t1,σ1
− −− → (q 1 , ν 1 )
t2,σ2
− −− → · · ·
tn,σn
−−−→ (q n , ν n ),
where ν 0 (c) = 0, t i ∈ R ≥0 stands for the time delay spending on q i−1 before δ i =
(q i−1 , σ i , φ i , b i , q i ) ∈ Δ is taken, only if (1) ν i−1 +t i satisfies φ i , (2) ν i (c) = ν i−1 (c)+
t i if b i = ⊥, otherwise ν i (c) = 0, for all 1 ≤ i ≤ n. A run ρ is accepting if q n ∈ F .
The trace of a run ρ is a timed word, denoted by trace(ρ). trace(ρ) = if ρ =
(q 0 , ν 0 ), and trace(ρ) = (σ 1 , t 1 )(σ 2 , t 2 ) · · · (σ n , t n ) if ρ = (q 0 , ν 0 )
t1,σ1
− −− → (q 1 , ν 1 )
t2,σ2
− −− →
· · ·
tn,σn
−−−→ (q n , ν n ). Since t i is the time delay on q i−1 , for 1 ≤ i ≤ n, such a timed