We address the class of Time Petri Nets (TPNs) where time intervals are associated with transitions and constrain when those transitions can be fired. For TPN with strong semantics, i.e. where time elapsing cannot disable transitions, reachability, coverability and boundedness problems are undecidable. They are however decidable with the weak semantics in which time elapsing can disable transitions. We first propose an intermediate semantics allowing us to study the decidability border between weak and strong semantics. We prove that with only one transition in strong semantics, reachability, coverability and boundedness are undecidable. We then consider the so-called read, reset and transfer arcs for which the coverability problem is decidable in the untimed context and we study their impact on TPN with a weak semantics (weak TPN). We prove that coverability becomes undecidable for weak TPN when we add either 2 read arcs, or 2 reset arcs, or 2 transfer arcs. Lastly, considering bounded nets, we propose a state space computation algorithm for weak TPN with read, reset and transfer arcs that proves the decidability of the reachability problem.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Decidability Problems for Weak Time Petri Nets with Read, Reset and Transfer Arcs

  • Didier Lime,
  • Rémi Parrot,
  • Olivier H. Roux

摘要

We address the class of Time Petri Nets (TPNs) where time intervals are associated with transitions and constrain when those transitions can be fired. For TPN with strong semantics, i.e. where time elapsing cannot disable transitions, reachability, coverability and boundedness problems are undecidable. They are however decidable with the weak semantics in which time elapsing can disable transitions. We first propose an intermediate semantics allowing us to study the decidability border between weak and strong semantics. We prove that with only one transition in strong semantics, reachability, coverability and boundedness are undecidable. We then consider the so-called read, reset and transfer arcs for which the coverability problem is decidable in the untimed context and we study their impact on TPN with a weak semantics (weak TPN). We prove that coverability becomes undecidable for weak TPN when we add either 2 read arcs, or 2 reset arcs, or 2 transfer arcs. Lastly, considering bounded nets, we propose a state space computation algorithm for weak TPN with read, reset and transfer arcs that proves the decidability of the reachability problem.