Complete Finite Prefixes of Symbolic Unfoldings of Safe Time Petri Nets

Abstract. Time Petri nets have proved their interest in modeling realtime 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".

• Type: Conference
• Year: 2006
• Where: APN
• Authors: Thomas Chatain, Claude Jard
• Keywords: APN 2006, Artificial Intelligence, Place/transition Bounded Nets, Realtime Concurrent Systems, Time Petri Nets