Capacity Bounded Grammars and Petri Nets
Ralf Stiebe, Sherzod Turaev
容量有界文法是指通过给每个非终结符的个数赋一个界来限制其推导的文法。本文研究了容量有界文法及其Petri网控制文法的生成能力和闭包性质。
A capacity bounded grammar is a grammar whose derivations are restricted by assigning a bound to the number of every nonterminal symbol in the sentential forms. In the paper the generative power and closure properties of capacity bounded grammars and their Petri net controlled counterparts are investigated.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Extended time Petri nets
针对现有时间Petri网无法兼容多类时间数据的问题，本文提出一种扩展时间Petri网，整合现有各类时间Petri网的特性，支持在统一模型中使用不同类型时间数据，解决建模时时间数据不一致或不完整带来的难题。
Continuous Reachability for Unordered Data Petri nets is in PTime
无序数据Petri网（UDPN）是经典Petri网的扩展，带有从无限域携带数据的令牌，其中变迁可以检查令牌的相等和不相等。UDPN具有良好的结构，因此其可覆盖性和可终止性问题是可判定的，但其复杂性高于Petri网。另一方面，UDPN的可达性问题令人惊讶地复杂，其可判定性状态仍然是开放的。在本文中，我们考虑了UDPN的连续可达性问题，它可以被看作是可达性问题的过近似。我们的主要结果是UDPN的连续可达性和多项式时间算法求解它的一个特征。这是一个组合参数的结果，它表明，如果连续可达性保持，那么存在一个运行只使用多项式多个数据值。
Invariants and Home Spaces in Transition Systems and Petri Nets
本文系统比较变迁系统与Petri网中的不变量和归位空间概念，借助线性代数与半流、生成集等代数工具提取并行系统不变性质，并通过实例展示其在行为性质证明中的应用。
On the expressive power of non-deterministic and unambiguous Petri nets over infinite words
本文证明非确定性Petri网与图灵机的ω-语言拓扑复杂度相同，且相关判定问题高度不可判定；相反，无歧义Petri网可确定化为Muller计数器机，其ω-语言为Δ₀₃集合。
Synthesizing Petri Nets from Labelled Petri Nets using Token Trail Regions
本文提出一种新的区域理论，结合基于状态和基于语言的规范，用于从标记Petri网合成Petri网，以解决传统方法的局限性。
Coverability, Termination, and Finiteness in Recursive Petri Nets
本文证明递归Petri网的可覆盖性、终止性、有界性和有限性问题均为EXPSPACE完全，且其可覆盖性语言严格包含Petri网与上下文无关语言的并集，从而免费获得更强模型。
Transformation From Legal-marking Set to Admissible-marking Set of Petri Nets With Uncontrollable Transitions
在含有不可控变迁的Petri网中，线性约束变换是解决禁止状态问题的关键步骤。本文研究了在这种网的情况下，从合法标记集到其容许标记集的等价变换。首先，定义了逃逸标记集和变换标记集的概念。在此基础上，给出了线性约束的可允许标记集和变换标记集的计算算法，为线性约束的等价变换奠定了理论基础。其次，建立了具有不可控变迁的Petri网的线性约束条件之或的等价变换理论。第三，给出了两个规则来确定转换的优先级。最后，通过两个例子说明了从一个给定的线性约束到一个能描述其整个容许标记集的线性约束逻辑表达式的转换过程。
Collaboration Miner: Discovering Collaboration Petri Nets (Extended Version)
针对协作流程缺乏标准挖掘模型的问题，本研究结合协作Petri网提出Collaboration Miner方法，可发现多类协作概念，在26个事件日志上验证了其低表示偏差、高拟合精度的优势。
Petri Nets and Bio-Modelling - and how to benefit from their synergy
在这次演讲中，我们关注的是一方面Petri网与另一方面膜系统和反应系统之间的内在相似性和差异。
Well-Formed Free-Choice Petri Nets Revisited
本文重新审视自由选择Petri网的well-formed性质，引入半T组件概念并推导经典定理及对偶定理。
Correctness Notions for Petri Nets with Identifiers
本文提出适用于描述信息系统的Petri网扩展形式，探讨了资源和对象感知信息系统的正确性标准，并讨论了其在特定系统类中的可判定性。
Acyclic Petri and Workflow Nets with Resets
本文提出两类带重置的无环Petri网新子类，证明其可覆盖性或可达性问题复杂度从Ackermann难/不可判定降至PSPACE完全，为相关问题求解提供了可处理的网类。
Decidability Issues for Petri Nets -- a survey
该文系统梳理Petri网25年可判定性研究，汇集重要性质、等价概念及时序逻辑可判定性的核心成果。
Time Delays in Membrane Systems and Petri Nets
研究了具有显式资源和并行性的形式主义中的时间方面，并提出了时间膜系统和具有局部性的时间Petri网之间的形式联系。对于这两种形式主义，时间并没有增加表达能力;然而，时间膜系统和时间Petri网在描述时间是关键资源的分子现象时更加灵活。我们建立了时间膜系统和时间Petri网与地方之间的联系，并证明了它们之间的操作对应关系。
On the Topological Complexity of omega-Languages of Non-Deterministic Petri Nets
我们证明了具有Büchi接受条件的非确定Petri网或等价的Büchi盲计数器自动机可以接受无限词的$Σ_3^0$ -完全语言.这表明非确定性Petri网所接受的Omega语言在拓扑上比确定性Petri网所接受的Omega语言更复杂。
Converting Reconfigurable Petri Nets to Maude
模型检验是理论计算机科学的一个重要研究方向。它可以验证具有一组属性（如活性，死锁或安全性）的模型。典型的建模技术之一是Petri网，它们被很好地理解并且可以用于模型检验。可重构Petri网是基于一组规则的Petri网。这些规则可以动态地用于改变网络。缺少的是验证可重构网络和死锁或活性等属性的可能性。本文介绍了一个转换可重构Petri网Maude，使我们能够填补空白。提出了一种基于Maude方程-重写逻辑和LTLR模型检验器的网变换方法。
Toward uniform random generation in 1-safe Petri nets
研究了1-安全Petri网无限执行空间上的一致测度的概念。在这里，1-安全Petri网的执行被理解为并发转换的交换，这引入了一个挑战相比，通常的过渡系统。我们得到的随机生成的无限执行减少到一个有限状态马尔可夫链的模拟。讨论了生物学问题。
Biologically Inspired Process Calculi, Petri Nets and Membrane Computing
本卷代表了第五届膜计算和生物启发过程演算研讨会（MeCBIC 2011）的会议记录，该研讨会于2011年8月23日在法国枫丹白露举行的第12届膜计算国际会议上举行。
Concurrent programming is used in all large and complex computer systems. However, concurrency errors and system failures (ex: crashes and deadlocks) are common. We find that Petri nets can be used to model concurrent systems and find and remove errors ahead of time. We introduce a novel generalization of Petri nets with nondeterministic transition nodes to match real systems. These allow for a compact way to construct, optimize, and prove computer programs at the concurrency level. Petri net programs can also be optimized by automatically solving for maximal concurrency, where the maximum num…
On the Upward/Downward Closures of Petri Nets
研究了以可覆盖性为接受条件的有限状态自动机（FSA）表示和逼近Petri网语言的向下闭包和向上闭包的规模和计算复杂性。我们将展示如何构建一个FSA识别的Petri网语言的向上封闭的双指数时间，因此，大小是最多的双指数。对于向下闭包，我们证明了最小自动机的大小可以是非本原递归的。在BPP网（Petri网的一个众所周知的子类）的情况下，我们证明了接受向下/向上闭包的FSA可以在指数时间内构造。此外，我们考虑的问题，检查是否一个简单的正则语言是包括在向下/向上的Petri网/BPP网语言的闭包。我们证明了这个问题是EXPSPACE-完全的（resp. NP完全）的情况下的Petri网（分别。BPP网）。最后，我们证明了它是可判定的，是否Petri网语言是向上/向下封闭的。为此，我们证明了一个可以决定是否一个给定的正则语言是一个Petri网覆盖性语言的子集。
Persistent Permutability in Choice Petri Nets
研究了选择Petri网中的持久可交换性，证明了某些类别的Petri网中持久可交换性可推导出整体持久性。
Relating Reversible Petri Nets and Reversible Event Structures, categorically
本文扩展因果网以支持非对称冲突，范畴化地构造其可逆版本，并建立其与可逆非对称事件结构范畴之间的对应关系。
We present a unified framework for Petri nets and various variants, such as pre-nets and Kock's whole-grain Petri nets. Our framework is based on a less well-studied notion that we call $Σ$-nets, which allow finer control over whether tokens are treated using the collective or individual token philosophy. We describe three forms of execution semantics in which pre-nets generate strict monoidal categories, $Σ$-nets (including whole-grain Petri nets) generate symmetric strict monoidal categories, and Petri nets generate commutative monoidal categories, all by left adjoint functors. We also const…
Bi-reachability in Petri nets with data
该研究针对带数据的Petri网提出双向可达性问题的判定过程，明确其介于可判定的覆盖性问题与可判定性未知的可达性问题之间，推进了相关可判定性边界研究。
Parameterized complexity results for 1-safe Petri nets
我们将一个图与一个1-安全的Petri网，并研究了各种问题的参数化复杂性与参数来自图。以树宽为参数，对1-安全Petri网的许多问题给出了W[1]-硬度结果。作为一个推论，这证明了唐尼等人的一个猜想。关于一些图卵石问题的硬度。我们考虑了参数效益深度（这是已知的，是有助于获得更好的算法一般Petri网），并再次给出了W[1]-硬度的结果，各种问题的1-安全Petri网。我们还考虑了更强的参数顶点覆盖数。结合著名的自动机理论方法和一元线性规划的固定参数易处理性（FPT）结果，给出了1-安全Petri网上一元二阶（MSO）公式模型检验的FPT算法，参数为公式的顶点覆盖数和大小.
Priced Timed Petri Nets
我们考虑定价时间Petri网，即，无界Petri网，其中每个令牌携带一个实值时钟。过渡弧标记有时间间隔，这指定了对令牌年龄的约束。此外，我们的成本模型将每时间单位的令牌存储成本分配给地点，并将发射成本分配给转换。这个一般模型严格包含定价时间自动机和无界定价Petri网。我们研究的成本计算，达到一个给定的控制状态。通常，由于时间约束的严格不等式，具有最小成本的计算可能不存在。然而，我们表明，达到一个给定的控制状态的成本的下确界是可计算的情况下，所有的地方和过渡成本是非负的。另一方面，如果允许负成本，那么给定的控制状态是否以零总成本可达的问题变得不可判定。事实上，即使在离散时间的简单情况下（即，整数值时钟）。
On Petri Nets with Hierarchical Special Arcs
我们研究的可判定性的终止性，可达性，覆盖性和死锁的Petri网赋予了一个层次的地方，并与抑制弧，复位弧和转移弧，尊重这一层次。我们还研究了当我们有这些特殊的弧，其中一些尊重层次结构，而其他人不混合时会发生什么。我们解决了上述四个问题的可判定性状态的层次，抑制，重置和转移弧的所有组合，除了两个组合的终止问题。对于这两种组合，我们表明，终止问题是很难决定线性递归序列的积极性-一个长期存在的开放问题。
Compositional model checking of concurrent systems, with Petri nets
组合性和进程等价性都是进程代数的标准概念。复合性意味着一个复合系统的行为只依赖于其组成部分的行为，即没有涌现行为。过程等价意味着系统的显式状态空间让位于其交互模式：环境可以通过交互获得的信息。Petri网是一个经典的，但被广泛使用和理解的并发模型。然而，它们经常被描述为非组合模型，并且工具倾向于处理整体的、全局指定的模型。本教程论文集中在Petri网与边界（PNB）：1-安全网的合成，图形代数，以及其应用程序中的可达性检查工具彭罗斯。该算法的特点是使用组合性和进程等价，一个强大的组合，可以利用，以提高性能的检查可达性和覆盖性在几个常见的例子，其中Petri网模型现实的并发系统。
Goal-Driven Unfolding of Petri Nets
在探索Petri网的运行时，展开提供了一种有效的方法来避免由于并发变迁的交织而导致的状态空间爆炸。适当阶理论允许定义包含所有可达标记的展开的有限前缀。在本文中，我们感兴趣的是一个单一的给定标记，称为目标的可达性。我们提出了一个算法，用于计算一个1-安全的Petri网，保持达到这一目标的所有最小配置的展开的有限前缀。该算法将展开技术与动态模型降阶技术相结合，通过静态分析来降低模型降阶，避免了对不必要分支的探索。我们提出了一些实验结果。
On Functions Weakly Computable by Pushdown Petri Nets and Related Systems
本文研究文法控制向量加法系统（GVASes）弱可计算的函数，证明其能计算快速增长函数但无法计算逆函数或次线性函数，基于独立有趣的泵引理。
Recently introduced Petri net-based formalisms advocate the importance of proper representation and management of case objects as well as their co-evolution. In this work we build on top of one of such formalisms and introduce the notion of soundness for it. We demonstrate that for nets with non-deterministic synchronization between case objects, the soundness problem is decidable.
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)$，改善了少数已知的结果在这个主题上。我们的调查还强调了几个有趣的权衡。
Synthesis of Reduced Asymmetric Choice Petri Nets
一个Petri网是无选择的，如果任何地方有最多一个转移在其后集（消耗其令牌），它是（扩展）自由选择（EFC），如果任何两个地方的后集是相等的或不相交的。非对称选择（AC）扩展了EFC，使得两个位置也可以具有一个包含在另一个中的后置集。在简化的AC网中，这种包容是有限的：如果后集既不不相交也不相等，则一个是单例，另一个正好有两个转换。Petri网综合的目的是在某个目标类中找到一个非标号Petri网，它的可达图同构于给定的有限标号变迁系统。无选择网具有强大的属性，允许经常容易地检测合成何时失败或至少加速合成。以EFC为目标类，只有少数属性可以提前检查，似乎没有捷径降低合成的复杂性（与任意Petri网相比）。对于AC网络，根本没有已知的合成过程。我们在这里展示了如何合成一个超类的减少AC网（不包含完整的AC网类）可以完成。
We show how a particular variety of hierarchical nets, where the firing of a transition in the parent net must correspond to an execution in some child net, can be modelled utilizing a functorial semantics from a free category -- representing the parent net -- to the category of sets and spans between them. This semantics can be internalized via Grothendieck construction, resulting in the category of executions of a Petri net representing the semantics of the overall hierarchical net. We conclude the paper by giving an engineering-oriented overview of how our model of hierarchical nets can be …
Deciding Detectability for Labeled Petri Nets
本文研究了由标记Petri网建模的离散事件系统中强可检测性和弱可检测性的验证问题，证明强可检测性是可判定的而弱可检测性是不可判定的，扩展了现有研究从有限状态自动机到标记Petri网的可检测性验证。
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网：分支和下推栈。
Due to the mobility and frequent disconnections, the correctness of mobile interaction systems, such as mobile robot systems and mobile payment systems, are often difficult to analyze. This paper introduces three critical properties of systems, called system connectivity, interaction soundness and data validity, and presents a related modeling and analysis method, based on a kind of Petri nets called VPN. For a given system, a model including component nets and interaction structure nets is constructed by using VPNs. The component net describes the internal process of each component, while the…
Secret Protection in Labeled Petri Nets
本文将秘密保护问题从有限自动机扩展到带标签Petri网，提出Parikh和指示器两种变体，证明其判定版本为ExpSpace完全，从而排除多项式时间或空间算法的存在。
We provide a categorical semantics for bounded Petri nets, both in the collective- and individual-token philosophy. In both cases, we describe the process of bounding a net internally, by just constructing new categories of executions of a net using comonads, and externally, using lax-monoidal-lax functors. Our external semantics is non-local, meaning that tokens are endowed with properties that say something about the global state of the net. We then prove, in both cases, that the internal and external constructions are equivalent, by using machinery built on top of the Grothendieck construct…
Testing experiments on synchronized Petri nets
本文研究了有限状态机模型系统的同步序列计算，提出利用Petri网结构高效计算同步序列的新方法，避免穷举状态空间。
The Essence of Petri Net Gluings
本文提出一个在组合Petri网时尊重其语义的范畴框架，并证明其能推广先前通过资源共享或变迁同步进行粘合的方法。
Critical Observability for Automata and Petri Nets
本文研究了自动机和Petri网模型中临界可观测性问题的计算复杂性，证明了对于有限状态自动机，该问题在NL完全；对于自动机网络，问题在PSPACE完全；而对于标记化Petri网，问题不可判定，但当临界状态集为有限或余有限时，问题变得可判定且与Petri网的不可达性问题等难。
Techniques to discover Petri nets from event data assume precisely one case identifier per event. These case identifiers are used to correlate events, and the resulting discovered Petri net aims to describe the life-cycle of individual cases. In reality, there is not one possible case notion, but multiple intertwined case notions. For example, events may refer to mixtures of orders, items, packages, customers, and products. A package may refer to multiple items, multiple products, one order, and one customer. Therefore, we need to assume that each event refers to a collection of objects, each …
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。