Compact Constraints for Verification of Well Quasi-Ordered Programs
2003 (English)Doctoral thesis, monograph (Other academic)
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.
Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1104-2516 ; 51
IdentifiersURN: urn:nbn:se:uu:diva-3813ISBN: 91-554-5788-6OAI: oai:DiVA.org:uu-3813DiVA: diva2:163756
2003-12-04, Häggsalen, Ångströmlaboratoriet, Lägerhyddsvägen 1, Uppsala, 10:00
Sere, Kaisa, Professor
Abdulla, Parosh, Professor