uu.seUppsala University Publications
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
Minimization of Non-deterministic Automata with Large Alphabets
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Algorithmic Program Verification)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Algorithmic Program Verification)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Algorithmic Program Verification)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Algorithmic Program Verification)
2006 (English)In: Implementation and Application of Automata, Springer Berlin/Heidelberg, 2006, 31-42 p.Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2006. 31-42 p.
Series
Lecture Notes in Computer Science, 3845
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-94525DOI: 10.1007/11605157_3ISBN: 3-540-31023-1 (print)OAI: oai:DiVA.org:uu-94525DiVA: diva2:168401
Conference
CIAA 2005, June 27-29, Sophia Antipolis, France
Available from: 2006-05-12 Created: 2006-05-12 Last updated: 2014-07-01Bibliographically approved
In thesis
1. Verification of Parameterized and Timed Systems: Undecidability Results and Efficient Methods
Open this publication in new window or tab >>Verification of Parameterized and Timed Systems: Undecidability Results and Efficient Methods
2006 (English)Doctoral thesis, comprehensive summary (Other academic)
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.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2006. 29 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 187
Keyword
Parameterized Systems, Timed Systems, Symbolic Model Checking, Forward Reachability, Acceleration, Robust Languages, Language Universality, Automata Minimization, Bisimulation
Identifiers
urn:nbn:se:uu:diva-6891 (URN)91-554-6574-9 (ISBN)
Public defence
2006-06-02, Häggsalen, Ångström Laboratory, Polacksbacken, Lägerhyddsvägen 1, Uppsala, 10:00
Opponent
Supervisors
Available from: 2006-05-12 Created: 2006-05-12 Last updated: 2011-02-18Bibliographically approved
2. Reduction Techniques for Finite (Tree) Automata
Open this publication in new window or tab >>Reduction Techniques for Finite (Tree) Automata
2008 (English)Doctoral thesis, comprehensive summary (Other academic)
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.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2008. 65 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 562
Keyword
Finite automata, tree automata, bisimulation, minimization, simulation, composed bisimulation, composed simulation
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-9330 (URN)978-91-554-7313-6 (ISBN)
Public defence
2008-11-21, Room 2446, Polacksbacken, Lägerhyddsvägen 2D, Uppsala, 09:15 (English)
Opponent
Supervisors
Available from: 2008-10-31 Created: 2008-10-31 Last updated: 2014-07-01Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Abdulla, Parosh AzizDeneux, JohannKaati, Lisa

Search in DiVA

By author/editor
Abdulla, Parosh AzizDeneux, JohannKaati, Lisa
By organisation
Computer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 1212 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