[BB11] Relevant Timed Schedules / Clock Vectors for Constructing Time Petri Net Reachability GraphsRevue Internationale avec comité de lecture : Journal Discrete Event Dynamic Systems: Theory and Applications, vol. 21(2 - 2011), pp. 171-204 , 2011
Mots clés: Time Petri nets – Reachability graph – Timed schedule based graph – Clock vector based graph
Résumé: We consider here the time Petri nets (the TPN model) and its state space abstractions. We show that only some timed schedules/clock vectors (one per enabled transition) of the clock/firing domains are relevant to construct reachability graphs for the TPN. Moreover, we prove formally that the resulting graphs are smaller than the TPN reachability graphs proposed in the literature. Furthermore, these results establish a relation between dense time and discrete time analysis of time Petri nets and allow also improving discrete time analysis by considering only some elements of the clock/firing domains.