Implementing timed extensions of Petri nets in Real-Time Maude

Abstract

We study three timed extensions of Petri nets. We demonstrate methods for transforming these types of Petri nets into Real-Time Maude programs. This lays the groundwork for a timed Petri net analysis tool in which these transformations will be automated. The programs we present elucidate the differences between the timed Petri net variants. This work provides further evidence that Real-Time Maude can be used to naturally express different models of concurrent real-time systems.