We define an extension of time Petri nets such that the time at which a transition can fire, also called its firing date, may be dynamically updated. Our extension provides two mechanisms for updating the timing constraints of a net. First, we propose to change the static time interval of a transition each time it is newly enabled; in this case the new time interval is given as a function of the current marking. Next, we allow to update the firing date of a transition when it is persistent, that is when a concurrent transition fires. We show how to carry the widely used state class abstraction to this new kind of time Petri nets and define a class of nets for which the abstraction is exact. We show the usefulness of our approach with two applications: first for scheduling preemptive task, as a poor man’s substitute for stopwatch, then to model hybrid systems with non trivial continuous behavior.
For future works, we plan to study an extension of our approach to other models of real-time systems and to other state-space abstractions. For instance the Strong construction of @cite_11 , that is finer than the construction but that is needed when considering the addition of priorities. The strong relies on the use of , rather than firing domains, and has some strong resemblance with the zone constructions commonly used for analysis of . Another, quite different, type of abstractions rely on the use of a discrete time semantics for . We can obtain a discrete semantic by, for instance, restricting continuous transitions @math to the case where @math is an integer. This approach could be useful when modeling hybrid systems, since it is a simple way to add a quantization over time as well as over values.
@cite_11
1841167015
This paper is concerned with construction of some state space abstractions for Time Petri nets. State class spaces were introduced long ago by Berthomieu and Menasche as finite representations for the typically infinite state spaces of Time Petri nets, preserving their linear time temporal properties. This paper proposes a similar construction that preserves their branching time temporal properties. The construction improves a previous proposal by Yoneda and Ryuba. The method has been implemented, computing experiments are reported.