caa a22 4500 445822805 CHVBK 20180317145249.0 cr unu---uuuuu 170323e20110601xx s 000 0 eng 10.1007/s10626-011-0100-4 doi (NATIONALLICENCE)springer-10.1007/s10626-011-0100-4 Relevant Timed Schedules/Clock Vectors for Constructing Time Petri Net Reachability Graphs [Elektronische Daten] [Hanifa Boucheneb, Kamel Barkaoui] 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. Springer Science+Business Media, LLC, 2011 Time Petri nets nationallicence Reachability graph nationallicence Timed schedule based graph nationallicence Clock vector based graph nationallicence Boucheneb Hanifa Laboratoire VeriForm, Department of Computer Engineering, École Polytechnique de Montréal, Station Centre-ville, P.O. Box 6079, H3C 3A7, Montréal, Québec, Canada aut Barkaoui Kamel Laboratoire CEDRIC, Conservatoire National des Arts et Métiers, 292 rue Saint Martin, Paris, Cedex 03, France aut Discrete Event Dynamic Systems Springer US; http://www.springer-ny.com 21/2(2011-06-01), 171-204 0924-6703 21:2<171 2011 21 10626 https://doi.org/10.1007/s10626-011-0100-4 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10626-011-0100-4 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Boucheneb Hanifa Laboratoire VeriForm, Department of Computer Engineering, École Polytechnique de Montréal, Station Centre-ville, P.O. Box 6079, H3C 3A7, Montréal, Québec, Canada aut NATIONALLICENCE 700 1- Barkaoui Kamel Laboratoire CEDRIC, Conservatoire National des Arts et Métiers, 292 rue Saint Martin, Paris, Cedex 03, France aut NATIONALLICENCE 773 0- Discrete Event Dynamic Systems Springer US; http://www.springer-ny.com 21/2(2011-06-01), 171-204 0924-6703 21:2<171 2011 21 10626 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer