Technical Report 2000-021

BQOs and Timed Petri Nets

Parosh Aziz Abdulla and Aletta Nylén

August 2000

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.