We look in detail at the structural liveness problem (SLP) for subclasses of Petri nets, namely immediate observation nets (IO nets) and their generalized variant called branching immediate multi-observation nets (BIMO nets), that were recently introduced by Esparza, Raskin, and Weil-Kennedy. We show that SLP is PSPACE-hard for IO nets and in PSPACE for BIMO nets. In particular, we discuss the (small) bounds on the token numbers in net places that are decisive for a marking to be (non)live.
翻译:我们详细研究Petri网的子类的结构性活性问题(SLP),即最近由Esparza、Raskin和Weil-Kennedy引入的立即观察网(IO网)及其称为分支立即多观察网(BIMO网)的广义变体。我们证明SLP对于IO网是PSPACE难的,对于BIMO网是PSPACE。特别是,我们讨论了对于标记是(非)活性的关键性标网站的标记令牌数量(小)边界。