Structurally Cyclic Petri Nets
Drewes Frank, Leroux Jérôme
一个Petri网在结构上是循环的，如果每一个配置都可以通过一个或多个步骤从它自己到达。我们证明了结构周期性在确定性多项式时间内是可判定的。为此，我们适应Kanghaju的方法一般的可达性问题的Petri网。
A Petri net is structurally cyclic if every configuration is reachable from itself in one or more steps. We show that structural cyclicity is decidable in deterministic polynomial time. For this, we adapt the Kosaraju's approach for the general reachability problem for Petri nets.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Petri Nets and its Polynomials
对于每一个有限Petri网，我们从自然数半环中构造了一个二元系数的交换多项式。我们还提出了一个逆结构，并证明了多项式的乘法对应的产品的相应的Petri网的范畴内的Petri网与Winskel的态射。我们赋予所有的Petri网的集合与Zurski拓扑。
On Concept of Creative Petri Nets
本文提出了一种新的Petri网形式，它采用了“位置-弧-变迁”三元组和“变迁-弧-位置”三元组作为结构形成单元。根据融合原理，Petri网的分析表示。我们提出了创造性Petri网的概念，它允许在Petri网中实现结构变化的繁殖/删除的结构单元或复合物。
Semantic Embedding of Petri Nets into Event-B
我们提出了一个嵌入到B抽象系统的Petri网。嵌入是通过翻译的静态结构（建模方面）和Petri网的进化语义。Petri网的静态结构通过图结构在B抽象系统中捕获。这个抽象的系统，然后包含在另一个抽象的系统，捕获的进化语义的Petri网。演化语义的结果取决于所选择的策略：基本网或高级Petri网的一些B事件。目前的嵌入使人们能够在同一系统开发中联合使用Petri网和Event-B，但在不同的步骤和各种分析。
On Concept of Petri Nets Receptors and Effectors
介绍了Petri网的新子类-- Petri网受体和Petri网效应子。在主Petri网中引入/排除这样的子结构可以根据融合/去融合原则来实现。我们提出了两对实体：位置标记受体（效应器）和过渡标记受体（效应器），它允许观察主Petri网的参数，如果必要的话，进行调节。
On Distributability of Petri Nets
我们正式的分布式系统的一般概念，顺序组件异步交互。我们定义了一个相应的类的Petri网，称为LSGA网，并精确地将这些系统规范，可以实现为LSGA网分支ST-双相似性与明确的分歧。
Reachability via Compositionality in Petri nets
我们介绍了一种新的技术，检查Petri网的可达性，依赖于最近推出的组合代数网。我们证明了该技术是正确的，并讨论了我们的实现。我们报告一些著名的例子有希望的实验结果。
Dialectica Fuzzy Petri Nets
Brown和Gurr在de~Paiva的Dialectica范畴的基础上提出了一种Petri网模型。该模型在一份未发表的技术报告中得到了改进，其中使用了具有多重性的Petri网，而不是{ \em基本}网（即，只考虑多重性为0和1的网）。在这篇文章中，我们扩展了这种建模来处理{ \em模糊} Petri网。其基本思想是使用具有{ \em lineale}结构的所有属性的单位区间作为Dialectica范畴结构中的对偶对象。
Efficient Restrictions of Immediate Observation Petri Nets
在以前的论文中，我们介绍了即时观察Petri网，Petri网的一个子类，在分布式协议（人口协议）和理论化学（化学反应网络）中具有应用领域。IO网具有许多有用的性质，但与保守Petri网一样，它们也存在PSPACE完全可达性问题。在本文中，我们探讨了IO网的可达性问题的两个限制，大大降低了问题的复杂性。对于分布式协议中的应用，第一个限制的复杂性是NP完全的，对于化学环境中的应用，第二个限制的复杂性是多项式的。
A Web Interface for Petri Nets with Transits and Petri Games
为分布式系统开发算法是一项容易出错的任务。形式化的模型，如Petri网与过境和Petri游戏可以防止错误时，开发这样的算法。带变迁的Petri网允许我们跟踪分布式系统中组件之间的数据流。它们可以根据LTL中的规范在本地数据流和全局行为上进行模型检查。Petri游戏允许从安全规范的分布式系统的本地控制器的合成。在这些形式主义建模问题需要定义扩展的Petri网，这可能是繁琐的文本执行时。在本文中，我们提出了一个Web界面，允许一个直观的，可视化的定义Petri网与过境和Petri游戏。相应的模型检验和综合问题直接在服务器上求解。在界面中，可以分析和模拟实现，反例和所有中间步骤。逐步模拟和交互式状态空间生成支持用户检测建模错误。
Analysis of Petri Nets and Transition Systems
本文介绍了一个独立的，没有装饰的工具，支持（标记）的地方/过渡Petri网的分析和标记的过渡系统到Petri网的合成。它被实现为一个独立的，专用的算法的集合，这些算法被设计为模块化，可移植，可扩展和有效地操作。
A general translation from nested Petri nets into PROMELA
嵌套Petri网已被应用于建模的交互协议，移动性，自适应系统和跨组织的工作流。然而，很少有结果报告使用自动化工具来分析这些网络的行为。在本文中，我们提出了一个一般的翻译，从嵌套Petri网到PROMELA，并解释如何使用SPIN模型检查这些网的一些性质可以研究。此外，我们讨论了如何处理的主要限制，可能会影响SPIN性能时，验证实际的例子。
Petri Nets and Higher-Dimensional Automata
本文重新审视Petri网的高维自动机语义，将翻译扩展至带抑制弧的网和广义自修改网，并提供了实现该翻译的工具。
Controlling Reversibility in Reversing Petri Nets with Application to Wireless Communications
Petri网是一种对分布式系统的行为进行建模和推理的形式主义。最近，一个可逆的方法，Petri网，反向Petri网（RPN），已被提出，允许转移被逆转自发或因果顺序。在这项工作中，我们提出了一种方法，用于控制RPN的动作的逆转，通过关联过渡的条件，其满足/违反允许执行的过渡在向前/向后的方向，分别。我们说明了一种新的，分布式算法在分布式天线阵列的天线选择模型的框架。
The Reachability Problem for Petri Nets is Not Primitive Recursive
我们提供了一个阿克曼复杂性下界检查程序的可达性问题，一个模型相当于Petri网。此外，在固定维数的$2d+4$中，我们证明了该问题是$\mathbb{F}_d$ -困难的.作为一个直接的推论，10维中的可达性问题不是基本的。
Computing Optimal Coverability Costs in Priced Timed Petri Nets
我们考虑时间Petri网，即，无界Petri网，其中每个令牌携带一个实值时钟。过渡弧标记有时间间隔，这指定了对令牌年龄的约束。我们的成本模型将每时间单位的令牌存储成本分配给位置，并将发射成本分配给转换。我们研究的成本达到一个给定的控制状态。一般来说，成本最优运行可能不存在。然而，我们表明，下确界的成本是可计算的。
Stochastic Decision Petri Nets
我们介绍随机决策Petri网（SDPN），这是一种形式的随机Petri网配备了奖励和控制机制，通过可控转移的失活。这样的网络可以被转化为马尔可夫决策过程（MDP），可能会导致由于并发状态的数量组合爆炸。因此，我们限制自己的情况下，网是安全的，自由选择和无环网（SAFC网），甚至发生网和政策是由一个恒定的失活模式定义的。我们得到的复杂性理论的结果，这种情况下，通过一个紧密的连接到贝叶斯网络，特别是我们表明，SAFC网的问题是否有一个政策，保证奖励高于一定的阈值是$\mathsf{NP}^\mathsf{PP}$ -完成。我们还介绍了一个偏序程序，使用SMT求解器来解决这个问题。
Petri Nets with Time and Cost
我们考虑时间Petri网，即，无界Petri网，其中每个令牌携带一个实值时钟。过渡弧标记有时间间隔，这指定了对令牌年龄的约束。我们的成本模型将每时间单位的令牌存储成本分配给位置，并将发射成本分配给转换。我们研究的成本达到一个给定的控制状态。一般来说，成本最优运行可能不存在。然而，我们表明，下确界的成本是可计算的。
Decomposing Petri nets
在最近的工作中，第二和第三作者介绍了一种技术的可达性检查1-有界Petri网，基于布线分解，这是一个片段的组合代数的网络与边界的表达式。在这里，我们将该技术推广到全代数，并介绍了有关的结构性质的分解宽度的有向超图。小的分解宽度是必要的可达性检查算法的适用性。我们给出的例子，家庭的网络与恒定的分解宽度和发展的基本理论的分解。
Proposal for Adding Useful Features to Petri-Net Model Checkers
长期存在的问题提出的解决方案的自动分解的Petri网到并发进程，以及在格勒诺布尔开发的方法的自动转换的安全Petri网NUPN（嵌套单元Petri网），需要一定的性能计算的Petri网。我们注意到，虽然这些属性在理论上是有趣的，实际上是有用的，他们目前还没有实现在主流的Petri网工具。考虑到这些属性将为工具开发人员开辟富有成效的研究方向，也为模型检验竞赛开辟新的视角。
Free Choice Petri Nets without frozen tokens and Bipolar Synchronization Systems
双极同步系统（BP系统）构成了一类有色Petri网，非常适合于离散动态系统的控制流建模。每个BP系统都有一个底层的普通Petri网，它是一个T系统。此外，它还附加了第二个普通网，这是一个自由选择系统。我们证明了BP系统是活的和安全的，如果T系统和自由选择系统是活的和安全的，如果自由选择系统没有冻结令牌。这个结果是Genrich和Thiagarajan的一个定理的逆，并证明了一个老猜想。该证明利用Petri网的态射和自由选择系统的经典理论对不同的Petri网进行了比较
Flatness and Complexity of Immediate Observation Petri Nets
在以前的论文中，我们介绍了即时观察（IO）Petri网，一类感兴趣的研究人口协议和酶化学网络。在本文的第一部分中，我们表明，IO网是全球平坦的，所以他们的安全性能可以检查有效的符号模型检验工具，使用加速技术，如FAST。在第二部分中，我们研究了分支IO网（BIO网），其转换可以创建令牌。BIO网扩展了IO网和无通信网，也称为BPP网，这是一个广泛研究的类别。我们表明，虽然BIO网不再是全球平坦的，他们的可达标记集可能是非半线性的，他们仍然是局部平坦的。因此，BIO网的可覆盖性和可达性问题，甚至是它们的某个集合参数化版本，都在PSPACE中。这使得BIO网的第一个自然网类与非半线性可达性关系，可达性问题是可证明的简单比一般的Petri网。
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-完全的.
Feedback control logic synthesis for non safe Petri nets
研究了非安全Petri网（PN）建模离散事件系统的禁止状态问题。为了防止被禁止的状态，可以使用与转换相关联的条件或谓词。一般来说，有许多禁戒态，因此许多复杂的条件与过渡。提出了一种计算非安全Petri网谓词的新思想。利用这种方法，我们可以构造一个最大允许控制器，如果它存在。
Structural Liveness of Conservative Petri Nets
研究证明保守Petri网的结构活力问题在保守子类中仍为EXPSPACE难，且结构活的保守网的最小活标记值不超过双指数，从而证明其EXPSPACE完全性。
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网的模型检验问题。因此，可以验证在无限数量的人的公平性假设下具有策略更新的物理访问控制。
Unifying Inference for Bayesian and Petri Nets
作者最近的工作装备Petri发生网（PN）的概率分布，完全取代非确定性。为了避免所谓的混淆问题，这种结构强加了额外的因果依赖关系，限制了某些被称为结构分支单元（s-单元）的选择。贝叶斯网（BN）通常被构造为偏序，其中节点定义条件概率分布。本文用对称Monoidal范畴（SMC）把这两种结构统一起来，使我们能应用于PN的普通分析技术。有趣的是，事实证明，不能被SMC分解的PN正是s-细胞。这一结果证实了SMC和S-细胞的Petri网的重要性。
Parameterized Analysis of Immediate Observation Petri Nets
我们介绍即时观察Petri网，一类感兴趣的研究人口协议（分布式计算模型），和酶化学网络。在这些领域中，相关的分析问题转化为参数化的Petri网问题：具有相同底层网但不同初始标记的Petri网的无限集合是否满足给定的性质。研究了直接观察Petri网的参数化可达性、可覆盖性和活性问题。我们发现，所有这三个问题是在PSPACE的计数约束，一类足够丰富的预期应用程序定义的初始标记的无限集。这是值得注意的，因为当标记集是单例时，问题已经是PSPACE困难的，即，在非参数化的情况下。我们使用这些结果来证明即时观察人口协议的正确性问题是PSPACE完全的，回答了以前的论文中留下的一个问题。
SMPT: A Testbed for Reachability Methods in Generalized Petri Nets
SMPT（Satisfiability Modulo Petri Net）是一个用于Petri网可达性问题的模型检测器。它最初是一个试验符号模型检验的方法组合，并被设计为易于扩展。一些独特的功能是它能够从结构简化中受益，并生成判决证书。与模型检验竞赛中的其他最先进的工具相比，我们的工具相当成熟，表现良好。
Reversible Computation in Cyclic Petri Nets
Petri网是一种用于分布式系统建模和推理的数学语言。在本文中，我们提出了一种方法，Petri网嵌入可逆性，即，在操作过程中的任何一点上，使已执行的操作序列反向的能力。具体而言，我们引入机器和相关的语义来支持三种主要形式的可逆性，即回溯，因果反转，和在循环Petri网的变化，令牌是持久的，并相互区分的身份的顺序颠倒的cabetual。我们的形式主义的影响，在生物化学中的应用，但方法可以应用到广泛的问题，功能可逆性。特别是，我们证明了我们的方法的适用性与ERK信号通路的模型，一个例子，本质上具有可逆的行为。
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台交换机的软件定义网络。
A "Symbolic" Representation of Object-Nets (Extended Version)
本文针对基本对象系统（EOS，一种网中嵌套Petri网的形式体系）状态空间规模大的问题，将Petri网同态扩展至EOS，利用拓扑自同构的对称性压缩状态空间，为嵌套Petri网的状态分析提供了符号化方法。
Compositional Semantics of Finite Petri Nets
本文针对有限 Petri 网，证明保结构互模拟关于 FMN 算子为同余，并给出尊重因果性与分支结构的组合语义及可靠公理化基础。
Perpetual Free-choice Petri nets are lucent -- proof of a theorem of van der Aalst using CP-exhaustions
本文通过CP-子网穷举法证明van der Aalst定理，即永久自由选择Petri网是清晰的，并用初等方法分析所得T-系统。
Structural Liveness of Immediate Observation Petri Nets
本文研究了即时观察网（IO网）及其广义变体BIMO网的结构活性问题，证明了该问题对IO网是PSPACE-hard的，对BIMO网属于PSPACE，并讨论了决定标记活性的令牌数界限。
A Polynomial Translation of pi-calculus FCPs to Safe Petri Nets
我们开发了一个多项式的翻译有限控制π演算过程安全的低级别Petri网。据我们所知，这是第一个这样的翻译。这是自然的，因为有一个密切的对应关系之间的控制流，享有互模拟的结果，并适合于实际的模型检验。
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
本文证明了（强）全并发互模拟性和i-因果网互模拟性在有限有界Petri网上是可判定的，其核心方法是对Vogler的有序标记证明技术进行推广。
Homogeneous Equations of Algebraic Petri Nets
代数Petri网是一种用于分布式系统和算法建模的形式主义，通过结合Petri网和代数规范来描述控制和数据流。指定代数Petri网模型$N$的正确性的一种方式是基于项替换和来自阿贝尔群$G$的系数来指定在$N$的位置上的线性方程$E$。然后，$E$在$N$中有效，当且仅当$E$在$N$的每个可达标记中有效。由于代数Petri网的表达能力，有效性通常是不可判定的。稳定的线性方程组形成一类有效性可判定的线性方程组。位置不变量给出了所有稳定线性方程的一个很好理解但不完整的特征。在本文中，我们提供了一个完整的特征的稳定性子类的齐次线性方程，限制自己的解释条款的Herbrand结构，而不考虑进一步的平等公理。在此基础上，证明了当$G$是循环群时，齐次线性方程的稳定性是可判定的.
State Space Computation and Analysis of Time Petri Nets
Petri网理论提供了一个通用的框架来描述实时反应式系统的行为，时间Petri网的引入也考虑了时间规范。本文提出了一种基于前向区域的算法来计算有界时间Petri网的状态空间：该方法与经典的状态类图不同，并且更有效。我们证明该算法是精确的可达性问题。此外，我们提出了一个翻译的计算状态空间到一个时间自动机，证明了原来的时间Petri网的时间双相似。当该方法产生单个时间自动机时，可以应用语法时钟减少方法（例如Daws和Yovine）来产生具有更少时钟的自动机。然后，我们的方法允许通过使用高效的时间自动机工具进行模型检查TTPN。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
The Monadic Second Order Theory of Grid-Free 1-Safe Petri Nets is Decidable
有限1-安全Petri网，也称为\emph{net systems}，是异步并发的自然模型。网络系统的事件结构描述了所有可能的执行及其并发性质：两个事件可能是因果有序的，并行发生或冲突。一元二阶逻辑（MSO）可以用来描述网系统的行为性质。Thiagarajan猜想指出MSO是可判定的当且仅当网络系统是无网格的。本文对这一猜想给出了肯定的回答。
Subtyping for Hierarchical, Reconfigurable Petri Nets
层次Petri网允许更抽象的视图和可重构Petri网模型的动态结构适应。在这方面的贡献，我们提出了可重构Petri网和层次Petri网的组合产生层次结构的可重构Petri网。层次结构是通过将转换替换为“转换”来建立的。这些对象本身是可重新配置的，因此它们被提供了自己的规则集。此外，提供了可以应用于所有网络的全局规则。
Deciding structural liveness of Petri nets
库所/变迁Petri网是一类可达空间可能是无限的分布式系统的标准模型。其中一个研究得很好的主题是验证该模型的安全性和活性属性，尽管广泛的研究工作，一些基本的问题仍然是开放的，这是由开放的复杂性状态的可达性问题的例证。活性问题与可达性问题密切相关，许多与活性相关的网的结构性质已经被研究。有些令人惊讶的是，如果一个网络在结构上是活的，即如果有一个初始标记，它是活的，这个问题的可判定性状态仍然是开放的，正如最近的一篇论文（Best和Esparza，2016）强调的那样。在这里，我们证明了Petri网的结构活性问题是可判定的。证明的一个重要组成部分是Leroux（LiCS 2013）的结果，该结果表明，如果一个标记Petri网的可达集是半线性的，我们可以计算该集的有限（Presburger）描述。
Bisimulation Relations Between Automata, Stochastic Differential Equations and Petri Nets
如果两个形式随机模型的解作为随机过程是概率等价的，则称它们是双相似的。两种随机模型形式之间的双相似性意味着一种随机模型形式的优点可以被另一种随机模型形式所利用。本文的目的是解释随机混杂自动机、混杂空间上的随机微分方程和随机混杂Petri网之间的双相似关系。这些双相似关系使得将自动机的形式化验证能力与随机微分方程的分析能力和Petri网的组合规范能力相结合成为可能。的关系和它们的综合优势，说明了空中交通的例子。
Distributed Diagnosability Analysis with Petri Nets
我们提出了一个框架，分布式诊断能力分析的并发系统建模与Petri网作为一个集合的组件同步的共同可观察的转变，故障可能发生在几个组件。通过验证每个组件与其他组件的无故障版本的相互作用，并行完成整个系统的可诊断性分析。此外，我们使用现有的有效的方法和工具，特别是并行LTL-X模型检验的基础上展开，可诊断性验证。
ω-Petri nets
我们介绍了ω-Petri网（ωPN），一个扩展的普通Petri网与ω-标记的输入和输出弧，这是非常适合于分析参数并发系统与动态线程创建。在普通Petri网环境中提出的大多数技术（例如Karp和Miller树或Rackoff技术）并不直接适用于ωPN，因为ωPN定义了具有无限分支的转移系统。这激发了对ωPN的计算方面的彻底分析。我们表明，ωPN可以变成一个普通的Petri网，允许恢复的可达集的ωPN，但不保持终止。这就产生了ωPN上的可达性、（位置）有界性和可覆盖性问题的复杂性界。我们提供了一个实用的算法来计算一个覆盖集的ωPN和决定终止适应经典的Karp和Miller树的结构。我们还将Rackoff技术应用于ωPN，以获得终止问题的精确复杂度。最后，我们考虑了具有重置弧和转移弧的ωPN的扩展，并展示了这种扩展如何影响上述问题的可判定性和复杂性。
Token Multiplicity in Reversing Petri Nets Under the Individual Token Interpretation
反向Petri网（Reversing Petri nets，RPNs）是最近提出的一种基于网的方法，用于建模因果和非因果顺序的可逆性。它们基于可以通过债券连接在一起的单个代币的概念。在本文中，我们扩展RPN允许多个相同类型的令牌存在于一个网的基础上的个人令牌解释的Petri网。根据这种解释，相同类型的令牌区分通过其因果path.We开发的模型的因果语义，我们证明了RPN的表达能力与多个令牌的RPN与单令牌的RPN是等价的，通过建立一个同构之间的标签转换系统（LTS）捕获的可达部分的各个RPN模型。
Integrated Structure and Semantics for Reo Connectors and Petri Nets
在本文中，我们提出了一个集成的结构和行为模型的Reo连接器和Petri网，允许直接比较两个并发模型。为此，我们引入了一个概念的连接器，它由一些相互连接的，用户定义的原语与固定的行为。虽然连接器的结构类似于超图，但它们的语义是根据所谓的端口自动机给出的。我们在分类设置中定义了这两种模型，其中组合操作可以被优雅地定义和集成。具体来说，我们正式的结构胶合的连接器作为推出，并加入端口自动机作为拉回。然后，我们定义了一个语义函子从连接器的端口自动机类别，保持这种组合。我们进一步展示了如何将Reo连接器和Petri网编码到这个模型中，并指出了使用双推出图变换建模的动态重新配置的应用程序。
Time Petri Nets with Dynamic Firing Dates: Semantics and Applications
我们定义了一个扩展的时间Petri网，这样的时间，过渡可以火，也称为其发射日期，可以动态更新。我们的扩展提供了两种机制，用于更新网络的时间约束。首先，我们建议在每次新启用时更改转换的静态时间间隔;在这种情况下，新的时间间隔是作为当前标记的函数给出的。接下来，我们允许在转换持久化时更新转换的触发日期，也就是在并发转换触发时。我们展示了如何进行广泛使用的状态类抽象到这种新的时间Petri网，并定义了一类网的抽象是准确的。我们展示了我们的方法的实用性与两个应用程序：第一调度抢占式任务，作为一个穷人的秒表的替代品，然后建模混合动力系统与非平凡的连续行为。
Decidable Reversible Equivalences for Finite Petri Nets
本研究证明Petri网中因果网互模拟与遗传因果网互模拟等价，明确其可逆行为等价属性，同时证明库所互模拟更精细且可逆，为真并发谱提供两种可判定可逆等价关系，替代不可判定的遗传保历史互模拟。
A Process Calculus for Expressing Finite Place/Transition Petri Nets
我们介绍了进程演算多CCS，它扩展了保守CCS与操作员的强前缀能够模拟原子序列的行动，以及多方同步。多CCS配备了一个标记的转换系统语义，它利用了最小的结构一致性。多CCS还配备了一个不安全的P/T Petri网语义的一种新技术。这是第一个富进程演算，包括CCS作为子演算，它接收不安全的标记P/T网的语义。本文的主要结果是，一类多CCS过程，称为有限网过程，能够表示所有有限（约简）P/T网。
Resource Bisimilarity in Petri Nets is Decidable
本文针对 Petri 网中的资源互模拟关系，提出判定算法，证明其可判定性，并给出相似但不互模拟的实例，区别于不可判定的资源相似性。
Theory of CHTW-systems. Born by Petri Nets
本文首次提出基于Petri网的多维CHTW系统概念，基于混合函数Petri网构建理论，引入膜与载体概念（与超弦理论概念为远距类比），研究其定常与非定常动态描述并给出初步分类，明确后续研究方向。
Configuration Structures, Event Structures and Petri Nets
本文将Nielsen、Plotkin和Winskel等人提出的安全Petri网与事件结构之间的对应关系，在集体令牌解释下，推广到任意无自环网。为此，我们提出了一个更一般的形式的事件结构，匹配这样的网络的表达能力。这些新的事件结构和网络通过将这两个概念与配置结构相关联而连接起来，配置结构可以被视为事件结构或网络的表示，这些结构或网络根据动作发生及其之间的因果关系捕获它们的行为，但从任何辅助结构中抽象出来。一个构形结构也可以在逻辑上被认为是一类命题模型，或者等价地被认为是一个在析取范式中的命题理论。将这种理论转化为合取范式是将这种结构转化为网的关键思想。对于各种类别的事件结构，我们将相关类别的配置结构的闭包性质，以及在相关的命题理论的公理化的简单规定形式的公式，并在相关的Petri网的结构性质。
Homology Groups of Pipeline Petri Nets
研究了流水线系统的基本Petri网的同调群。我们证明了这些网在0维和1维上的整同调群等于整数群，并且它们在其他维上为零。我们证明了基本Petri网的有向同调群在所有维度上都为零。
TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets
本文提出了一种针对Petri网的HyperLTL模型检查器，用于验证超属性，该工具集成于TAPAAL框架并展示了其在计算机网络领域的应用性能。
Coverability, Termination, and Finiteness in Recursive Petri Nets
本文证明递归Petri网的可覆盖性、终止性、有界性和有限性问题均为EXPSPACE完全，且其可覆盖性语言严格包含Petri网与上下文无关语言的并集，从而免费获得更强模型。
Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets
我们提出了一个框架，规范的行为保留的重新配置系统建模为Petri网。该框架是基于开放的网络，一个温和的泛化普通的地方/过渡网适合模型开放的系统，可能会与周围的环境相互作用，并赋予一个colimit为基础的组合操作。我们表明，自然的概念开网的双相似性是同余的组合操作。所考虑的行为等效性因观察结果的选择而异，这些观察结果可以是单次击发或并行步骤。此外，我们认为这种等价的弱形式，在不可观察的行动的存在下产生的。我们还提供了一个最多的技术，以促进双相似性证明。该理论是用来确定合适的类的重新配置规则（在双推出重写方法），其应用程序保留了观察语义的网。
Universal Safety for Timed Petri Nets is PSPACE-complete
一个定时网络由任意数量的初始相同的1时钟定时自动机组成，通过握手通信进行交互。在这种情况下，没有唯一的中央控制器，因为所有的自动机最初都是相同的。我们考虑这种无限制定时网络的普遍安全问题，即，验证无论网络的大小如何，坏事件（启用某些给定的转换）都是不可能的。这个普遍的安全问题是时间弧Petri网的存在可覆盖性问题的对偶，即，是否存在多个$m$令牌，使得从给定位置中的$m$令牌开始，并且在其它位置中没有令牌，最终启用某个给定转换。我们证明了这些问题是PSPACE完备的。
Methods for Efficient Unfolding of Colored Petri Nets
本文提出两种静态分析方法，通过颜色等价类和颜色过近似来减少展开后的彩色Petri网规模，显著提升了多个模型检查竞赛基准的展开效率和结果质量。
Property Directed Reachability for Generalized Petri Nets
我们提出了一个半决策过程检查广义可达性，广义Petri网，这是基于属性导向可达性（PDR）方法。我们实际上定义了三个不同的版本，这取决于用于提取可能的证人的方法，并且能够处理越来越困难的问题。我们已经实现了我们的方法在一个模型检查器称为SMPT，并给出经验证据，我们的方法可以处理的问题，是困难的或不可能检查与当前最先进的工具。
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网的范畴，其态射是这个网可以进行的过程。这是以组合的方式完成的，因此这些类别可以在较小的数组上计算，然后粘在一起。第二种是可达性语义，它简单地说，从输入的给定标记可以到达输出的哪些标记。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。