Affiliations: IRCCyN 1 rue de la Noë, BP 92101 44321
Nantes Cedex 03, France.
E-mail: {morgan.magnin,pierre.molinaro,olivier-h.roux}@irccyn.ec-nantes.fr
Abstract: With this contribution, we aim to draw a comprehensive
classification of Petri nets with stopwatches w.r.t. expressiveness and
decidability issues. This topic is too ambitious to be summarized in a single
paper. That is why we present our results in two different parts. In the first
part of our work, we established new results regarding to both dense-time and
discrete-time semantics. We now focus on the discrete-time specificities. We
address the class of bounded Petri nets with stopwatches and reset arcs
(rSwPNs), which is an extension of T-time Petri nets (TPNs) where time is
associated with transitions. Stopwatches can be reset, stopped and started. We
recall the formal dense-time and discrete-time semantics of these models in
terms of Transition Systems. We study the expressiveness of rSwPNs and its
subclasses w.r.t. (weak) bisimilarity (behavioral semantics). The main results
are following: 1) Discrete-time bounded TPNs, discrete-time bounded rSwPNs and
untimed Petri nets are equally expressive; 2) The resulting (final)
classification of models is given by a set of relations explained in Fig. 7.
While investigating expressiveness, we exhibit proofs that can be easily
extended to the resolution of decidability issues. Among other results, we
prove that, for bounded rSwPNs, the state and marking reachability problems -
undecidable with dense-time semantics - are decidable when discrete-time is
considered. Table 1 gives a synthesis of the main decidability results for
these models. For the sake of simplicity, our results are explained on a model
such that the stopwatches behaviors are expressed using inhibitor arcs. Our
conclusions can however be easily extended to the general class of Stopwatch
Petri nets.
Keywords: real-time systems, time Petri nets, discrete-time semantics, Petri nets with stopwatches, expressiveness, decidability
