uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Verification of Infinite-State Systems: Decision Problems and Efficient Algorithms
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
1999 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

This thesis presents methods for the verification of distributed systems with infinite state spaces. We consider several verification problems for lossy channel systems, a class of infinite-state systems consisting of finite-state machines that communicate over unbounded, but lossy, FIFO channels. We also combine partial order techniques with symbolic techniques to improve performance of verification algorithms for infinite state systems.

We study several implementation relations between lossy channel systems and finite transition systems, and show decidability of the following problems: trace inclusion, trace equivalence, simulation preorder, bisimulation equivalence, weak bisimulation equivalence in both directions, and weak simulation preorder in one direction. We further show that weak simulation preorder in the other direction is undecidable.

Partial order reduction techniques are utilised to avoid exploring multiple interleavings of independent transitions. Constraint systems are introduced as a symbolic technique to represent (possibly infinite) sets of states. We present general methods for the application of partial order techniques for the verification of constraint systems. The method described is used for checking safety properties using forward or backward reachability analysis. It is based on the use of a—not necessarily symmetric—commutativity relation between operations. In contrast with previously existing approaches to partial order verification, which are based on a symmetric relation on transitions, our method does not require the relation to be symmetric. Partial order verification methods for lossy channel systems and for unsafe (i.e., infinite-state) Petri nets are developed to demonstrate the applicability of this approach.

Place, publisher, year, edition, pages
Department of Computer Systems, Uppsala University , 1999. , 120 p.
DoCS, ISSN 0283-0574 ; 110
National Category
Computer Engineering
Research subject
Computer Systems
URN: urn:nbn:se:uu:diva-1167ISBN: 99-2963604-8OAI: oai:DiVA.org:uu-1167DiVA: diva2:160718
Public defence
1999-06-07, Room X, Uppsala University, Uppsala, 13:00 (English)
Available from: 1999-05-17 Created: 1999-05-17 Last updated: 2015-01-30Bibliographically approved

Open Access in DiVA

No full text

By organisation
Department of Computer Systems
Computer Engineering

Search outside of DiVA

GoogleGoogle Scholar

Total: 420 hits
ReferencesLink to record
Permanent link

Direct link