Symbolic State Space of Stopwatch Petri Nets with Discrete-Time Semantics (Theory Paper)

In this paper, we address the class of bounded Petri nets with stopwatches (SwPNs), which is an extension of T-time Petri nets (TPNs) where time is associated with transitions. Contrary to TPNs, SwPNs encompass the notion of actions that can be reset, stopped and started. Models can be defined either with discrete-time or dense-time semantics. Unlike dense-time, discrete-time leads to combinatorial explosion (state space is computed by an exhaustive enumeration of states). We can however take advantage from discrete-time, especially when it comes to SwPNs: state and marking reachability problems, undecidable even for bounded nets, become decidable once discrete-time is considered. Thus, to mitigate the issue of combinatorial explosion, we now aim to extend the well-known symbolic handling of time (using convex polyhedra) to the discrete-time setting. This is basically done by computing the state space of discrete-time nets as the discretization of the state space of the corresponding d...

• Type: Conference
• Year: 2008
• Where: APN
• Authors: Morgan Magnin, Didier Lime, Olivier H. Roux
• Keywords: APN 2008, Artificial Intelligence, Discrete-time, Discrete-time Net, State Space