Algebraical Characterisation of Interval-Timed Petri Nets with Discrete Delays

Issue title: Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Popova-Zeugmann, Louchka | Pelz, Elisabeth

Affiliations: Department of Computer Science, Humboldt University, Germany, [email protected] | LACL, Université Paris Est Créteil, Fac de Sciences, Créteil, France, [email protected]

Note: [] Address for correspondence: Department of Computer Science, Humboldt University, Germany

Abstract: In this paper we consider Interval-Timed Petri nets (ITPN) which are an extension of Timed Petri nets. They are considered to behave with discrete delays. The class of ITPNs is Turing complete and therefore the reachability of an arbitrary marking in such a net is not decidable. We introduce a time dependent state equation for a firing sequence of ITPNs, which is analogous to the state equation for a firing sequence in standard Petri nets and we prove its correctness using linear algebra. Our result is original and delivers both a necessary condition for reachability and a sufficient condition for non-reachability of an arbitrary marking in an ITPN.

Keywords: Interval-Timed Petri nets, state equation, reachability, Interval-Timed Petri net analysis

DOI: 10.3233/FI-2012-766

Journal: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 341-357, 2012