Sciweavers

Share
FORMATS
2008
Springer

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

8 years 3 months ago
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
Louis-Marie Traonouez, Didier Lime, Olivier H. Rou
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FORMATS
Authors Louis-Marie Traonouez, Didier Lime, Olivier H. Roux
Comments (0)
books