Coverability, Termination, and Finiteness in Recursive Petri Nets
本文证明递归Petri网的可覆盖性、终止性、有界性和有限性问题均为EXPSPACE完全，且其可覆盖性语言严格包含Petri网与上下文无关语言的并集，从而免费获得更强模型。
2021-12-20 cs.FL cs.LO
Transformation From Legal-marking Set to Admissible-marking Set of Petri Nets With Uncontrollable Transitions
在含有不可控变迁的Petri网中，线性约束变换是解决禁止状态问题的关键步骤。本文研究了在这种网的情况下，从合法标记集到其容许标记集的等价变换。首先，定义了逃逸标记集和变换标记集的概念。在此基础上，给出了线性约束的可允许标记集和变换标记集的计算算法，为线性约束的等价变换奠定了理论基础。其次，建立了具有不可控变迁的Petri网的线性约束条件之或的等价变换理论。第三，给出了两个规则来确定转换的优先级。最后，通过两个例子说明了从一个给定的线性约束到一个能描述其整个容许标记集的线性约束逻辑表达式的转换过程。
2015-01-20 cs.FL
Petri Nets and Bio-Modelling - and how to benefit from their synergy
在这次演讲中，我们关注的是一方面Petri网与另一方面膜系统和反应系统之间的内在相似性和差异。
2011-08-17 cs.DC cs.FL
Well-Formed Free-Choice Petri Nets Revisited
Palacký University Olomouc（帕尔察基大学）；Carl von Ossietzky Universität Oldenburg（奥尔登堡卡尔·冯·奥西茨基大学）；Université Libre de Bruxelles（布鲁塞尔自由大学）
本文重新审视自由选择Petri网的well-formed性质，引入半T组件概念并推导经典定理及对偶定理。
2026-07-31 cs.FL
Correctness Notions for Petri Nets with Identifiers
Utrecht University（乌得勒支大学）；Technical University of Denmark（丹麦技术大学）；Free University of Bozen-Bolzano（博尔扎诺自由大学）；The University of Melbourne（墨尔本大学）
本文提出适用于描述信息系统的Petri网扩展形式，探讨了资源和对象感知信息系统的正确性标准，并讨论了其在特定系统类中的可判定性。
2024-01-18 cs.FL
Acyclic Petri and Workflow Nets with Resets
本文提出两类带重置的无环Petri网新子类，证明其可覆盖性或可达性问题复杂度从Ackermann难/不可判定降至PSPACE完全，为相关问题求解提供了可处理的网类。
2023-11-06 cs.FL cs.LO
Decidability Issues for Petri Nets -- a survey
该文系统梳理Petri网25年可判定性研究，汇集重要性质、等价概念及时序逻辑可判定性的核心成果。
2024-11-03 cs.DC cs.FL
Time Delays in Membrane Systems and Petri Nets
研究了具有显式资源和并行性的形式主义中的时间方面，并提出了时间膜系统和具有局部性的时间Petri网之间的形式联系。对于这两种形式主义，时间并没有增加表达能力;然而，时间膜系统和时间Petri网在描述时间是关键资源的分子现象时更加灵活。我们建立了时间膜系统和时间Petri网与地方之间的联系，并证明了它们之间的操作对应关系。
2011-07-06 cs.DC cs.FL
On the Topological Complexity of omega-Languages of Non-Deterministic Petri Nets
我们证明了具有Büchi接受条件的非确定Petri网或等价的Büchi盲计数器自动机可以接受无限词的$Σ_3^0$ -完全语言.这表明非确定性Petri网所接受的Omega语言在拓扑上比确定性Petri网所接受的Omega语言更复杂。
2014-01-27 cs.CC cs.FL cs.LO
Converting Reconfigurable Petri Nets to Maude
模型检验是理论计算机科学的一个重要研究方向。它可以验证具有一组属性（如活性，死锁或安全性）的模型。典型的建模技术之一是Petri网，它们被很好地理解并且可以用于模型检验。可重构Petri网是基于一组规则的Petri网。这些规则可以动态地用于改变网络。缺少的是验证可重构网络和死锁或活性等属性的可能性。本文介绍了一个转换可重构Petri网Maude，使我们能够填补空白。提出了一种基于Maude方程-重写逻辑和LTLR模型检验器的网变换方法。
2014-11-12 cs.FL cs.LO
Toward uniform random generation in 1-safe Petri nets
研究了1-安全Petri网无限执行空间上的一致测度的概念。在这里，1-安全Petri网的执行被理解为并发转换的交换，这引入了一个挑战相比，通常的过渡系统。我们得到的随机生成的无限执行减少到一个有限状态马尔可夫链的模拟。讨论了生物学问题。
2017-06-19 cs.DM cs.FL
Biologically Inspired Process Calculi, Petri Nets and Membrane Computing
本卷代表了第五届膜计算和生物启发过程演算研讨会（MeCBIC 2011）的会议记录，该研讨会于2011年8月23日在法国枫丹白露举行的第12届膜计算国际会议上举行。
2011-08-17 cs.DC cs.FL
Petri Nets for Concurrent Programming
并发程序设计用于所有大型和复杂的计算机系统。然而，并发错误和系统故障（例如：崩溃和死锁）是常见的。我们发现，Petri网可以用来建模并发系统，发现和删除错误提前。我们引入了一种新的广义的Petri网与不确定的过渡节点，以匹配真实的系统。这些允许以紧凑的方式在并发级别构造、优化和证明计算机程序。Petri网程序也可以通过自动求解最大并发来优化，其中有效线程的最大数量由执行之前的Petri网结构确定。本文讨论了一种计算给定Petri网起始状态对的状态图的算法。我们介绍我们的开源软件框架，实现这一理论作为一个通用的并发集中的中间件。
2022-10-01 cs.DC cs.FL
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
Persistent Permutability in Choice Petri Nets
Carl von Ossietzky Universität Oldenburg（奥尔登堡卡尔·冯·奥西茨基大学）；Université Libre de Bruxelles（布鲁塞尔自由大学）
研究了选择Petri网中的持久可交换性，证明了某些类别的Petri网中持久可交换性可推导出整体持久性。
2026-06-05 cs.DM cs.FL
Relating Reversible Petri Nets and Reversible Event Structures, categorically
本文扩展因果网以支持非对称冲突，范畴化地构造其可逆版本，并建立其与可逆非对称事件结构范畴之间的对应关系。
2025-06-03 cs.FL cs.LO
Categories of Nets
我们提出了一个统一的框架，Petri网和各种变体，如前网和科克的全粒Petri网。我们的框架是基于一个较少研究的概念，我们称之为$Σ$ -网，它允许更好地控制是否使用集体或个人令牌的哲学令牌处理。我们描述了三种形式的执行语义，其中前网生成严格的monoidal类别，$Σ$ -网（包括全粒Petri网）生成对称严格的幺半范畴，和Petri网生成交换的幺半范畴，所有的左伴随函子。我们还构建了这些类别的网络相互关联的解释，特别是表明，所有类型的网络可以嵌入在统一的类别的$Σ$ -网，在某种程度上，他们的执行语义一致的通勤。
2021-04-26 cs.FL math.CT
Bi-reachability in Petri nets with data
University of Warsaw（华沙大学）
该研究针对带数据的Petri网提出双向可达性问题的判定过程，明确其介于可判定的覆盖性问题与可判定性未知的可达性问题之间，推进了相关可判定性边界研究。
2024-07-11 cs.CL cs.FL cs.LO
Parameterized complexity results for 1-safe Petri nets
我们将一个图与一个1-安全的Petri网，并研究了各种问题的参数化复杂性与参数来自图。以树宽为参数，对1-安全Petri网的许多问题给出了W[1]-硬度结果。作为一个推论，这证明了唐尼等人的一个猜想。关于一些图卵石问题的硬度。我们考虑了参数效益深度（这是已知的，是有助于获得更好的算法一般Petri网），并再次给出了W[1]-硬度的结果，各种问题的1-安全Petri网。我们还考虑了更强的参数顶点覆盖数。结合著名的自动机理论方法和一元线性规划的固定参数易处理性（FPT）结果，给出了1-安全Petri网上一元二阶（MSO）公式模型检验的FPT算法，参数为公式的顶点覆盖数和大小.
2011-06-10 cs.CC cs.DS cs.FL
Priced Timed Petri Nets
我们考虑定价时间Petri网，即，无界Petri网，其中每个令牌携带一个实值时钟。过渡弧标记有时间间隔，这指定了对令牌年龄的约束。此外，我们的成本模型将每时间单位的令牌存储成本分配给地点，并将发射成本分配给转换。这个一般模型严格包含定价时间自动机和无界定价Petri网。我们研究的成本计算，达到一个给定的控制状态。通常，由于时间约束的严格不等式，具有最小成本的计算可能不存在。然而，我们表明，达到一个给定的控制状态的成本的下确界是可计算的情况下，所有的地方和过渡成本是非负的。另一方面，如果允许负成本，那么给定的控制状态是否以零总成本可达的问题变得不可判定。事实上，即使在离散时间的简单情况下（即，整数值时钟）。
2013-11-09 cs.FL cs.LO
On Petri Nets with Hierarchical Special Arcs
我们研究的可判定性的终止性，可达性，覆盖性和死锁的Petri网赋予了一个层次的地方，并与抑制弧，复位弧和转移弧，尊重这一层次。我们还研究了当我们有这些特殊的弧，其中一些尊重层次结构，而其他人不混合时会发生什么。我们解决了上述四个问题的可判定性状态的层次，抑制，重置和转移弧的所有组合，除了两个组合的终止问题。对于这两种组合，我们表明，终止问题是很难决定线性递归序列的积极性-一个长期存在的开放问题。
2017-07-04 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
Goal-Driven Unfolding of Petri Nets
在探索Petri网的运行时，展开提供了一种有效的方法来避免由于并发变迁的交织而导致的状态空间爆炸。适当阶理论允许定义包含所有可达标记的展开的有限前缀。在本文中，我们感兴趣的是一个单一的给定标记，称为目标的可达性。我们提出了一个算法，用于计算一个1-安全的Petri网，保持达到这一目标的所有最小配置的展开的有限前缀。该算法将展开技术与动态模型降阶技术相结合，通过静态分析来降低模型降阶，避免了对不必要分支的探索。我们提出了一些实验结果。
2016-11-04 cs.FL cs.LO
On Functions Weakly Computable by Pushdown Petri Nets and Related Systems
本文研究文法控制向量加法系统（GVASes）弱可计算的函数，证明其能计算快速增长函数但无法计算逆函数或次线性函数，基于独立有趣的泵引理。
2019-12-17 cs.FL cs.LO
Soundness in Object-centric Workflow Petri Nets
HSE University（俄罗斯国立高等经济大学）；Free University of Bozen-Bolzano（博尔扎诺自由大学）
最近引入的基于Petri网的形式主义主张的情况下，对象的适当表示和管理，以及他们的共同进化的重要性。在这项工作中，我们建立在这样的形式主义之一，并介绍了它的概念的合理性。我们证明，对于网的情况下对象之间的非确定性同步，合理性问题是可判定的。
2021-12-30 cs.AI cs.FL cs.LO
Small Universal Petri Nets with Inhibitor Arcs
研究了带抑制弧的小型通用Petri网的构造问题。我们考虑了四个概念复杂度参数：位置数、转换数、抑制弧数和转换的最大程度，我们试图使每个参数最小化。我们给出了六个结构具有以下参数值（按上述顺序列出）：$(30,34,13,3)$，$(14, 31, 51, 8)$，$(11, 31, 79, 11)$，$(21,25,13,5)$，$(67, 64, 8, 3)$，$(58, 55, 8, 5)$，改善了少数已知的结果在这个主题上。我们的调查还强调了几个有趣的权衡。
2013-12-16 cs.CC cs.DM cs.FL
Synthesis of Reduced Asymmetric Choice Petri Nets
一个Petri网是无选择的，如果任何地方有最多一个转移在其后集（消耗其令牌），它是（扩展）自由选择（EFC），如果任何两个地方的后集是相等的或不相交的。非对称选择（AC）扩展了EFC，使得两个位置也可以具有一个包含在另一个中的后置集。在简化的AC网中，这种包容是有限的：如果后集既不不相交也不相等，则一个是单例，另一个正好有两个转换。Petri网综合的目的是在某个目标类中找到一个非标号Petri网，它的可达图同构于给定的有限标号变迁系统。无选择网具有强大的属性，允许经常容易地检测合成何时失败或至少加速合成。以EFC为目标类，只有少数属性可以提前检查，似乎没有捷径降低合成的复杂性（与任意Petri网相比）。对于AC网络，根本没有已知的合成过程。我们在这里展示了如何合成一个超类的减少AC网（不包含完整的AC网类）可以完成。
2019-11-22 cs.CC cs.DS cs.FL
A Categorical Semantics for Hierarchical Petri Nets
我们展示了如何一个特定的各种层次网，在父网络中的过渡发射必须对应于在一些子网络中的执行，可以利用一个函子语义建模从一个自由的类别-代表父网络-到集范畴类和它们之间的跨度。这种语义可以通过Grothendieck构造内在化，从而产生表示整个层次网的语义的Petri网的执行类别。最后，我们给出了一个面向工程的概述，说明我们的分层网络模型如何在基于交易的智能合约环境中实现。
2021-12-21 cs.DC cs.FL math.CT
Deciding Detectability for Labeled Petri Nets
Institute of Mathematics, Czech Academy of Sciences（捷克科学院数学研究所）；Department of Automation, Shanghai Jiao Tong University（上海交通大学自动化系）；Key Laboratory of System Control and Information Processing, Ministry of Education of China（教育部系统控制与信息处理重点实验室）
本文研究了由标记Petri网建模的离散事件系统中强可检测性和弱可检测性的验证问题，证明强可检测性是可判定的而弱可检测性是不可判定的，扩展了现有研究从有限状态自动机到标记Petri网的可检测性验证。
2018-11-29 cs.FL cs.LO cs.SY
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
Modeling and Analysis of Three Properties of Mobile Interactive Systems Based on Variable Petri Nets
由于移动性和频繁断开连接，移动交互系统，如移动机器人系统和移动支付系统的正确性，往往是很难分析。本文介绍了系统的三个重要性质：系统连通性、交互可靠性和数据有效性，并提出了一种基于Petri网VPN的建模和分析方法。对于一个给定的系统，使用VPN构建了一个包括组件网和交互结构网的模型。构件网描述了各构件的内部过程，交互结构网反映了构件之间的动态交互。在此模型的基础上，定义并分析了三个属性。一个实际的移动支付系统的案例研究表明，所提出的方法的有效性。
2021-01-15 cs.FL cs.SY eess.SY
Secret Protection in Labeled Petri Nets
INRIA France（法国国家信息与自动化研究所）
本文将秘密保护问题从有限自动机扩展到带标签Petri网，提出Parikh和指示器两种变体，证明其判定版本为ExpSpace完全，从而排除多项式时间或空间算法的存在。
2025-11-08 cs.FL cs.SY eess.SY
A Categorical Semantics for Bounded Petri Nets
我们提供了一个范畴语义有界Petri网，无论是在集体和个人令牌哲学。在这两种情况下，我们描述了一个网络内部绑定的过程，通过使用comonads构建新的网络执行类别，外部使用lax-monoidal-lax函子。我们的外部语义是非局部的，这意味着令牌被赋予了一些关于网络全局状态的属性。然后，我们证明，在这两种情况下，内部和外部的建设是等效的，通过使用机器建立在顶部的Grothendieck建设。单个令牌的情况更困难，因为它需要更明确地依赖抽象方法。
2022-11-03 cs.FL cs.LO math.CT
Testing experiments on synchronized Petri nets
University of Aix-Marseille（艾克斯-马赛大学）；University of Cagliari（卡利亚里大学）
本文研究了有限状态机模型系统的同步序列计算，提出利用Petri网结构高效计算同步序列的新方法，避免穷举状态空间。
2013-07-09 cs.FL cs.SY eess.SY
The Essence of Petri Net Gluings
本文提出一个在组合Petri网时尊重其语义的范畴框架，并证明其能推广先前通过资源共享或变迁同步进行粘合的方法。
2023-06-26 cs.DC cs.FL math.CT
Critical Observability for Automata and Petri Nets
Palacky University（帕尔茨基大学）；Institute of Mathematics of the Czech Academy of Sciences（捷克科学院数学研究所）
本文研究了自动机和Petri网模型中临界可观测性问题的计算复杂性，证明了对于有限状态自动机，该问题在NL完全；对于自动机网络，问题在PSPACE完全；而对于标记化Petri网，问题不可判定，但当临界状态集为有限或余有限时，问题变得可判定且与Petri网的不可达性问题等难。
2019-04-17 cs.FL cs.SY eess.SY
Discovering Object-Centric Petri Nets
RWTH Aachen University（亚琛工业大学）；Fraunhofer Institute for Applied Information Technology（弗劳恩霍夫应用信息技术研究所）
从事件数据中发现Petri网的技术假设每个事件只有一个案例标识符。这些案例标识符被用来关联事件，由此发现的Petri网旨在描述单个案例的生命周期。事实上，并不存在一个可能的案例概念，而是多个相互交织的案例概念。例如，事件可以指订单、项目、包、客户和产品的混合。一个包可以指多个物品、多个产品、一个订单和一个客户。因此，我们需要假设每个事件都引用一个对象集合，每个对象都有一个类型（而不是一个case标识符）。这种以对象为中心的事件日志更接近于现实生活中的信息系统中的数据。从一个以对象为中心的事件日志，我们要发现一个以对象为中心的Petri网的地方，对应于对象类型和转换，可以消费和生产不同类型的对象的集合。以对象为中心的Petri网可视化了不同类型对象之间的复杂关系。本文讨论了一种新的进程发现方法在PM4Py中实现。正如将要证明的那样，如果需要的话，发现可以用于向下钻取到特定视点的整体过程模型确实是可行的。
2020-10-05 cs.AI cs.FL cs.LG
