首页 | 本学科首页   官方微博 | 高级检索  
     


Decidability and complexity of Petri nets with unordered data
Authors:Fernando Rosa-Velardo  David de Frutos-Escrig
Affiliation:
  • Sistemas Informáticos y Computación, Facultad de Informática, Universidad Complutense de Madrid, C/Profesor José García Santesmases, s/n 28040 Madrid, Spain
  • Abstract:We prove several decidability and undecidability results for ν-PN, an extension of P/T nets with pure name creation and name management. We give a simple proof of undecidability of reachability, by reducing reachability in nets with inhibitor arcs to it. Thus, the expressive power of ν-PN strictly surpasses that of P/T nets. We encode ν-PN into Petri Data Nets, so that coverability, termination and boundedness are decidable. Moreover, we obtain Ackermann-hardness results for all our decidable decision problems. Then we consider two properties, width-boundedness and depth-boundedness, that factorize boundedness. Width-boundedness has already been proven to be decidable. Here we prove that its complexity is also non-primitive recursive. Then we prove undecidability of depth-boundedness. Finally, we prove that the corresponding “place version” of all the boundedness problems is undecidable for ν-PN. These results carry over to Petri Data Nets.
    Keywords:Petri nets  Pure names  Well-structured transition systems  Reachability  Boundedness
    本文献已被 ScienceDirect 等数据库收录!
    设为首页 | 免责声明 | 关于勤云 | 加入收藏

    Copyright©北京勤云科技发展有限公司  京ICP备09084417号