Petri Nets and its Polynomials
对于每一个有限Petri网，我们从自然数半环中构造了一个二元系数的交换多项式。我们还提出了一个逆结构，并证明了多项式的乘法对应的产品的相应的Petri网的范畴内的Petri网与Winskel的态射。我们赋予所有的Petri网的集合与Zurski拓扑。
2017-06-25 cs.LO
On Concept of Creative Petri Nets
本文提出了一种新的Petri网形式，它采用了“位置-弧-变迁”三元组和“变迁-弧-位置”三元组作为结构形成单元。根据融合原理，Petri网的分析表示。我们提出了创造性Petri网的概念，它允许在Petri网中实现结构变化的繁殖/删除的结构单元或复合物。
2019-10-17 cs.LO
Semantic Embedding of Petri Nets into Event-B
我们提出了一个嵌入到B抽象系统的Petri网。嵌入是通过翻译的静态结构（建模方面）和Petri网的进化语义。Petri网的静态结构通过图结构在B抽象系统中捕获。这个抽象的系统，然后包含在另一个抽象的系统，捕获的进化语义的Petri网。演化语义的结果取决于所选择的策略：基本网或高级Petri网的一些B事件。目前的嵌入使人们能够在同一系统开发中联合使用Petri网和Event-B，但在不同的步骤和各种分析。
2005-10-24 cs.LO
Priced Timed Petri Nets
我们考虑定价时间Petri网，即，无界Petri网，其中每个令牌携带一个实值时钟。过渡弧标记有时间间隔，这指定了对令牌年龄的约束。此外，我们的成本模型将每时间单位的令牌存储成本分配给地点，并将发射成本分配给转换。这个一般模型严格包含定价时间自动机和无界定价Petri网。我们研究的成本计算，达到一个给定的控制状态。通常，由于时间约束的严格不等式，具有最小成本的计算可能不存在。然而，我们表明，达到一个给定的控制状态的成本的下确界是可计算的情况下，所有的地方和过渡成本是非负的。另一方面，如果允许负成本，那么给定的控制状态是否以零总成本可达的问题变得不可判定。事实上，即使在离散时间的简单情况下（即，整数值时钟）。
2013-11-09 cs.FL cs.LO
On Concept of Petri Nets Receptors and Effectors
介绍了Petri网的新子类-- Petri网受体和Petri网效应子。在主Petri网中引入/排除这样的子结构可以根据融合/去融合原则来实现。我们提出了两对实体：位置标记受体（效应器）和过渡标记受体（效应器），它允许观察主Petri网的参数，如果必要的话，进行调节。
2019-12-18 cs.LO
On Petri Nets with Hierarchical Special Arcs
我们研究的可判定性的终止性，可达性，覆盖性和死锁的Petri网赋予了一个层次的地方，并与抑制弧，复位弧和转移弧，尊重这一层次。我们还研究了当我们有这些特殊的弧，其中一些尊重层次结构，而其他人不混合时会发生什么。我们解决了上述四个问题的可判定性状态的层次，抑制，重置和转移弧的所有组合，除了两个组合的终止问题。对于这两种组合，我们表明，终止问题是很难决定线性递归序列的积极性-一个长期存在的开放问题。
2017-07-04 cs.FL cs.LO
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
On Distributability of Petri Nets
我们正式的分布式系统的一般概念，顺序组件异步交互。我们定义了一个相应的类的Petri网，称为LSGA网，并精确地将这些系统规范，可以实现为LSGA网分支ST-双相似性与明确的分歧。
2012-07-16 cs.LO
Reachability via Compositionality in Petri nets
我们介绍了一种新的技术，检查Petri网的可达性，依赖于最近推出的组合代数网。我们证明了该技术是正确的，并讨论了我们的实现。我们报告一些著名的例子有希望的实验结果。
2014-04-21 cs.LO
Subtyping for Hierarchical, Reconfigurable Petri Nets
层次Petri网允许更抽象的视图和可重构Petri网模型的动态结构适应。在这方面的贡献，我们提出了可重构Petri网和层次Petri网的组合产生层次结构的可重构Petri网。层次结构是通过将转换替换为“转换”来建立的。这些对象本身是可重新配置的，因此它们被提供了自己的规则集。此外，提供了可以应用于所有网络的全局规则。
2018-02-13 cs.DM cs.LO
Dialectica Fuzzy Petri Nets
Brown和Gurr在de~Paiva的Dialectica范畴的基础上提出了一种Petri网模型。该模型在一份未发表的技术报告中得到了改进，其中使用了具有多重性的Petri网，而不是{ \em基本}网（即，只考虑多重性为0和1的网）。在这篇文章中，我们扩展了这种建模来处理{ \em模糊} Petri网。其基本思想是使用具有{ \em lineale}结构的所有属性的单位区间作为Dialectica范畴结构中的对偶对象。
2020-03-08 cs.LO
Efficient Restrictions of Immediate Observation Petri Nets
在以前的论文中，我们介绍了即时观察Petri网，Petri网的一个子类，在分布式协议（人口协议）和理论化学（化学反应网络）中具有应用领域。IO网具有许多有用的性质，但与保守Petri网一样，它们也存在PSPACE完全可达性问题。在本文中，我们探讨了IO网的可达性问题的两个限制，大大降低了问题的复杂性。对于分布式协议中的应用，第一个限制的复杂性是NP完全的，对于化学环境中的应用，第二个限制的复杂性是多项式的。
2020-10-08 cs.LO
A Web Interface for Petri Nets with Transits and Petri Games
为分布式系统开发算法是一项容易出错的任务。形式化的模型，如Petri网与过境和Petri游戏可以防止错误时，开发这样的算法。带变迁的Petri网允许我们跟踪分布式系统中组件之间的数据流。它们可以根据LTL中的规范在本地数据流和全局行为上进行模型检查。Petri游戏允许从安全规范的分布式系统的本地控制器的合成。在这些形式主义建模问题需要定义扩展的Petri网，这可能是繁琐的文本执行时。在本文中，我们提出了一个Web界面，允许一个直观的，可视化的定义Petri网与过境和Petri游戏。相应的模型检验和综合问题直接在服务器上求解。在界面中，可以分析和模拟实现，反例和所有中间步骤。逐步模拟和交互式状态空间生成支持用户检测建模错误。
2021-03-29 cs.LO
Analysis of Petri Nets and Transition Systems
本文介绍了一个独立的，没有装饰的工具，支持（标记）的地方/过渡Petri网的分析和标记的过渡系统到Petri网的合成。它被实现为一个独立的，专用的算法的集合，这些算法被设计为模块化，可移植，可扩展和有效地操作。
2015-08-20 cs.LO
Bi-reachability in Petri nets with data
University of Warsaw（华沙大学）
该研究针对带数据的Petri网提出双向可达性问题的判定过程，明确其介于可判定的覆盖性问题与可判定性未知的可达性问题之间，推进了相关可判定性边界研究。
2024-07-11 cs.CL cs.FL cs.LO
A general translation from nested Petri nets into PROMELA
嵌套Petri网已被应用于建模的交互协议，移动性，自适应系统和跨组织的工作流。然而，很少有结果报告使用自动化工具来分析这些网络的行为。在本文中，我们提出了一个一般的翻译，从嵌套Petri网到PROMELA，并解释如何使用SPIN模型检查这些网的一些性质可以研究。此外，我们讨论了如何处理的主要限制，可能会影响SPIN性能时，验证实际的例子。
2014-03-31 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
Petri Nets and Higher-Dimensional Automata
本文重新审视Petri网的高维自动机语义，将翻译扩展至带抑制弧的网和广义自修改网，并提供了实现该翻译的工具。
2025-02-04 cs.LO
Controlling Reversibility in Reversing Petri Nets with Application to Wireless Communications
Petri网是一种对分布式系统的行为进行建模和推理的形式主义。最近，一个可逆的方法，Petri网，反向Petri网（RPN），已被提出，允许转移被逆转自发或因果顺序。在这项工作中，我们提出了一种方法，用于控制RPN的动作的逆转，通过关联过渡的条件，其满足/违反允许执行的过渡在向前/向后的方向，分别。我们说明了一种新的，分布式算法在分布式天线阵列的天线选择模型的框架。
2019-05-28 cs.LO
Structurally Cyclic Petri Nets
一个Petri网在结构上是循环的，如果每一个配置都可以通过一个或多个步骤从它自己到达。我们证明了结构周期性在确定性多项式时间内是可判定的。为此，我们适应Kanghaju的方法一般的可达性问题的Petri网。
2015-12-20 cs.LO
The Reachability Problem for Petri Nets is Not Primitive Recursive
我们提供了一个阿克曼复杂性下界检查程序的可达性问题，一个模型相当于Petri网。此外，在固定维数的$2d+4$中，我们证明了该问题是$\mathbb{F}_d$ -困难的.作为一个直接的推论，10维中的可达性问题不是基本的。
2021-09-02 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
Homology Groups of Pipeline Petri Nets
研究了流水线系统的基本Petri网的同调群。我们证明了这些网在0维和1维上的整同调群等于整数群，并且它们在其他维上为零。我们证明了基本Petri网的有向同调群在所有维度上都为零。
2013-03-01 cs.LO math.AT
Computing Optimal Coverability Costs in Priced Timed Petri Nets
我们考虑时间Petri网，即，无界Petri网，其中每个令牌携带一个实值时钟。过渡弧标记有时间间隔，这指定了对令牌年龄的约束。我们的成本模型将每时间单位的令牌存储成本分配给位置，并将发射成本分配给转换。我们研究的成本达到一个给定的控制状态。一般来说，成本最优运行可能不存在。然而，我们表明，下确界的成本是可计算的。
2011-04-04 cs.LO
Stochastic Decision Petri Nets
我们介绍随机决策Petri网（SDPN），这是一种形式的随机Petri网配备了奖励和控制机制，通过可控转移的失活。这样的网络可以被转化为马尔可夫决策过程（MDP），可能会导致由于并发状态的数量组合爆炸。因此，我们限制自己的情况下，网是安全的，自由选择和无环网（SAFC网），甚至发生网和政策是由一个恒定的失活模式定义的。我们得到的复杂性理论的结果，这种情况下，通过一个紧密的连接到贝叶斯网络，特别是我们表明，SAFC网的问题是否有一个政策，保证奖励高于一定的阈值是$\mathsf{NP}^\mathsf{PP}$ -完成。我们还介绍了一个偏序程序，使用SMT求解器来解决这个问题。
2023-03-23 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
Petri Nets with Time and Cost
我们考虑时间Petri网，即，无界Petri网，其中每个令牌携带一个实值时钟。过渡弧标记有时间间隔，这指定了对令牌年龄的约束。我们的成本模型将每时间单位的令牌存储成本分配给位置，并将发射成本分配给转换。我们研究的成本达到一个给定的控制状态。一般来说，成本最优运行可能不存在。然而，我们表明，下确界的成本是可计算的。
2013-02-14 cs.LO
Decomposing Petri nets
在最近的工作中，第二和第三作者介绍了一种技术的可达性检查1-有界Petri网，基于布线分解，这是一个片段的组合代数的网络与边界的表达式。在这里，我们将该技术推广到全代数，并介绍了有关的结构性质的分解宽度的有向超图。小的分解宽度是必要的可达性检查算法的适用性。我们给出的例子，家庭的网络与恒定的分解宽度和发展的基本理论的分解。
2013-04-10 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
Proposal for Adding Useful Features to Petri-Net Model Checkers
长期存在的问题提出的解决方案的自动分解的Petri网到并发进程，以及在格勒诺布尔开发的方法的自动转换的安全Petri网NUPN（嵌套单元Petri网），需要一定的性能计算的Petri网。我们注意到，虽然这些属性在理论上是有趣的，实际上是有用的，他们目前还没有实现在主流的Petri网工具。考虑到这些属性将为工具开发人员开辟富有成效的研究方向，也为模型检验竞赛开辟新的视角。
2021-01-21 cs.LO
Free Choice Petri Nets without frozen tokens and Bipolar Synchronization Systems
双极同步系统（BP系统）构成了一类有色Petri网，非常适合于离散动态系统的控制流建模。每个BP系统都有一个底层的普通Petri网，它是一个T系统。此外，它还附加了第二个普通网，这是一个自由选择系统。我们证明了BP系统是活的和安全的，如果T系统和自由选择系统是活的和安全的，如果自由选择系统没有冻结令牌。这个结果是Genrich和Thiagarajan的一个定理的逆，并证明了一个老猜想。该证明利用Petri网的态射和自由选择系统的经典理论对不同的Petri网进行了比较
2007-09-10 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
Open Petri Nets
Petri网的可达性语义可以用开放Petri网来研究。对我们来说，一个“开放”的Petri网是一个通过集合的余跨度指定为输入和输出的某些地方。我们可以通过将一个Petri网的输出粘到另一个Petri网的输入来组成开放Petri网。开放Petri网可以看作是范畴$\mathsf{Open}(\mathsf{Petri})$的态射，它在不交并下成为对称幺半群.然而，由于开放Petri网的复合仅定义为同构，因此最好将它们视为对称monoidal双范畴$\mathbb{O}\mathbf{pen}(\mathsf{Petri})$的态射。我们描述了两种形式的语义开放Petri网使用对称monoidal双函子的$\mathbb{O}\mathbf{pen}(\mathsf{Petri})$。第一，一个操作语义，给每个开放的Petri网的范畴，其态射是这个网可以进行的过程。这是以组合的方式完成的，因此这些类别可以在较小的数组上计算，然后粘在一起。第二种是可达性语义，它简单地说，从输入的给定标记可以到达输出的哪些标记。
2022-07-25 cs.LO math.CT
Hardness Results for the Synthesis of $b$-bounded Petri Nets (Technical Report)
一个$τ$型Petri网的合成是下面的搜索问题：对于一个转移系统$A$，找到一个$τ$型的Petri网$N$，它的状态图与$A$同构，如果存在的话。为了确定有界Petri网类型的综合的计算复杂性，我们调查其相应的决策版本，称为可行性。我们证明了当$b\in \mathbb{N}^+$是有界P/T-网时，（纯）$b$ -有界P/T-网的可行性是NP-完全的.我们通过整数模$(b+1)$的加性群$\mathbb{Z}_{b+1}$扩展了（纯）$b$ -有界P/T-网，并证明了所得类型是NP-完全的可行性.为了判定$A$是否具有事件状态分离性质，证明了对于（纯）$b$ -有界和群扩展（纯）$b$ -有界P/T-网，事件状态分离性质是NP-完全的.对于（纯）$b$ -有界P/T-网，证明了判定$A$是否具有状态分离性质是NP-完全的.
2019-03-17 cs.LO
Feedback control logic synthesis for non safe Petri nets
研究了非安全Petri网（PN）建模离散事件系统的禁止状态问题。为了防止被禁止的状态，可以使用与转换相关联的条件或谓词。一般来说，有许多禁戒态，因此许多复杂的条件与过渡。提出了一种计算非安全Petri网谓词的新思想。利用这种方法，我们可以构造一个最大允许控制器，如果它存在。
2010-03-25 cs.LO
Structural Liveness of Conservative Petri Nets
CNRS, Univ. Bordeaux（法国国家科学研究中心，波尔多大学）
研究证明保守Petri网的结构活力问题在保守子类中仍为EXPSPACE难，且结构活的保守网的最小活标记值不超过双指数，从而证明其EXPSPACE完全性。
2026-10-09 cs.LO
Quantum Petri Nets with Event Structures semantics
针对量子并发领域缺乏类似经典佩特里网的规范模型问题，本文引入具有量子赋值的量子佩特里网（QPNs），定义局部量子发生网（LQONs）并构建组合框架，为量子并发建立语义基础。
2025-08-20 cs.LO quant-ph
Model Checking Branching Properties on Petri Nets with Transits (Full Version)
为了对并发系统进行模型检验，区分数据流和控制流是很方便的。正确性是在数据流级别上指定的，而系统是在控制级别上配置的。带变迁的Petri网和Flow-LTL是相应的形式体系。在Flow-LTL中，数据流的正确性以及控制的公平性和最大性的假设都以线性时间表示。到目前为止，分支行为不能指定的Petri网与过境。在本文中，我们引入Flow-CTL* 来表达数据流的预期分支行为，同时保持LTL的公平性和最大化假设的控制。我们编码的物理访问控制与策略更新的Petri网与过境，并给出标准的要求在流CTL *。在模型检验方面，我们通过构造自动机将Flow-CTL* 的带变迁Petri网的模型检验问题归结为LTL的Petri网的模型检验问题。因此，可以验证在无限数量的人的公平性假设下具有策略更新的物理访问控制。
2020-07-14 cs.LO
Quantum Petri Nets with Event Structure semantics
针对量子并发缺乏严格语义与展开理论的问题，提出与量子事件结构语义兼容的量子Petri网（QPNs），通过定义局部量子发生网、构建展开语义及组合框架，建立了语义严谨的量子并发模型，桥接了Petri网理论与量子编程。
2025-09-17 cs.LO quant-ph
Unifying Inference for Bayesian and Petri Nets
作者最近的工作装备Petri发生网（PN）的概率分布，完全取代非确定性。为了避免所谓的混淆问题，这种结构强加了额外的因果依赖关系，限制了某些被称为结构分支单元（s-单元）的选择。贝叶斯网（BN）通常被构造为偏序，其中节点定义条件概率分布。本文用对称Monoidal范畴（SMC）把这两种结构统一起来，使我们能应用于PN的普通分析技术。有趣的是，事实证明，不能被SMC分解的PN正是s-细胞。这一结果证实了SMC和S-细胞的Petri网的重要性。
2018-07-17 cs.LO
Parameterized Analysis of Immediate Observation Petri Nets
我们介绍即时观察Petri网，一类感兴趣的研究人口协议（分布式计算模型），和酶化学网络。在这些领域中，相关的分析问题转化为参数化的Petri网问题：具有相同底层网但不同初始标记的Petri网的无限集合是否满足给定的性质。研究了直接观察Petri网的参数化可达性、可覆盖性和活性问题。我们发现，所有这三个问题是在PSPACE的计数约束，一类足够丰富的预期应用程序定义的初始标记的无限集。这是值得注意的，因为当标记集是单例时，问题已经是PSPACE困难的，即，在非参数化的情况下。我们使用这些结果来证明即时观察人口协议的正确性问题是PSPACE完全的，回答了以前的论文中留下的一个问题。
2019-03-28 cs.LO
SMPT: A Testbed for Reachability Methods in Generalized Petri Nets
SMPT（Satisfiability Modulo Petri Net）是一个用于Petri网可达性问题的模型检测器。它最初是一个试验符号模型检验的方法组合，并被设计为易于扩展。一些独特的功能是它能够从结构简化中受益，并生成判决证书。与模型检验竞赛中的其他最先进的工具相比，我们的工具相当成熟，表现良好。
2023-02-28 cs.LO
Reversible Computation in Cyclic Petri Nets
Petri网是一种用于分布式系统建模和推理的数学语言。在本文中，我们提出了一种方法，Petri网嵌入可逆性，即，在操作过程中的任何一点上，使已执行的操作序列反向的能力。具体而言，我们引入机器和相关的语义来支持三种主要形式的可逆性，即回溯，因果反转，和在循环Petri网的变化，令牌是持久的，并相互区分的身份的顺序颠倒的cabetual。我们的形式主义的影响，在生物化学中的应用，但方法可以应用到广泛的问题，功能可逆性。特别是，我们证明了我们的方法的适用性与ERK信号通路的模型，一个例子，本质上具有可逆的行为。
2020-10-07 cs.LO
AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL (Full Version)
网络的正确性通常用组件的单个数据流来描述，而不是它们的全局行为。在软件定义网络中，指定数据包的正确行为比指定整个网络的全局行为要方便得多。带变迁的Petri网扩展了Petri网，Flow-LTL扩展了LTL，使得令牌的数据流可以被跟踪。我们提出的工具AdamMC作为第一个模型检查器的Petri网与过境对流LTL。我们描述了如何AdamMC可以自动编码并发更新的软件定义的网络作为Petri网的过境和常见的网络规范可以表示在流LTL。底层AdamMC是一个电路模型检验问题的简化。我们引入了一个新的减少方法，结果在巨大的性能改进相比，以前的原型。因此，AdamMC可以处理多达82台交换机的软件定义网络。
2020-05-15 cs.LO
A "Symbolic" Representation of Object-Nets (Extended Version)
本文针对基本对象系统（EOS，一种网中嵌套Petri网的形式体系）状态空间规模大的问题，将Petri网同态扩展至EOS，利用拓扑自同构的对称性压缩状态空间，为嵌套Petri网的状态分析提供了符号化方法。
2024-10-31 cs.LO
Compositional Semantics of Finite Petri Nets
本文针对有限 Petri 网，证明保结构互模拟关于 FMN 算子为同余，并给出尊重因果性与分支结构的组合语义及可靠公理化基础。
2023-08-17 cs.LO
Perpetual Free-choice Petri nets are lucent -- proof of a theorem of van der Aalst using CP-exhaustions
本文通过CP-子网穷举法证明van der Aalst定理，即永久自由选择Petri网是清晰的，并用初等方法分析所得T-系统。
2021-11-10 cs.LO
Structural Liveness of Immediate Observation Petri Nets
本文研究了即时观察网（IO网）及其广义变体BIMO网的结构活性问题，证明了该问题对IO网是PSPACE-hard的，对BIMO网属于PSPACE，并讨论了决定标记活性的令牌数界限。
2023-03-28 cs.LO
Wadge Degrees of $ω$-Languages of Petri Nets
我们证明了$ω$ -语言的（非确定性）Petri网和$ω$ -语言（非确定性）图灵机具有相同的拓扑复杂性：$ω$类的Borel和Wadge层次--（非确定性）Petri网等同于$ω$类的Borel和Wadge层次结构-（非确定性的）图灵机，它也形成了有效分析集的类别。特别地，对于每个非空递归序数$α< ω\_1^{\rm CK} $，存在一些${\bf Σ}^0\_α$ -完全和一些${\bf Π}^0\_α$ -完全的Petri网$ω$ -语言，并且Petri网$ω$ -语言的Borel秩集合的上确界是序数$γ\_2^1$，它严格大于第一个非递归序数$ω\_1^{\rm CK}$ .我们还证明了存在一些${\bf Σ}\_1^1$ -完全的，因而非Borel的Petri网$ω$ -语言，并且与ZFC一致的是，存在一些既不是Borel也不是${\bf Σ}\_1^1$ -完全的Petri网$ω$ -语言.这回答了[DFR 14，FS 14]中未解决的（非确定性）Petri网语言$ω$的拓扑复杂性问题。
2018-03-26 cs.LO math.LO
A Polynomial Translation of pi-calculus FCPs to Safe Petri Nets
我们开发了一个多项式的翻译有限控制π演算过程安全的低级别Petri网。据我们所知，这是第一个这样的翻译。这是自然的，因为有一个密切的对应关系之间的控制流，享有互模拟的结果，并适合于实际的模型检验。
2013-09-16 cs.LO
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
本文证明了（强）全并发互模拟性和i-因果网互模拟性在有限有界Petri网上是可判定的，其核心方法是对Vogler的有序标记证明技术进行推广。
2023-12-20 cs.LO
Homogeneous Equations of Algebraic Petri Nets
代数Petri网是一种用于分布式系统和算法建模的形式主义，通过结合Petri网和代数规范来描述控制和数据流。指定代数Petri网模型$N$的正确性的一种方式是基于项替换和来自阿贝尔群$G$的系数来指定在$N$的位置上的线性方程$E$。然后，$E$在$N$中有效，当且仅当$E$在$N$的每个可达标记中有效。由于代数Petri网的表达能力，有效性通常是不可判定的。稳定的线性方程组形成一类有效性可判定的线性方程组。位置不变量给出了所有稳定线性方程的一个很好理解但不完整的特征。在本文中，我们提供了一个完整的特征的稳定性子类的齐次线性方程，限制自己的解释条款的Herbrand结构，而不考虑进一步的平等公理。在此基础上，证明了当$G$是循环群时，齐次线性方程的稳定性是可判定的.
2016-06-22 cs.LO
A Categorical Semantics for Bounded Petri Nets
我们提供了一个范畴语义有界Petri网，无论是在集体和个人令牌哲学。在这两种情况下，我们描述了一个网络内部绑定的过程，通过使用comonads构建新的网络执行类别，外部使用lax-monoidal-lax函子。我们的外部语义是非局部的，这意味着令牌被赋予了一些关于网络全局状态的属性。然后，我们证明，在这两种情况下，内部和外部的建设是等效的，通过使用机器建立在顶部的Grothendieck建设。单个令牌的情况更困难，因为它需要更明确地依赖抽象方法。
2022-11-03 cs.FL cs.LO math.CT
