Learning One-Clock Timed Automata
449
for constructing a hypothesis, the learner makes membership queries as “Is the logicaltimed word γ in L(A)?”. If there does not exist a run ρ such that Γ (trace(ρ)) = γ,
meaning that there is some k such that the run is blocked after the k’th action (i.e.
γ is invalid) and hence the teacher gives a negative answer, associated with a resetlogical-timed word γ r where all b i ’s with i > k are set to ; If there exists a run ρ
(which is unique due to the determinacy of A) that admits γ (i.e., γ is valid), the teacher
answers “Yes”, if ρ is accepting, or “No” otherwise, while in both cases providing the
corresponding reset-logical-timed word γ r , with Π {1,2} γ r = γ.
For the sake of simplicity, we define a function π that maps a logical-timed word to
its unique reset-logical-timed counterpart in membership queries. Information gathered
from the membership queries is stored in a timed observation table defined as follows.
Definition 2 (Timed observation table). A timed observation table for a COTA A is a
7-tuple T = (Σ, Σ, Σ r , S, R, E, f) where Σ is the finite alphabet; Σ = Σ × R ≥0
is the infinite set of logical-timed actions; Σ r = Σ × R ≥0 × B is the infinite set of
reset-logical-timed actions; S, R ⊂ Σ
∗
r and E ⊂ Σ
∗ are finite sets of words, where S
is called the set of prefixes, R the boundary, and E the set of suffixes. Specifically,
– S and R are disjoint, i.e., S ∪ R = S R;
– The empty word is by default both a prefix and a suffix, i.e., ∈ E and ∈ S;
– f : (S ∪ R) · E → {−, +} is a classification function such that for a reset-logicaltimed word γ r , γ r ·e ∈ (S ∪R)·E, f (γ r ·e) = − if Π {1,2} γ r ·e is invalid, otherwise
if Π {1,2} γ r · e /
∈ L(A), f (γ r · e) = −, and f (γ r · e) = + if Π {1,2} γ r · e ∈ L(A).
Given a table T, we define row : S ∪ R → (E → {+, −}) as a function mapping
each γ r ∈ S ∪ R to a vector indexed by e ∈ E, each of whose components is defined
as f (γ r · e), denoting a potential location.
Before constructing a hypothesis H based on the timed observation table T, the
learner has to ensure that T satisfies the following conditions:
– Reduced: ∀s, s
∈ S : s = s
implies row (s) = row (s
);
– Closed: ∀r ∈ R, ∃s ∈ S : row (s) = row (r);
– Consistent: ∀γ r , γ r
∈ S ∪ R, row (γ r ) = row (γ r
) implies row (γ r · σ r ) =
row (γ r
· σ r
), for all σ r , σ r
∈ Σ r satisfying γ r · σ r , γ r
· σ r
∈ S ∪ R and
Π {1,2} σ r = Π {1,2} σ r
;
– Evidence-closed: ∀s ∈ S and ∀e ∈ E, the reset-logical-timed word π(Π {1,2} s · e)
belongs to S ∪ R;
– Prefix-closed: S ∪ R is prefix-closed.
A timed observation table T is prepared if it satisfies the above five conditions. To
get the table prepared, the learner can perform the following operations:
Making T closed. If T is not closed, there exists r ∈ R such that for all s ∈ S
row (r) = row (s). The learner thus can move such r from R to S. Moreover, each
reset-logical-timed word π(Π {1,2} r · σ) needs to be added to R, where σ = (σ, 0) for
all σ ∈ Σ. Such an operation is important since it guarantees that at every location all
actions in Σ are enabled, while specifying a clock valuation of these actions, despite
that some invalid logical-timed words might be involved. Particularly, giving a bottom
value 0 as the clock valuation satisfies the precondition of the partition functions that
will be described in Sect. 3.2.