On the identifiability in the limit of timed automata
Sicco Verwer s.e.verwer@tudelft.nl
Mathijs de Weerdt m.m.deweerdt@tudelft.nl
Cees Witteveen c.witteveen@tudelft.nl
Delft University of Technology, P.O.Box 5031 2600GA Delft
We are interested in identifying a model for discrete event systems from observations. A common way to model discrete event systems is by using deterministic finite state automata (DFA). When observing a sys-tem, however, there often is information in addition to the system events, namely, their times of occurrence. If this time information is important, a DFA is too limited. For example, it is impossible to distinguish between events that occur quickly after each other, and events that occur after each other with a signifi-cant delay between them. Consequently, we would like a model that can also deal with time information. A well-known model for this purpose is the timed au-tomaton (TA) (Alur & Dill, 1994). In this model the time information is represented by a finite set of clocks, which can be reset by state transitions. The values of these clocks are then used in the guards of transitions. A clock guard is a Boolean constraint on the values of the clocks. A state transition can only occur when the guard of the transition is satisfied. We use intervals to intervals to denote a constraint for a single clock. Such a constraint is satisfied when the clock value is an element of this interval.
Formally a timed automaton (TA) is a tuple A = hQ, X, Σ, T, q0, F i, where Q is a finite set of states,
Σ is a finite set of symbols, X is a finite set of clocks, T is a finite set of transitions, F ⊆ Q is a subset of final states. A transition d ∈ T in this automaton is a tuple hq, q0, a, g, Ri, where q, q0∈ Q are the source and
target states, a ∈ Σ is the transition label, g is a clock guard, and R ⊆ X denotes the set of clocks reset by this transition.
Each clock of a TA increases synchronously with time. Thus when at some point in time a clock valuates to 1, it will valuate to 2 one time unit later. This is true unless the clock has been reset in the meantime. A reset of clock x at time t sets the time value of x to 0, after which it immediately continues increasing. We study the problem of identifying TAs from a data
1 4 3 b x [0,1], reset y d x [100, 110] 2 a reset x c y [0, 1], reset y 4
Figure 1. A DTA that is not identifiable from polynomial data. This is due to the fact that in order to reach state 4, a path needs to be of length exponential in the size of the clock guard (which are encoded in binary).
sample containing both positively and negatively la-beled timed strings. Such a string consists of event-time value pairs. For this problem is it interesting to know whether it is possible to construct a characteris-tic set (de la Higuera, 1997) for TAs. This proves to be the case for most, but not all, TAs. The TAs for which such a construction cannot exists are exactly those for which the shortest path to the part of the TA that needs to be identified is of length exponential in the size of the TA. This is a contradiction with the requirement that a characteristic set has to be of size polynomial in the size of the target concept. Figure 1 shows an example of such a TA.
Our proof for the identifiability of other TAs is based on a construction similar to the one used in the RPNI algorithm (Oncina & Garcia, 1992). The algorithm that we use is a standard state merging type of algo-rithm (Lang et al., 1998). In our algoalgo-rithm we first assume that there is one clock x, with 0 as its initial value. Then, we construct a timed APTA: each transi-tion in the TAPTA is given as clock guard the degen-erate interval (of length zero) of exactly the time value of the timed sample string used to create the transi-tion. For example, suppose that the pair (ai, ti) of a
timed example string is used to create a transition d. In this case, the value of the clock guard g of d is such that g(x) = [ti, ti]. Figure 2 shows an example of a
On the identifiability in the limit of timed automata . . . . a [0.8, 0.8] b [1.4, 1.4] [4.6, 4.6]b [8.0, 8.0]b a [1.5, 1.5] b [2.0, 2.0] [5.2, 5.2]a rejecting accepting
Figure 2. A TAPTA is usually a list of strings instead of a tree. a [0.8, 2.5] a a [1.5, 4.0] b a [0.8, 4.0] a b
Figure 3. A merge of two transitions by the determiniza-tion process.
In addition to a modified APTA, our timed state merg-ing algorithm requires a modified determinization pro-cedure. After a merge, when there are two transitions that have the same source state and the same label, and of which the clock guards g and g0 overlap, then these transitions and their target states are merged into one, see Figure 3.
Like the RPNI algorithm, our algorithm merges nodes in a fixed order based on the distance of the nodes and transitions from the start state. This distance is determined by an order ≺ over the timed strings of runs that end in nodes and transitions pointing to it. Given two timed strings s and s0, this order is such that s ≺ s0if: s is shorter than s0, or they are of equal length and the last character of s is alphabetically smaller than the last character of s0, or their untimed strings are equal and for each clock x ∈ X it holds that its value at the end of s is less then its value at the end of s0.
This order makes it possible to construct a character-istic set in an RPNI-like way:
• For each piece f (state, transition, guard, clock reset) of the TA that needs to be identified, create a positive string that reaches f in the shortest possible way (using ≺).
• For each piece that defines the behavior (i.e. tran-sitions, clock guards, and clock resets) create a pair of inconsistent examples (again using ≺) for every other possible behavior.
x y p p p l u
Figure 4. With two clocks the guards can be visualized as rectangles. The lower corner l and upper corner u are pos-itive examples. The projections p’s of u on other guards, together with u are pairs of inconsistent examples.
The first rule ensures that every piece is capable of being identified. The second rule ensures that our al-gorithm has to infer the target TA correctly. This is done by creating inconsistencies in such a way that only consistent merges are possible.
The key to the construction of our characteristic set is the merge order defined by ≺. Using this order we can directly identify the lower bound and the upper bound of all clock guards. Moreover, we can create pairs of inconsistent examples that ensure that the guard can-not be wrongly merged with acan-nother guard. These examples and are visualized in Figure 4.
The existence of a characteristic set implies identifi-ability in the limit from polynomial time and data. Hence there are a lot of TAs that are efficiently iden-tifiable in the limit. These TAs include all one-clock automata. When more than one clock exists, construc-tions such as the one in Figure 1 are possible that make the identifiability problem intractable. It is an open problem how often these cases occur in practice.
References
Alur, R., & Dill, D. L. (1994). A theory of timed automata. Theoretical Computer Science, 126, 183– 235.
de la Higuera, C. (1997). Characteristic sets for poly-nomial grammatical inference. Machine Learning, 27.
Lang, K. J., Pearlmutter, B. A., & Price, R. A. (1998). Results of the abbadingo one dfa learning competi-tion and a new evidence-driven state merging algo-rithm. ICGI. Springer.
