Rewriting Logic and Elan: Prototyping Tools for Petri Nets with Time

摘要

Rewriting logic (RL) is an extension of standard algebraic specificationtechniques which use rewrite rules to model the dynamic behaviour of a system. In this paper we consider using RL and an associated support tool Elan as an environment for rapidly prototyping and analysing Petri nets with time. We link these algebraic tools to PEP, an existing Petri net tool which provides a user-friendly front end to our framework. Our flexible approach allows the wide range of possible time extensions presented in the literature to be investigated and thus overcomes one of the major drawbacks of the current hardwired tools. We demonstrate our ideas by considering time Petri nets in which transitions are associated with a firing interval. The flexibility of our approach is illustrated by modelling a range of semantic alternatives for time Petri nets taken from the literature.