zbMATH — the first resource for mathematics

Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques. (English) Zbl 1309.68140
Summary: 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 ($$\mathcal{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 $$\mathcal{P}$$-MSHPNs amounts to the analysis of standard MSHPNs. Once the parametric state space of a $$\mathcal{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. $$\mathcal{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.
MSC:
 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) 68Q45 Formal languages and automata
Software:
HyTech; Kronos; PPL
Full Text: