Hybrid Predicate Transition Nets - A Formal Method for Modeling and Analyzing Cyber-Physical Systems

Cyber-physical systems are complex systems with hybrid behaviors. In this paper, hybrid predicate transition nets (HPrTNs) are proposed for modeling and analyzing cyberphysical systems. HPrTNs are formally defined and their relationships to hybrid automata are shown. Important features of HPrTNs including continuous places, differential equations for defining token evolution, and net composition are discussed. The applicability of HPrTNs is demonstrated through several wellknown benchmark hybrid systems.