Timed Petri Nets: Efficiency of Asynchronous Systems

Formal Methods for the Design of Real-Time Systems
Eds.:M. Bernardo, F. Corradini
Springer 2004, Lect. Notes Comput. Sci. 3185, 25 – 58
Copyright by Springer, Berlin, Heidelberg DOI: 10.1007/b110123

We shortly discuss how Petri nets have been extended with timing constraints and then choose to associate clocks to tokens and time intervals to arcs from places to transitions. In this model, we present a timed testing approach derived from the testing scenario of De Nicola and Hennessy; timed testing gives rise to an implementation relation that requires an implementation to be at least as satisfactory as the specification regarding functionality and efficiency.

We show that we get the same implementation relation whether we regard time as continuous or as discrete; so we will work with discrete time, which is easier to handle, and nevertheless get results for continuous time, which is presumably more realistic. With our testing approach, we can show that timed refusal traces of a system are exactly the behaviour that can be observed by a user. Interestingly, this can already be observed by asynchronous observers, and this leads naturally to a faster-than relation for asynchronous systems. We close with a discussion of some examples.