Reachability Analysis of P-time Petri Nets with Parametric Markings

This paper deals with the verification of P-Time Petri nets with parametric markings. It investigates the verification of reach ability properties in the case of an upward-closed set of initial markings. We propose an efficient state space abstraction which preserves markings and firing sequences. In such an abstraction, sets of states reached by the same firing sequence are over-approximated and represented concisely by their minimal marking and the union of their time domains (abstract states). We show that even if abstract states may contain some extra states, we can retrieve the exact reachable states and then verify reach ability properties.