Learning One-Clock Timed Automata
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 22 | |
| Author | ||
| License | CC Attribution 3.0 Germany: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/55023 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
| |
| Keywords |
00:00
Element (mathematics)Equivalence relationOracleSoftware frameworkQuery languageDeterministic finite automatonInfinityAutomationDeterminismHypothesisFunction (mathematics)Regular graphAutomatonState of matterInformationPoint (geometry)Database normalizationPartition (number theory)Similarity (geometry)Reduction of orderNormal (geometry)Natural languageGroup actionBoundary value problemExponential functionKolmogorov complexityProcess (computing)Radical (chemistry)Instance (computer science)IterationPlastikkarteTheory of relativityMultiplication signResultantSoftware testingElectronic mailing listCASE <Informatik>Social classInformationProcess (computing)Row (database)AutomatonKolmogorov complexityNatural languageAlgorithmElement (mathematics)Query languageState of matterPlastikkarteFunction (mathematics)Set (mathematics)Equivalence relationTable (information)Extension (kinesiology)AdditionState observerNormal (geometry)WordSummierbarkeitTheoremInstance (computer science)Category of beingRevision controlComplete metric spaceSynchronizationSymbol tableCondition numberModal logicGroup actionCorrespondence (mathematics)Form (programming)NumberAbstract machine1 (number)Endliche ModelltheorieSampling (statistics)Thermal fluctuationsPairwise comparisonExponential functionMixed realitySeries (mathematics)Physical systemAreaMachine learningDifferent (Kate Ryan album)Parameter (computer programming)Power (physics)Alphabet (computer science)Graph (mathematics)Reduction of orderCellular automatonOrder (biology)Communications protocolDeterminismSign (mathematics)Radical (chemistry)Point (geometry)Address spaceReal-time operating systemMereologySystem identificationLink (knot theory)Regular graphUniform resource locatorDeterministic finite automatonLevel (video gaming)Sigma-algebraMechanism designCompilerLogical constantCounterexampleGenetic programmingRandomizationMaxima and minimaPartition (number theory)Semiconductor memoryHypothesisRight angleDecision theoryAverageComputer animation
Transcript: English(auto-generated)
00:02
Hi everyone, my name is Bo Kuo Tan. Today, I will describe our work on Learning in Cloud-Time Automata. This is joint work with Jie An, Minxuan Acheng, Nanjing Zhang, and Miao-Miao Zhang from Tongji University, Haqing University, and the Institute of Thoughtwork, Chinese Academy of Sciences.
00:25
This talk will be in three parts. First, I will briefly introduce automata learning and the L-STAR algorithm. Next, I will describe our work extending the L-STAR algorithm to Learning in Cloud-Time Automata. Finally, I will conclude with a discussion of future work.
00:47
First, let us begin by introducing automata learning by comparison with regular machine learning. In machine learning, we usually have a model in the form of a function f from x to y and a set of samples which are pairs of points from s and y.
01:05
From this sample set, we wish to identify or approximate its function f and use it to predict the value of f and other points. In automata learning, the setting is a bit different. Here, the model f is a language over some alphabet sigma,
01:23
which can be described by some kind of automaton. We are provided with a set of words over the alphabet, and for each word, whether it lies in the language or not. From this information, we need to identify or learn automaton.
01:43
Automaton learning has many applications, from system identification, to black-box learning, to language identification, and to inductive inference. Indeed, it is already a very well-established field. A major advancement in this area comes in 1987,
02:03
when Dana Anglin introduced the L-STAR algorithm for the active learning of deterministic finite automata. In the setting of active learning, the learner is allowed two kinds of queries, membership and equivalent queries. The learning process usually begins with the learner asking a series of membership queries
02:26
in the form of whether a word u is in the language, and the teacher responds yes or no. The learner then records this information in something called an observation table.
02:42
When the observation table is ready in some sense, the learner produces a hypothesis, which is an automaton a, and asks the teacher whether the language of a, l of a, is the same as the language to be learned. The teacher either replies yes,
03:00
in which case the learning process is over, or no, in which case she has to provide a counterexample u' in the difference between l of a and l. The learner then incorporates this counterexample into the observation table, and asks further membership queries,
03:21
eventually producing a more refined hypothesis. One significant feature of the algorithm is that it has polynomial costs. The number of required membership and equivalent queries is polynomial in the sense of the automaton.
03:43
More recent work extends the L-STAR algorithm to different models. For example, mini-machines, high automata, register automata, non-deterministic final automaton, push automata, symbolic automata, and Markov decision processes, and so on.
04:02
In our work, we wish to do something similar, extending the L-STAR algorithm to timed automata, in order to learn timed models of real-time systems. There have been work in learning timed models in the past as well, including active learning of event-reporting automata,
04:22
passive identification of timed automata, and passive learning of timed automata via genetic programming and testing techniques. However, we believe that we are the first to consider active learning of real-time automata based on the L-STAR algorithm.
04:44
This concludes the introduction and motivation, and we now move to the main part of the talk. In this work, we consider learning timed automata with a single clock. Even in this restricted setting, there are still many challenges compared to learning DFAs.
05:04
In particular, the state now includes both location and the value of clock. Each transition is described not only by an action, but also by a guard condition, and recent information indicating whether the clock should be reset after each transition.
05:24
Finally, and somewhat related to all of the above points, see the difference between the time as observed from the outside of the automata and the clock value observed inside of the automata. And we have to build a link between these two kinds of timing values.
05:40
Our solution addresses each of the above challenges in turn. First, we describe a normalization map. We describe a normalization map from delay timed words corresponding to time as observed from the outside to logical timed words corresponding to value of the clock inside the automaton.
06:03
This map assumes that recent information is already available. Second, for the logical timed words, we define a partition function matching logical timed values to finite intervals. This idea is already familiar from existing research on learning symbolic automata.
06:24
Finally, we address the difficult issue of learning recent information. We first consider the case of a smart teacher who can tell their learner recent information, build a polynomial algorithm under this setting, and then drop this assumption that is we reduce the problem to the normal teacher case
06:45
by using a mechanism for getting recent information. And this reduction and this guessing process will result in an exponential increase in complexity.
07:00
So this is the basic idea of the algorithm. And now let us look at some details. First, we begin by fixing some notations. Let A be a determinated one-clock timed automata abbreviated as DOTA, which recognizes a target language L. Let sigma be the alphabet for concreteness consisting of two actions A and B here.
07:26
And we use top and bottom symbols to denote reset and no reset. We consider the case of complete DOTA. If the initial DOTA is not complete, we complete it by adding a sync and necessary additional conditions.
07:45
We define delayed timed words to correspond to observations of time delayed from the outset. For example, here in the delayed timed word omega, 0, 1.1, and 1 are the time that we wait before taking each action.
08:03
In contrast, the logical timed words correspond to values of clock inside the automaton. So here in the logical timed word gamma, 0, 1.1, and 2.1 correspond to the value of clock when taking each action.
08:20
We can also record reset information in a logical timed word, resulting in reset logical timed words. For example, in this case, the reset logical timed word gamma r corresponds to the delayed timed word omega above. In particular, since there is no delay after the second transition,
08:42
we see that the clock value at the third transition should be the sum of the previous two delays, which is 1.1 plus 1, which equals 2.1. Given a DOTA, let L of A represent the reset logical timed language recognized by A,
09:06
and let L of A be the logical timed language recognized by A. The guiding principle of the algorithm is the following theorem shown below, which means that learning the delayed timed language of A, which is our eventual goal,
09:23
can be reduced to learning the reset logical timed language of A. Hence, the smart teacher setting can be considered as the process of learning the reset logical timed language. The membership queries are logical timed words, and the teacher responds by providing additional reset information.
09:48
The observation table that we use is an extension of the observation table in the usual LTA algorithm. The main thing to note here is that the rows s and r correspond to reset logical timed words,
10:02
and the columns e, which serve to distinguish between the rows, correspond to logical timed words. We define several properties on the observation table, similar to in other versions of LTA algorithms.
10:20
Reduced, closed, consistent, and evidence-closed. If the observation table does not satisfy any one of its properties, the learner extends the table in an appropriate way and asks membership queries to fill in the table. When all properties are satisfied, the learner is able to produce a candidate timed automaton on the table
10:45
and use it to ask an equivalence query. Here is an illustrative example of an observation table. We see that the rows s and r correspond to reset logical timed words,
11:06
and the columns e are logical timed words. Each entry on the table corresponds to whether the logical timed word is formed by connecting the timed word in the corresponding row and column within the language as determined by two membership queries.
11:25
For example, this graph here in this cell says that the timed word a1.1, followed by the empty timed word, is in the language as provided by the teacher. This information for no reset is also provided by the teacher.
11:44
Likewise, this minor sign here says that the timed word a0, followed by the empty timed word, is not in the language as given by the teacher, and likewise, the reset information here for having a reset is also provided by the teacher.
12:06
In the paper, we prove the following theoretical results. In the smart teacher setting, the learning process terminates and returns a data which recognizes the topic-timed language L. Furthermore, the complexity of the algorithm is polynomial in the size of the automaton
12:24
for both the number of membership queries and the number of equivalent queries. Next, we describe the algorithm in the normal teacher setting. In this setting, the teacher responds to delayed timed words and no longer returns reset information.
12:44
So the learner has to get the recent information in order to convert between delayed and logical timed words. The basic process is as follows. At every round, the learner passes all needed resets and puts all the resulting table candidates into a set to explore.
13:05
Then one table instance is taken from to-explore to be processed. Since the tables in to-explore already have test recent information available, fluctuations to be performed on the table are the same as the ones in the smart teacher setting.
13:25
In the paper, we prove the following results. The learning process with the normal teacher also terminates. The basic idea is that at every iteration, we select the table instance which requires the least number of guesses.
13:41
Moreover, the table candidate that practically gets its all-rated information is already in the search tree. This means the algorithm is finished before the number of tables considered reaches true to the power of the number of required guesses. This argument also shows that the complexity of the algorithm is exponential in the size of the automata.
14:06
In particular, the number of tables considered, the number of mixed queries, and the number of equivalent queries are all exponential in the size of the input. We now look at some experimental results.
14:27
We generated random time automata for different number of locations, size of alphabet, and maximum clock constant. For each group, we generated 10 time automata so that the number shown here is the average over 10 examples.
14:45
We see that in the smart teacher setting, the algorithm can easily handle time automata with up to 10, 12, and 14 locations. We also tried our algorithm on a real-life example coming from the functional specification of the TTP protocol.
15:06
On the left shows the original time automata, and on the right shows the result of learning. Here we note one aspect of the algorithm, which is that it is not guaranteed to return the automata with the minimum number of locations.
15:22
Instead, we see that some locations can be split in the learned automata. Finally, we look at experimental results in the normal teacher setting. Because of the exponential complexity of the algorithm, it can only do a small number of locations up to six in the time automata.
15:47
And in fact, we see that for some of the larger examples, and for some of the random examples, the algorithm is a time-out or a run-out of memory and is unable to learn the automata in the required time.
16:04
In conclusion, in our work, we introduce an active learning algorithm for deterministic run-clock time automata in the smart teacher setting. This results in an efficient polynomial algorithm.
16:20
Moreover, we describe the active learning algorithm in the normal teacher setting, in which case there is an exponential increase in complexity. In future work, we wish to extend the algorithm to more general classes of timed automata, for example, non-deterministic and multi-clock timed automata.
16:41
Moreover, we wish to consider how to improve the efficiency of the algorithm, in particular, dealing with the exponential complexity when testing results. And this is the list of related work.
17:03
Thank you for listening and I will now receive any questions.