×

zbMATH — the first resource for mathematics

Timed Petri nets and BQOs. (English) Zbl 0986.68092
Colom, José-Manuel (ed.) et al., Applications and theory of Petri nets 2001. 22nd international conference, ICATPN 2001, Newcastle upon Tyne, GB, June 25-29, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2075, 53-70 (2001).
Summary: We consider (unbounded) Timed Petri Nets (TPNs) where each token is equipped with a real-valued clock representing the “age” of the token. Each arc in the net is provided with a subinterval of the natural numbers, restricting the ages of the tokens travelling the arc. We apply a methodology previously developed by the authors, based on the theory of better quasi orderings (BQOs), to derive an efficient constraint system for automatic verification of safety properties for TPNs. We have implemented a prototype based on our method and applied it for verification of a parametrized version of Fischer’s protocol.
For the entire collection see [Zbl 0967.00078].

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
Uppaal
PDF BibTeX Cite
Full Text: Link