Priced Timed Petri Nets
我们考虑定价时间Petri网，即，无界Petri网，其中每个令牌携带一个实值时钟。过渡弧标记有时间间隔，这指定了对令牌年龄的约束。此外，我们的成本模型将每时间单位的令牌存储成本分配给地点，并将发射成本分配给转换。这个一般模型严格包含定价时间自动机和无界定价Petri网。我们研究的成本计算，达到一个给定的控制状态。通常，由于时间约束的严格不等式，具有最小成本的计算可能不存在。然而，我们表明，达到一个给定的控制状态的成本的下确界是可计算的情况下，所有的地方和过渡成本是非负的。另一方面，如果允许负成本，那么给定的控制状态是否以零总成本可达的问题变得不可判定。事实上，即使在离散时间的简单情况下（即，整数值时钟）。
2013-11-09 cs.FL cs.LO
ω-Petri nets
我们介绍了ω-Petri网（ωPN），一个扩展的普通Petri网与ω-标记的输入和输出弧，这是非常适合于分析参数并发系统与动态线程创建。在普通Petri网环境中提出的大多数技术（例如Karp和Miller树或Rackoff技术）并不直接适用于ωPN，因为ωPN定义了具有无限分支的转移系统。这激发了对ωPN的计算方面的彻底分析。我们表明，ωPN可以变成一个普通的Petri网，允许恢复的可达集的ωPN，但不保持终止。这就产生了ωPN上的可达性、（位置）有界性和可覆盖性问题的复杂性界。我们提供了一个实用的算法来计算一个覆盖集的ωPN和决定终止适应经典的Karp和Miller树的结构。我们还将Rackoff技术应用于ωPN，以获得终止问题的精确复杂度。最后，我们考虑了具有重置弧和转移弧的ωPN的扩展，并展示了这种扩展如何影响上述问题的可判定性和复杂性。
2013-01-28 cs.LO
Parameterized Analysis of Immediate Observation Petri Nets
我们介绍即时观察Petri网，一类感兴趣的研究人口协议（分布式计算模型），和酶化学网络。在这些领域中，相关的分析问题转化为参数化的Petri网问题：具有相同底层网但不同初始标记的Petri网的无限集合是否满足给定的性质。研究了直接观察Petri网的参数化可达性、可覆盖性和活性问题。我们发现，所有这三个问题是在PSPACE的计数约束，一类足够丰富的预期应用程序定义的初始标记的无限集。这是值得注意的，因为当标记集是单例时，问题已经是PSPACE困难的，即，在非参数化的情况下。我们使用这些结果来证明即时观察人口协议的正确性问题是PSPACE完全的，回答了以前的论文中留下的一个问题。
2019-03-28 cs.LO
On the Upward/Downward Closures of Petri Nets
研究了以可覆盖性为接受条件的有限状态自动机（FSA）表示和逼近Petri网语言的向下闭包和向上闭包的规模和计算复杂性。我们将展示如何构建一个FSA识别的Petri网语言的向上封闭的双指数时间，因此，大小是最多的双指数。对于向下闭包，我们证明了最小自动机的大小可以是非本原递归的。在BPP网（Petri网的一个众所周知的子类）的情况下，我们证明了接受向下/向上闭包的FSA可以在指数时间内构造。此外，我们考虑的问题，检查是否一个简单的正则语言是包括在向下/向上的Petri网/BPP网语言的闭包。我们证明了这个问题是EXPSPACE-完全的（resp. NP完全）的情况下的Petri网（分别。BPP网）。最后，我们证明了它是可判定的，是否Petri网语言是向上/向下封闭的。为此，我们证明了一个可以决定是否一个给定的正则语言是一个Petri网覆盖性语言的子集。
2018-04-06 cs.FL cs.LO
Universal Safety for Timed Petri Nets is PSPACE-complete
一个定时网络由任意数量的初始相同的1时钟定时自动机组成，通过握手通信进行交互。在这种情况下，没有唯一的中央控制器，因为所有的自动机最初都是相同的。我们考虑这种无限制定时网络的普遍安全问题，即，验证无论网络的大小如何，坏事件（启用某些给定的转换）都是不可能的。这个普遍的安全问题是时间弧Petri网的存在可覆盖性问题的对偶，即，是否存在多个$m$令牌，使得从给定位置中的$m$令牌开始，并且在其它位置中没有令牌，最终启用某个给定转换。我们证明了这些问题是PSPACE完备的。
2018-06-21 cs.LO
Flatness and Complexity of Immediate Observation Petri Nets
在以前的论文中，我们介绍了即时观察（IO）Petri网，一类感兴趣的研究人口协议和酶化学网络。在本文的第一部分中，我们表明，IO网是全球平坦的，所以他们的安全性能可以检查有效的符号模型检验工具，使用加速技术，如FAST。在第二部分中，我们研究了分支IO网（BIO网），其转换可以创建令牌。BIO网扩展了IO网和无通信网，也称为BPP网，这是一个广泛研究的类别。我们表明，虽然BIO网不再是全球平坦的，他们的可达标记集可能是非半线性的，他们仍然是局部平坦的。因此，BIO网的可覆盖性和可达性问题，甚至是它们的某个集合参数化版本，都在PSPACE中。这使得BIO网的第一个自然网类与非半线性可达性关系，可达性问题是可证明的简单比一般的Petri网。
2020-07-21 cs.LO
Decision Problems for Petri Nets with Names
我们证明了nu-PN，纯名称创建和名称管理的P/T网的扩展的可判定性和不可判定性的结果。通过将具有抑制弧的网的可达性归结为可达性，给出了可达性不可判定性的一个简单证明，从而证明了nu-PN网的表达能力严格优于P/T网。我们证明了nu-PN是结构良好的转移系统。特别地，我们得到了可覆盖性和可终止性的可判定性，从而没有达到图灵机的表达能力。此外，它们是严格良结构的，因此有界性问题也是可判定的。我们考虑两个属性，宽度有界性和深度有界性，分解有界性。宽度有界性已经被证明是可判定的。我们在这里证明深度有界的不可判定性。最后，我们得到阿克曼硬度的结果，我们所有的可判定的决策问题。
2010-11-17 cs.LO
Decidable Models of Recursive Asynchronous Concurrency
异步通信下推系统（ACPS）满足空栈约束（下推进程只能在其栈为空时接收）是一种流行的可判定模型，用于具有异步原子过程调用的递归程序。我们研究放松空栈约束ACPS，允许并发和通信行动在任何堆栈高度，称为形栈约束，从而使更大的一类并发程序进行建模。我们建立了一个紧密的连接ACPS与形栈和一个新的扩展Petri网：网与嵌套着色令牌（NNCTs）。NNCT中的令牌有两种类型：简单和复杂。复杂标记携带任意数量的彩色标记。NNCT的规则可以同步复杂和简单的令牌，将彩色令牌注入复杂令牌，并将指定颜色集的所有令牌弹出到预定义的位置。我们证明了NNCT的可覆盖性问题是塔完全的。据我们所知，NNCT是Petri网的第一个扩展，在具有无限令牌类型集的网类中，具有原始递归可覆盖性。这一结果意味着塔完全覆盖ACPS与形状的堆栈。
2015-01-18 cs.CC cs.LO
Bi-reachability in Petri nets with data
University of Warsaw（华沙大学）
该研究针对带数据的Petri网提出双向可达性问题的判定过程，明确其介于可判定的覆盖性问题与可判定性未知的可达性问题之间，推进了相关可判定性边界研究。
2024-07-11 cs.CL cs.FL cs.LO
On Petri Nets with Hierarchical Special Arcs
我们研究的可判定性的终止性，可达性，覆盖性和死锁的Petri网赋予了一个层次的地方，并与抑制弧，复位弧和转移弧，尊重这一层次。我们还研究了当我们有这些特殊的弧，其中一些尊重层次结构，而其他人不混合时会发生什么。我们解决了上述四个问题的可判定性状态的层次，抑制，重置和转移弧的所有组合，除了两个组合的终止问题。对于这两种组合，我们表明，终止问题是很难决定线性递归序列的积极性-一个长期存在的开放问题。
2017-07-04 cs.FL cs.LO
Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness
我们考虑密集时间Petri网（TPN），Petri网的扩展，其中每个令牌配备有实值时钟，并且语义是懒惰的（即，启用的转换不需要触发;时间可以流逝并禁用转换）。我们考虑了主题方案网络的下列核查问题。(i)Zenoness：是否存在来自给定标记的Zeno计算，即，只需要有限时间的无限计算。我们展示了TPN的zenoness的可判定性，从而解决了[Escrig et al.]的一个开放问题。此外，相关的问题，如果存在任意快速计算从一个给定的标记也是可判定的。另一方面，普遍的zenoness，即，如果所有来自给定标记的无限计算都是zeno，则问题是不可判定的。(ii)Token liveness：标记中的token是否存活，即，是否存在来自标记的最终消耗令牌的计算。我们通过将问题简化为可覆盖性问题来显示问题的可判定性，这对于TPN是可判定的。(iii)有界性：可达标记的大小是否有界。我们考虑两个版本的问题，即语义有界性，只有活令牌被考虑在标记，和语法有界性，也死令牌被认为是。我们展示了语义有界性的不可判定性，同时我们证明了句法有界性是可判定的，通过扩展的Karp-Miller算法。
2007-01-23 cs.LO
The Complexity of Coverability-Like Problems in Elementary Object Systems: Data-Nets to the Rescue
Free University of Bozen-Bolzano（博尔扎诺自由大学）；Chennai Mathematical Institute（金奈数学研究所）；IIT Dharwad（达瓦德印度理工学院）
该研究针对基本对象系统（EOSs）的类覆盖问题，将其归约为数据网中通道-νPNs的对应问题，得出保守EOSs覆盖性为$\text{F}_{\text{ω2}}$完全、终止性和有界性非原始递归的结论。
2026-09-01 cs.CC cs.FL cs.LO
Compositional model checking of concurrent systems, with Petri nets
组合性和进程等价性都是进程代数的标准概念。复合性意味着一个复合系统的行为只依赖于其组成部分的行为，即没有涌现行为。过程等价意味着系统的显式状态空间让位于其交互模式：环境可以通过交互获得的信息。Petri网是一个经典的，但被广泛使用和理解的并发模型。然而，它们经常被描述为非组合模型，并且工具倾向于处理整体的、全局指定的模型。本教程论文集中在Petri网与边界（PNB）：1-安全网的合成，图形代数，以及其应用程序中的可达性检查工具彭罗斯。该算法的特点是使用组合性和进程等价，一个强大的组合，可以利用，以提高性能的检查可达性和覆盖性在几个常见的例子，其中Petri网模型现实的并发系统。
2016-03-03 cs.FL cs.LO cs.SE
Nets-within-Nets through the Lens of Data Nets
本文将保守基本对象系统的覆盖性问题精确归约到数据网的一个中间片段，从而桥接网中网与数据网两种 Petri 网扩展方法，并据此确定其复杂度介于 F_{ω2} 与 F_{ω^ω} 之间。
2025-07-02 cs.CC cs.FL cs.LO
The Reachability Problem for Petri Nets is Not Elementary
Petri网，也被称为向量加法系统，是一种建立已久的并发模型，广泛应用于硬件，软件和数据库系统以及化学，生物和商业过程的建模和分析。Petri网的核心算法问题是可达性：从给定的初始配置是否存在一系列有效的执行步骤，达到给定的最终配置。这个问题的复杂性自20世纪60年代以来一直没有得到解决，它是验证理论中最突出的开放问题之一。可判定性是由Mayr在他的开创性的STOC 1981工作中证明的，目前最好的已发表的上限是LICS 2019的Leroux和Schmitz的非原始递归阿克曼。我们建立了一个非初等的下界，即可达性问题需要一个时间和空间的指数塔。直到这项工作，最好的下界一直是指数空间，由于利普顿在1976年。新的下界是一个重大突破，原因有几个。首先，它表明可达性问题比可覆盖性问题困难得多（即，状态可达性）问题，这也是普遍存在的，但自20世纪70年代后期以来，已知对于指数空间是完备的。其次，它意味着大量的问题，从形式语言，逻辑，并发系统，过程演算和其他领域，这是已知的承认减少从Petri网的可达性问题，也不是基本的。第三，它使目前最好的下界的可达性问题的两个关键扩展的Petri网：分支和下推栈。
2019-04-11 cs.FL cs.LO
Timed Basic Parallel Processes
时间基本并行进程（TBPP）扩展了无通信Petri网（aka。BPP或交换上下文无关文法）。TBPP可以被看作是具有上下文无关分支规则的时间自动机（TA）的扩展，因此可以用于对具有进程创建的独立时间自动机的网络进行建模。我们发现，覆盖性和可达性问题（一元编码的目标多重性）是PSPACE完全和EXPTIME完全，分别。对于1时钟TBPP的特殊情况，两者都是NP完全的，因此并不比不定时的BPP更复杂。这与已知的超阿克曼完整性和不可判定性的一般时间Petri网的结果。由于独立的兴趣，和我们的NP上界的基础上，我们表明，1-时钟TA的可达性关系可以表示的多项式大小的线性算术的存在片段的公式，这改善了最近的结果从文献中。
2019-07-08 cs.FL cs.LO
