### Thomas Chatain

* Distribcom research group, IRISA Rennes Cedex, France.
*
**Time: Thursday 18.5.2006, 15:00**

**Place: Room C3-204, Fr. Bajersvej 7**

###
Symbolic unfoldings of time Petri nets

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''.