Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets

AbstractThe aim of this research has been to associate the modeling capacities of hybrid Petri nets with the analysis power of hybrid automata in order to perform formal verification of hybrid dynamic systems. In this paper, we propose an extension of hybrid Petri nets, called multisingular hybrid Petri nets (MSHPNs), for modeling and verification of hybrid dynamic systems. This extension consists of enriching hybrid Petri nets with the capabilities of hybrid automata to control the execution and firing of transitions and some modeling facilities for describing some repeatedly encountered aspects of timed and hybrid systems. We discuss the challenging issues of speed computation raised by addition of execution predicates and introduce a speed-based partitioning technique, which is essential for state space computation. We also introduce a method for reachability analysis of MSHPNs, consisting of computing the state class graph. Thus, the verification of timing properties of MSHPNs can be conducted using the existing techniques and tools. The proposed formalism has the expressiveness of multisingular hybrid automata besides the capabilities of Petri nets for modeling concurrent and distributed systems. Some illustrative examples of the proposed formalism are also presented in this paper