Continuous Petri nets (CPNs) form a model of (uncountably infinite) dynamic systems that has been successfully explored for modelling and theoretical purposes. Let the mode of a marking be the set of transitions fireable in the future. Along a firing sequence, the sequence of different modes is non increasing, and forms what we call the trajectory of the sequence. In CPNs, a marking can be reachable by a finite sequence, or lim-reachable by an infinite convergent sequence. The set of trajectories (resp. markings) obtained via lim-reachability (sometimes strictly) includes the set of trajectories (resp. markings) obtained via reachability. Here, we introduce transfinite firing sequences over countable ordinals and establish several results: (1) while trans-reachability is equivalent to lim-reachability, the set of trajectories associated with trans-reachability may be strictly larger than the one associated with lim-reachability; (2) w.r.t. trajectories, transfinite sequences over ordinals smaller than ω 2 are enough; and (3) checking whether a trajectory is achievable is NP-complete. We then turn to a more difficult problem: the specification, for all transfinite firing sequences, of their achievable signatures, i.e. the sequences of markings witnessing the changes of mode along the trajectory. In view of this goal, we define a finite symbolic reachability tree (SRT) that tracks the possible signatures of the system; in the SRT, a set of markings with same mode is associated with each vertex. We establish that, for bounded CPNs, reversibility holds inside the leaves of the SRT (which correspond to the long-run behaviours). From an algorithmic point of view, we show how to build an effective representation of the SRT in exponential time, even when the CPN is unbounded. The length of an infinite firing sequence, i.e. the cumulated amount of firings, may be finite or infinite. Contrary to finite length infinite firing sequences, those with an infinite length may not converge and in fact their study is more involved. First we introduce a notion of similarity and show that every infinite length convergent firing sequence has a similar finite length firing sequence. Then we provide a necessary and sufficient condition for the existence of an infinite length firing sequence and another one for the existence of a converging infinite length firing sequence yielding polynomial time algorithms for checking such an existence.
Stefan et al. (Tue,) studied this question.