Parametric multisingular hybrid Petri nets: Formal definitions and analysis techniques

Multisingular hybrid Petri net (MSHPN) is an extension of hybrid Petri nets enriched with the capabilities of hybrid automata to achieve the practical expressive power of multisingular hybrid automata. In this paper, we define parametric multisingular hybrid Petri nets (P-MSHPNs), as a parametric extension of MSHPNs. We present the parametric reachability analysis techniques and algorithms and prove that the parametric reachability analysis of P-MSHPNs amounts to the analysis of standard MSHPNs. Once the parametric state space of a P-MSHPNs model is computed, it can either be used for parametric model checking analysis using the existing techniques or be instantiated to obtain non-parametric state spaces. P-MSHPNs models can be analysed to obtain the set of feasible configurations for the system parameters. We also give a method for deriving the set of constraints on the parameters that ensure the correctness of an invariant property and a method for finding the optimum parameter configuration.