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. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Traonouez, L. M., Lime, D., & Roux, O. H. (2008). Parametric model-checking of time petri nets with stopwatches using the state-class graph. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5215 LNCS, pp. 280–294). https://doi.org/10.1007/978-3-540-85778-5_20
Mendeley helps you to discover research relevant for your work.