Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph

Abstract. In this paper, we propose a new framework for the parametric verification of time Petri nets with stopwatches controlled by inhibitor arcs. We first introduce an extension of time Petri nets with inhibitor arcs (ITPNs) with temporal parameters. Then, we define a symbolic representation of the parametric state space based on the classical state class graph method. The parameters of the model are embedded into the firing domains of the classes, that are represented by convex polyhedra. Finally, we propose semi-algorithms for the parametric model-checking of a subset of parametric TCTL formulae on ITPNs. We can thus generate the set of the parameter valuations that satisfy the formulae. Key words: Time Petri nets, stopwatches, model-checking, parameters, state-class graph

• Type: Conference
• Year: 2008
• Where: FORMATS
• Authors: Louis-Marie Traonouez, Didier Lime, Olivier H. Roux
• Keywords: Formal Methods, FORMATS 2008, Inhibitor Arcs, Parametric State Space, Time Petri Nets