A Method to Prove Non-Reachability in Priority Duration Petri Nets

Article type: Research Article

Authors: Werner, Matthias | Popova-Zeugmann, Louchka | Richling, Jan

Affiliations: Kommunikations- und Betriebssysteme, Sekr. FR 6-3, Franklinstr. 28/29, TU Berlin, 10587 Berlin, Germany | Automata and System Theory Group, Department of Computer Science, Humboldt University of Berlin, Germany | Computer Architecture and Communication Group, Department of Computer Science, Humboldt University of Berlin, Germany

Abstract: Times and priorities are important concepts that are frequently used to model real-world systems. Thus, there exist extensions for Petri nets which allow to model times and priorities. In contrast, many proof techniques are based on classical (time-less and priority-less) Petri nets. However, this approach fails frequently for timed and prioritized Petri nets. In this paper, we present an approach to prove non-reachability in a Priority Duration Petri net. We use for this proving technique a state equation as well as conditions for firing that include a priority rule and a maximal step rule. Our approach leads to a system of equations and inequalities, which provide us with a sufficient condition of non-reachability. We demonstrate the application of our approach with an example.

Keywords: priority duration Petri net, state equation, non-reachability

Journal: Fundamenta Informaticae, vol. 61, no. 3-4, pp. 351-368, 2004