Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Minimization of Non-deterministic Automata with Large Alphabets
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. (Algorithmic Program Verification)
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. (Algorithmic Program Verification)
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. (Algorithmic Program Verification)
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. (Algorithmic Program Verification)
2006 (Engelska)Ingår i: Implementation and Application of Automata, Springer Berlin/Heidelberg, 2006, 31-42 s.Konferensbidrag, Publicerat paper (Refereegranskat)
Ort, förlag, år, upplaga, sidor
Springer Berlin/Heidelberg, 2006. 31-42 s.
Serie
Lecture Notes in Computer Science, 3845
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:uu:diva-94525DOI: 10.1007/11605157_3ISBN: 3-540-31023-1 (tryckt)OAI: oai:DiVA.org:uu-94525DiVA: diva2:168401
Konferens
CIAA 2005, June 27-29, Sophia Antipolis, France
Tillgänglig från: 2006-05-12 Skapad: 2006-05-12 Senast uppdaterad: 2014-07-01Bibliografiskt granskad
Ingår i avhandling
1. Verification of Parameterized and Timed Systems: Undecidability Results and Efficient Methods
Öppna denna publikation i ny flik eller fönster >>Verification of Parameterized and Timed Systems: Undecidability Results and Efficient Methods
2006 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
Abstract [en]

Software is finding its way into an increasing range of devices (phones, medical equipment, cars...). A challenge is to design verification methods to ensure correctness of software.

We focus on model checking, an approach in which an abstract model of the implementation and a specification of requirements are provided. The task is to answer automatically whether the system conforms with its specification.We concentrate on (i) timed systems, and (ii) parameterized systems.

Timed systems can be modeled and verified using the classical model of timed automata. Correctness is translated to language inclusion between two timed automata representing the implementation and the specification. We consider variants of timed automata, and show that the problem is at best highly complex, at worst undecidable.

A parameterized system contains a variable number of components. The problem is to verify correctness regardless of the number of components. Regular model checking is a prominent method which uses finite-state automata. We present a semi-symbolic minimization algorithm combining the partition refinement algorithm by Paige and Tarjan with decision diagrams.

Finally, we consider systems which are both timed and parameterized: Timed Petri Nets (TPNs), and Timed Networks (TNs). We present a method for checking safety properties of TPNs based on forward reachability analysis with acceleration. We show that verifying safety properties of TNs is undecidable when each process has at least two clocks, and explore decidable variations of this problem.

Ort, förlag, år, upplaga, sidor
Uppsala: Acta Universitatis Upsaliensis, 2006. 29 s.
Serie
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 187
Nyckelord
Parameterized Systems, Timed Systems, Symbolic Model Checking, Forward Reachability, Acceleration, Robust Languages, Language Universality, Automata Minimization, Bisimulation
Identifikatorer
urn:nbn:se:uu:diva-6891 (URN)91-554-6574-9 (ISBN)
Disputation
2006-06-02, Häggsalen, Ångström Laboratory, Polacksbacken, Lägerhyddsvägen 1, Uppsala, 10:00
Opponent
Handledare
Tillgänglig från: 2006-05-12 Skapad: 2006-05-12 Senast uppdaterad: 2011-02-18Bibliografiskt granskad
2. Reduction Techniques for Finite (Tree) Automata
Öppna denna publikation i ny flik eller fönster >>Reduction Techniques for Finite (Tree) Automata
2008 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
Abstract [en]

Finite automata appear in almost every branch of computer science, for example in model checking, in natural language processing and in database theory. In many applications where finite automata occur, it is highly desirable to deal with automata that are as small as possible, in order to save memory as well as excecution time.

Deterministic finite automata (DFAs) can be minimized efficiently, i.e., a DFA can be converted to an equivalent DFA that has a minimal number of states. This is not the case for non-deterministic finite automata (NFAs). To minimize an NFA we need to compute the corresponding DFA using subset construction and minimize the resulting automaton. However, subset construction may lead to an exponential blow-up in the size of the automaton and therefore even if the minimal DFA may be small, it might not be feasible to compute it in practice since we need to perform the expensive subset construction.

To aviod subset construction we can reduce the size of an NFA using heuristic methods. This can be done by identifying and collapsing states that are equal with respect to some suitable equivalence relation that preserves the language of the automaton. The choice of an equivalence relation is a trade-off between the desired amount of reduction and the computation time since the coarser a relation is, the more expensive it is to compute. This way we obtain a reduction method for NFAs that is useful in practice.

In this thesis we address the problem of reducing the size of non-deterministic automata. We consider two different computation models: finite tree automata and finite automata. Finite automata can be seen as a special case of finite tree automata and all of the previously mentioned results concerning finite automata are applicable to tree automata as well. For non-deterministic bottom-up tree automata, we present a broad spectrum of different relations that can be used to reduce their size. The relations differ in their computational complexity and reduction capabilities. We also provide efficient algorithms to compute the relations where we translate the problem of computing a given relation on a tree automaton to the problem of computing the relation on a finite automaton.

For finite automata, we have extended and re-formulated two algorithms for computing bisimulation and simulation on transition systems to operate on finite automata with alphabets. In particular, we consider a model of automata where the labels are encoded symbolically and we provide an algorithm for computing bisimulation on this partial symbolic encoding.

Ort, förlag, år, upplaga, sidor
Uppsala: Acta Universitatis Upsaliensis, 2008. 65 s.
Serie
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 562
Nyckelord
Finite automata, tree automata, bisimulation, minimization, simulation, composed bisimulation, composed simulation
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Datavetenskap
Identifikatorer
urn:nbn:se:uu:diva-9330 (URN)978-91-554-7313-6 (ISBN)
Disputation
2008-11-21, Room 2446, Polacksbacken, Lägerhyddsvägen 2D, Uppsala, 09:15 (Engelska)
Opponent
Handledare
Tillgänglig från: 2008-10-31 Skapad: 2008-10-31 Senast uppdaterad: 2014-07-01Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas

Övriga länkar

Förlagets fulltext

Sök vidare i DiVA

Av författaren/redaktören
Abdulla, Parosh AzizDeneux, JohannKaati, Lisa
Av organisationen
Datorteknik
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar

Altmetricpoäng

Totalt: 1190 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf