450
J. An et al.
Making T consistent. If T is not consistent, one inconsistency is resolved by adding
σ · e to E, where σ and e can be determined as follows. T being inconsistent implies
that there exist two reset-logical-timed words γ r , γ r
∈ S ∪ R at least, such that γ r ·
σ r , γ r
· σ r
∈ S ∪ R and Π {1,2} σ r = Π {1,2} σ r
for some σ r , σ r
∈ Σ r , with
row (γ r ) = row (γ r
) but row (γ r · σ r ) = row (γ r
· σ r
). So, let σ = Π {1,2} σ r =
Π {1,2} σ r
and e ∈ E such that f (γ r σ r · e) = f (γ r
σ r
· e). Thereafter, the learner
fills the table by making membership queries. Note that this operation keeps the set E
of suffixes being a set of logical-timed words.
Making T evidence-closed. If T is not evidence-closed, then the learner needs to add
all prefixes of π(Π {1,2} s · e) to R for every s ∈ S and e ∈ E, except those already in
S ∪ R. Similarly, the learner needs to fill the table through membership queries.
The condition that a timed observation table T is reduced and prefix-closed is inherently preserved by the aforementioned operations, together with the counterexample
processing described later in Sect. 3.3. Furthermore, a table may need several rounds of
these operations before being prepared (cf. Algorithm 1), since certain conditions may
be violated by different, interleaved operations.
3.2 Hypothesis construction
As soon as the timed observation table T is prepared, a hypothesis can be constructed
in two steps, i.e., the learner first builds a DFA M based on the information in T, and
then transforms M to a hypothesis H, which will later be shown as a COTA.
Given a prepared timed observation table T = (Σ, Σ, Σ r , S, R, E, f), a DFA
M = (Q M , Σ M , Δ M , q
0
M , F M ) can be built as follows:
– the finite set of locations Q M = {q row (s) | s ∈ S};
– the initial location q
0
M = q row () for ∈ S;
– the set of accepting locations F M = {q row (s) | f (s · ) = + for s ∈ S and ∈ E};
– the finite alphabet Σ M = {σ r ∈ Σ r | γ r · σ r ∈ S ∪ R for γ r ∈ Σ
∗
r };
– the finite set of transitions Δ M = {(q row (γr) , σ r , q row (γr·σr) ) | γ r · σ r ∈ S ∪
R for γ r ∈ Σ
∗
r and σ r ∈ Σ r }.
The constructed DFA M is compatible with the timed observation table T in the
sense captured by the following lemma.
Lemma 1. For a prepared timed observation table T = (Σ, Σ, Σ r , S, R, E, f), for
every γ r ·e ∈ (S ∪R)·E, the constructed DFA M = (Q M , Σ M , Δ M , q
0
M , F M ) accepts
π(Π {1,2} γ r · e) if and only if f (γ r · e) = +.
The learner then transforms the DFA M to a hypothesis H = (Σ, Q, q 0 , F, c, Δ),
with Q = Q M , q 0 = q
0
M , F = F M , c being the clock and Σ the given alphabet as in T.
The set of transitions Δ in H can be constructed as follows: For any q ∈ Q M and σ ∈
Σ, let Ψ q,σ = {μ | (q, (σ, μ, b), q
) ∈ Δ M }, then applying the partition function P
c
(·)
(defined below) to Ψ q,σ returns k intervals, written as I 1 , · · · , I k , satisfying μ i ∈ I i for
any 1 ≤ i ≤ k, where k = |Ψ q,σ |; consequently, for every (q, (σ, μ i , b i ), q
) ∈ Δ M , a
fresh transition δ i = (q, σ, I i , b i , q
) is added to Δ.
J. An et al.
Making T consistent. If T is not consistent, one inconsistency is resolved by adding
σ · e to E, where σ and e can be determined as follows. T being inconsistent implies
that there exist two reset-logical-timed words γ r , γ r
∈ S ∪ R at least, such that γ r ·
σ r , γ r
· σ r
∈ S ∪ R and Π {1,2} σ r = Π {1,2} σ r
for some σ r , σ r
∈ Σ r , with
row (γ r ) = row (γ r
) but row (γ r · σ r ) = row (γ r
· σ r
). So, let σ = Π {1,2} σ r =
Π {1,2} σ r
and e ∈ E such that f (γ r σ r · e) = f (γ r
σ r
· e). Thereafter, the learner
fills the table by making membership queries. Note that this operation keeps the set E
of suffixes being a set of logical-timed words.
Making T evidence-closed. If T is not evidence-closed, then the learner needs to add
all prefixes of π(Π {1,2} s · e) to R for every s ∈ S and e ∈ E, except those already in
S ∪ R. Similarly, the learner needs to fill the table through membership queries.
The condition that a timed observation table T is reduced and prefix-closed is inherently preserved by the aforementioned operations, together with the counterexample
processing described later in Sect. 3.3. Furthermore, a table may need several rounds of
these operations before being prepared (cf. Algorithm 1), since certain conditions may
be violated by different, interleaved operations.
3.2 Hypothesis construction
As soon as the timed observation table T is prepared, a hypothesis can be constructed
in two steps, i.e., the learner first builds a DFA M based on the information in T, and
then transforms M to a hypothesis H, which will later be shown as a COTA.
Given a prepared timed observation table T = (Σ, Σ, Σ r , S, R, E, f), a DFA
M = (Q M , Σ M , Δ M , q
0
M , F M ) can be built as follows:
– the finite set of locations Q M = {q row (s) | s ∈ S};
– the initial location q
0
M = q row () for ∈ S;
– the set of accepting locations F M = {q row (s) | f (s · ) = + for s ∈ S and ∈ E};
– the finite alphabet Σ M = {σ r ∈ Σ r | γ r · σ r ∈ S ∪ R for γ r ∈ Σ
∗
r };
– the finite set of transitions Δ M = {(q row (γr) , σ r , q row (γr·σr) ) | γ r · σ r ∈ S ∪
R for γ r ∈ Σ
∗
r and σ r ∈ Σ r }.
The constructed DFA M is compatible with the timed observation table T in the
sense captured by the following lemma.
Lemma 1. For a prepared timed observation table T = (Σ, Σ, Σ r , S, R, E, f), for
every γ r ·e ∈ (S ∪R)·E, the constructed DFA M = (Q M , Σ M , Δ M , q
0
M , F M ) accepts
π(Π {1,2} γ r · e) if and only if f (γ r · e) = +.
The learner then transforms the DFA M to a hypothesis H = (Σ, Q, q 0 , F, c, Δ),
with Q = Q M , q 0 = q
0
M , F = F M , c being the clock and Σ the given alphabet as in T.
The set of transitions Δ in H can be constructed as follows: For any q ∈ Q M and σ ∈
Σ, let Ψ q,σ = {μ | (q, (σ, μ, b), q
) ∈ Δ M }, then applying the partition function P
c
(·)
(defined below) to Ψ q,σ returns k intervals, written as I 1 , · · · , I k , satisfying μ i ∈ I i for
any 1 ≤ i ≤ k, where k = |Ψ q,σ |; consequently, for every (q, (σ, μ i , b i ), q
) ∈ Δ M , a
fresh transition δ i = (q, σ, I i , b i , q
) is added to Δ.