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
Compact Constraints for Verification of Well Quasi-Ordered Programs
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2003 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

In this thesis we present algorithms and constraint systems for efficient verification of infinite-state transition systems that are monotonic with respect to a well quasi-ordering.

A major problem in verification of infinite-state systems is constraint explosion, that is, the number of constraints generated during analysis is too large. The problem can be reduced either by reducing the number of constraints that need to be analysed (partial order methods) or by producing constraint systems that are more compact in the sense that the number of states represented by a single constraint is increased. The main contributions of this thesis are:

• An unfolding algorithm for symbolic verification of unbounded Petri nets. Unfoldings is a partial order method which has previously only been used in verification of finite-state systems.

• A framework for developing compact constraint systems. The framework is based on the theory of better quasi-ordering and allows construction of constraint systems that are much more compact than those developed in previous frameworks based on well quasi-ordering.

• A framework for developing constraint systems that are suitable for forward analysis. In forward analysis, the constraints give a characterization of the set of reachable states. Although this is not computable in general, it turns out that for some applications forward analysis is more efficient than backward analysis.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis , 2003. , 119 p.
Series
Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1104-2516 ; 51
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-3813ISBN: 91-554-5788-6 (print)OAI: oai:DiVA.org:uu-3813DiVA: diva2:163756
Public defence
2003-12-04, Häggsalen, Ångströmlaboratoriet, Lägerhyddsvägen 1, Uppsala, 10:00
Opponent
Supervisors
Available from: 2003-11-13 Created: 2003-11-13 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text
Buy this publication >>

By organisation
Division of Computer SystemsComputer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

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