Time Petri nets with inhibitor hyperarcs. Formal semantics and state space computation

In this paper, we define Time Petri Nets with Inhibitor Hyperarcs (IHTPN) as an extension of T-time Petri nets where time is associated with transitions. In this model, we consider stopwatches associated with transitions which can be reset, stopped and started by using classical arcs and branch inhibitor hyperarcs introduced by Janicki and Koutny [17]. We give a formal semantics for IHTPNs in terms of Timed Transition Systems and we position IHTPNs with regard to other classes of Petri nets in terms of timed language acceptance. We provide a method for computing the state space of IHTPNs. We first propose an exact computation using a general polyhedron representation of time constraints, then we propose an overapproximation of the polyhedra to allow a more efficient compact abstract representations of the state space based on DBM (Difference Bound Matrix).