Quantitative evaluation of time-dependent Petri nets and applications to biochemical networks

Time Petri nets (TPN) are a well-known extension of standard Petri nets, where each transition gets a continuous time interval, specifying the range of the transition's firing time. In contrast, Timed Petri nets are a different time-dependent extension where a time duration is associated with each transition. We sketch a locally defined transformation from a Timed into a Time Petri net. Additionally, we consider time-dependent Petri nets, where the firing of each transition lasts a certain time which is limited by both a lower and an upper bound. These nets can also be transformed locally into TPN and are used in this paper for modelling and analysing biochemical systems, and we present algorithms allowing their quantitative analyses. We consider algorithms which work for arbitrary systems, i.e., bounded as well as unbounded ones, and algorithms, which are suitable for bounded systems only. The crucial point is the state space reduction, which exploits basically two ideas: parametric state description and discretisation of the state space. Altogether, we introduce eight problems, characterised by their input/ output relation. A sketch of the solution idea as well as possible application scenarios to evaluate biochemical systems are given, too.