BQOs and Timed Petri Nets

• 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.

Publikations- och innehållstyp

vet (ämneskategori)

rap (ämneskategori)