Logo: to the web site of Uppsala University

uu.sePublications from Uppsala University
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Inference of Event-Recording Automata using Timed Decision Trees
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2008 (English)Report (Other academic)
Abstract [en]

In regular inference, the problem is to infer a regular language, typically represented by a deterministic finite automaton (DFA) from answers to a finite set of membership queries, each of which asks whether the language contains a certain word. There are many algorithms for learning DFAs, the most well-known being the L* algorithm due to Dana Angluin. However, there are almost no extensions of these algorithms to the setting of timed systems. We present an algorithm for inferring a model of a timed system using Angluin's setup. One of the most popular model for timed system is timed automata. Since timed automata can freely use an arbitrary number of clocks, we restrict our attention to systems that can be described by event-recording automata (DERAs). In previous work, we have presented an algorithm for inferring a DERA in the form of a region graph. In this paper, we present a novel inference algorithm for DERAs, which avoids constructing a (usually prohibitively large) region graph. We must then develop techniques for inferring guards on transitions of a DERA. Our construction deviates from previous work on inference of DERAs in that it first constructs a so called timed decision tree from observations of system behavior, which is thereafter folded into an automaton.

Place, publisher, year, edition, pages
2008.
Series
Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2008-014
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:uu:diva-97240OAI: oai:DiVA.org:uu-97240DiVA, id: diva2:172085
Available from: 2008-04-29 Created: 2008-04-29 Last updated: 2024-05-30Bibliographically approved
In thesis
1. Learning of Timed Systems
Open this publication in new window or tab >>Learning of Timed Systems
2008 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Regular inference is a research direction in machine learning. The goal of regular inference is to construct a representation of a regular language in the form of deterministic finite automaton (DFA) based on the set of positive and negative examples. DFAs take strings of symbols (words) as input, and produce a binary classification as output, indicating whether the word belongs to the language or not. There are two types of learning algorithms for DFAs: passive and active learning algorithms. In passive learning, the set of positive and negative examples is given and not chosen by inference algorithm. In contrast, in active learning, the learning algorithm chooses examples from which a model is constructed.

Active learning was introduced in 1987 by Dana Angluin. She presented the L* algorithm for learning DFAs by asking membership and equivalence queries to a teacher who knows the regular language accepted by DFA to be learned. A membership query checks whether a word belongs to the language or not. An equivalence query checks whether a hypothesized model is equivalent to the DFA to be learned.The L* algorithm has been found to be useful in different areas, including black box checking, compositional verification and integration testing. There are also other algorithms similar to L* for regular inference. However, the learning of timed systems has not been studied before. This thesis presents algorithms for learning timed systems in an active learning framework.

As a model of timed system we choose event-recording automata (ERAs), a determinizable subclass of the widely used timed automata. The advantages of ERA in comparison with timed automata, is that it is known priori the set of clocks of an ERA and when clocks are reset. The contribution of this thesis is four algorithms for learning deterministic event-recording automaton (DERA). Two algorithms learn a subclass of DERA, called event-deterministic ERA (EDERA) and two algorithms learn general DERA.

The problem with DERAs that they do not have canonical form. Therefore we focus on subclass of DERAs that have canonical representation, EDERA, and apply the L* algorithm to learn EDERAs. The L* algorithm in timed setting requires a procedure that learns clock guards of DERAs. This approach constructs EDERAs which are exponentially bigger than automaton to be learned. Another procedure can be used to lean smaller EDERAs, but it requires to solve NP-hard problem.

We also use the L* algorithm to learn general DERA. One drawback of this approach that inferred DERAs have a form of region graph and there is blow-up in the number of transitions. Therefore we introduce an algorithm for learning DERA which uses a new data structure for organising results of queries, called a timed decision tree, and avoids region graph construction. Theoretically this algorithm can construct bigger DERA than the L* algorithm, but in the average case we expect better performance.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2008. p. 44
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 434
Keywords
learning regular languages, timed systems, event-recording automata
Identifiers
urn:nbn:se:uu:diva-8763 (URN)978-91-554-7207-8 (ISBN)
Public defence
2008-05-23, polhemsalen, Ångström Laboratory, Uppsala University, Uppsala, 13:15
Opponent
Supervisors
Available from: 2008-04-29 Created: 2008-04-29 Last updated: 2022-01-28Bibliographically approved

Open Access in DiVA

fulltext(410 kB)91 downloads
File information
File name FULLTEXT01.pdfFile size 410 kBChecksum SHA-512
d7addc86e5e16966c3ed6255fb48ba48e14678f983cb06556babb01122db33699675ab883cfd838048d203dc13e97bb85e8971bbe4ab1e17da4d67a77f1549e8
Type fulltextMimetype application/pdf

Authority records

Grinchtein, OlgaJonsson, Bengt

Search in DiVA

By author/editor
Grinchtein, OlgaJonsson, Bengt
By organisation
Computer Systems
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 91 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 825 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf