无序数据Petri网在PTime中的连续可达性
Continuous Reachability for Unordered Data Petri nets is in PTime
摘要：
无序数据Petri网（UDPN）是经典Petri网的扩展，带有从无限域携带数据的令牌，其中变迁可以检查令牌的相等和不相等。UDPN具有良好的结构，因此其可覆盖性和可终止性问题是可判定的，但其复杂性高于Petri网。另一方面，UDPN的可达性问题令人惊讶地复杂，其可判定性状态仍然是开放的。在本文中，我们考虑了UDPN的连续可达性问题，它可以被看作是可达性问题的过近似。我们的主要结果是UDPN的连续可达性和多项式时间算法求解它的一个特征。这是一个组合参数的结果，它表明，如果连续可达性保持，那么存在一个运行只使用多项式多个数据值。
英文摘要：
Unordered data Petri nets (UDPN) are an extension of classical Petri nets with tokens that carry data from an infinite domain and where transitions may check equality and disequality of tokens. UDPN are well-structured, so the coverability and termination problems are decidable, but with higher complexity than for Petri nets. On the other hand, the problem of reachability for UDPN is surprisingly complex, and its decidability status remains open. In this paper, we consider the continuous reachability problem for UDPN, which can be seen as an over-approximation of the reachability problem. Our main result is a characterization of continuous reachability for UDPN and polynomial time algorithm for solving it. This is a consequence of a combinatorial argument, which shows that if continuous reachability holds then there exists a run using only polynomially many data values.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
