Logic in Computer Science (LICS 2000)

Paper: Better is Better than Well: On Efficient Verification of Infinite-State Systems (at LICS 2000)

Authors: Parosh Aziz Abdulla Aletta Nylén

Abstract

Many existing algorithms for model checking of infinite-state systems operate on constraints, which are used to represent (potentially infinite) sets of states. A general powerful technique, which can be employed for proving termination of these algorithms, is that of well quasi-orderings. Several methodologies have been proposed for derivation of new well quasi-ordered constraint systems. However, many of these constraint systems suffer from a “constraint explosion problem”, as the number of the generated constraints grows exponentially with the size of the problem. In this paper, we demonstrate that a refinement of the theory of well quasi-orderings, called the theory of better quasi-orderings is more appropriate for symbolic model checking, since it allows inventing constraint systems, which are both well quasi-ordered and compact. We apply our methodology to derive new constraint systems for verification of systems with unboundedly many clocks, broadcast protocols, lossy channel systems, and integral relational automata. The new constraint systems are exponentially more succinct than existing ones, and their well quasi-ordering cannot be shown by previous methods in the literature.

BibTeX

  @InProceedings{AbdullaNyln-BetterisBetterthanW,
    author = 	 {Parosh Aziz Abdulla and Aletta Nylén},
    title = 	 {Better is Better than Well: On Efficient Verification of Infinite-State Systems},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {132--140},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }