State class graph for fuzzy time Petri nets

The objective of this paper is the formal verification of quantitative temporal properties of embedded systems. Our approach is different from the current state of the art where the verification of the properties is done after a complete design with numerical values for all parameters. The application domain is that of concurrent engineering design, where essential parameters may be ill-known. The formal mathematical framework used to take into account these ill-known constraints is the fuzzy set theory. The use of fuzzy theory for temporal constraints and Petri net theory for the dynamic aspect in the construction of a graph of states classes allows ensuring some properties during design phases where the value of some parameters is not well defined.