@TechReport{	  it:2004-017,
  author	= {Parosh Aziz Abdulla and Aletta Nylen},
  title		= {Better-Structured Transition Systems},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {2004},
  number	= {2004-017},
  month		= apr,
  abstract	= {In automated verification of infinite-state systems, a
		  variety of algorithms that operate on constraints
		  representing sets of states have been developed. Many of
		  these algorithms rely on well quasi-ordering of the
		  constraint system for proving termination. A number of
		  methods for generating new well quasi-ordered constraint
		  systems have been proposed. However, many of these
		  constraint systems suffer from constraint explosion as the
		  number of constraints generated during analysis grows
		  exponentially with the size of the problem. We suggest
		  using the theory of better quasi-ordering to prove
		  termination since that will allow generation of constraint
		  systems that are less prone to constraint explosion. We
		  also present a method to derive such constraint systems. We
		  introduce existential zones, a constraint system for
		  verification of systems with an unbounded number of clocks
		  and use our methodology to prove that existential zones are
		  better quasi-ordered. We show how to use existential zones
		  in verification of timed Petri nets and present some
		  experimental results. Finally, we present several other
		  constraint systems which have been derived using our
		  methodology.}
}