In: Lecture Notes in Computer Science : Petri Nets and Other Models of Concurrency - ICATPN 2006, Volume 4024, 2006, pages 125-145. 2006. URL: http://dx.doi.org/10.1007/117675898.
Abstract: Time Petri nets have proved their interest in modeling real-time concurrent systems. Their usual semantics is defined in term of firing sequences, which can be coded in a (symbolic and global) state graph, computable from a bounded net. An alternative is to consider a partial order semantics given in term of processes, which keep explicit the notions of causality and concurrency without computing arbitrary interleavings. In ordinary place/transition bounded nets, it has been shown for many years that the whole set of processes can be finitely represented by a prefix of what is called the unfolding. This paper defines such a prefix for safe time Petri nets. It is based on a symbolic unfolding of the net, using a notion of partial state.