Hybrid Petri nets with general one-shot transitions

A hybrid Petri net formalism that allows deterministic, and fluid transitions is extended by generally distributed transitions that moves discrete tokens. Models in this formalism can be analyzed with Parametric Reachability Analysis, by computing all reachable locations, and by separating the deterministic and the stochastic evolution of the system. Several performance metrics, such as the distribution of fluid over time, can be derived by deconditioning according to arbitrary continuous probability distributions. This efficient concept allows for the analysis of an arbitrary number of fluid places, as opposed to classical stochastic hybrid Petri net approaches. Moreover, validation of our results against a FSPN tool shows that parametric reachability analysis provides more accurate results. A case study motivates and shows the potential of our approach.