August 2000
Abstract:In this paper, we use the theory of better quasi-orderings to define a methodology for inventing constraint systems which are both well quasi-ordered and compact. We apply our methodology by presenting new constraint systems for verification of systems with unboundedly many real-valued clocks, and use them for checking safety properties for lazy (non-urgent) timed Petri nets where each token is equipped with a real-valued clock.
Available as compressed Postscript (123 kB, no cover)
Download BibTeX entry.