Compact Constraints for Verification

of Well Quasi-Ordered Programs

By Aletta Nylen

December 2003

Uppsala University Press

ISBN: 91-554-5788-6

126 pages, 6 ½" x 9 ½"

$48.50 Paper Original

This Ph.D. dissertation explores 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 analyzed (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: (1) An unfolding algorithm for symbolic verification of unbound Petri nets. Unfoldings is a partial order method which has previously only been used in verification of finite-state systems, (2) 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, (3) 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.

Computer Science

Uppsala Dissertations from the Faculty of Science & Technology, No. 51

Return to Coronet Books main page