Time: Thursday 18.5.2006, 15:00
Place: Room C3-204, Fr. Bajersvej 7
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''.