Property Directed Reachability for Generalized Petri Nets
我们提出了一个半决策过程检查广义可达性，广义Petri网，这是基于属性导向可达性（PDR）方法。我们实际上定义了三个不同的版本，这取决于用于提取可能的证人的方法，并且能够处理越来越困难的问题。我们已经实现了我们的方法在一个模型检查器称为SMPT，并给出经验证据，我们的方法可以处理的问题，是困难的或不可能检查与当前最先进的工具。
2022-08-05 cs.LO
Checking marking reachability with the state equation in Petri net subclasses
虽然可判定的，标记的可达性问题的Petri网是众所周知的，是棘手的一般，和一个非初等下界最近被发现。为了减轻这个困难，各种结构和行为的限制已经被考虑，允许相关的可达性的属性，更容易检查。对于一个给定的初始标记，一组潜在的可达标记描述的状态方程的解决方案和过近似的可达标记的集合。在本文中，我们描绘了几个子类的加权Petri网，其中的可达标记集等于一组潜在的可达的，一个属性，我们称之为PR-R平等。当满足时，这个属性允许使用线性代数来回答可达性问题，避免了状态空间的暴力分析。值得注意的是，我们提供的条件下，这种平等持有的类更有表现力比标记的图形，增加了几个进出的过渡，这使得真正的应用程序与共享缓冲区建模的地方。为了实现这一点，我们研究了Petri网的活性，可逆性，有界性和潜在的可达性之间的关系。我们还表明，这种平等并不持有密切的建模能力，当条件放宽类。
2020-06-10 cs.LO
Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability
本文提出一种基于结构约简的Petri网广义可达性属性检查方法，通过线性复杂度的变量消去投影过程将属性转化为约简网的等价公式，可作为现有模型检测器的预处理步骤，实验证明其在约简量有限时依然有效。
2024-01-08 cs.LO
Deciding structural liveness of Petri nets
库所/变迁Petri网是一类可达空间可能是无限的分布式系统的标准模型。其中一个研究得很好的主题是验证该模型的安全性和活性属性，尽管广泛的研究工作，一些基本的问题仍然是开放的，这是由开放的复杂性状态的可达性问题的例证。活性问题与可达性问题密切相关，许多与活性相关的网的结构性质已经被研究。有些令人惊讶的是，如果一个网络在结构上是活的，即如果有一个初始标记，它是活的，这个问题的可判定性状态仍然是开放的，正如最近的一篇论文（Best和Esparza，2016）强调的那样。在这里，我们证明了Petri网的结构活性问题是可判定的。证明的一个重要组成部分是Leroux（LiCS 2013）的结果，该结果表明，如果一个标记Petri网的可达集是半线性的，我们可以计算该集的有限（Presburger）描述。
2016-08-08 cs.LO
Efficient Restrictions of Immediate Observation Petri Nets
在以前的论文中，我们介绍了即时观察Petri网，Petri网的一个子类，在分布式协议（人口协议）和理论化学（化学反应网络）中具有应用领域。IO网具有许多有用的性质，但与保守Petri网一样，它们也存在PSPACE完全可达性问题。在本文中，我们探讨了IO网的可达性问题的两个限制，大大降低了问题的复杂性。对于分布式协议中的应用，第一个限制的复杂性是NP完全的，对于化学环境中的应用，第二个限制的复杂性是多项式的。
2020-10-08 cs.LO
Decomposing Petri nets
在最近的工作中，第二和第三作者介绍了一种技术的可达性检查1-有界Petri网，基于布线分解，这是一个片段的组合代数的网络与边界的表达式。在这里，我们将该技术推广到全代数，并介绍了有关的结构性质的分解宽度的有向超图。小的分解宽度是必要的可达性检查算法的适用性。我们给出的例子，家庭的网络与恒定的分解宽度和发展的基本理论的分解。
2013-04-10 cs.LO
Bi-reachability in Petri nets with data
University of Warsaw（华沙大学）
该研究针对带数据的Petri网提出双向可达性问题的判定过程，明确其介于可判定的覆盖性问题与可判定性未知的可达性问题之间，推进了相关可判定性边界研究。
2024-07-11 cs.CL cs.FL cs.LO
A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking
本文提出一种基于多面体抽象的Petri网约简方法，结合SMT模型检验器，通过等价关系保证正确性，并在SMPT工具中实现BMC和PDR，实验验证其有效性。
2022-10-11 cs.LO
Approximating Petri Net Reachability Along Context-free Traces
我们调查的问题，问是否一个上下文无关的语言（CFL）和Petri网语言（PNL）的交集是空的。我们的贡献，以解决这个长期存在的问题，例如，在无界数据域的递归程序的可达性分析，是确定一类的CFL称为有限索引CFL的问题是可判定的。CFL的k索引近似可以通过丢弃所有不能在非终结符出现次数的预算k内导出的字来获得。因此，有限指数CFL是一个CFL，它与它对某个k的k指数近似一致。我们决定是否一个有限指标CFL和PNL的交集是空的，通过减少它的可达性问题的Petri网与弱抑制弧，一类系统具有无限多的状态，可达性是已知的可判定的。相反，我们表明，弱抑制弧的Petri网的可达性问题减少到一个PNL的有限指标CFL的空性问题。
2012-01-16 cs.FL cs.LO
On the Complexity of Proving Polyhedral Reductions
IMDEA Software Institute（IMDEA软件研究所）；LAAS-CNRS Université de Toulouse INSA CNRS（图卢兹大学国家科学研究中心实验室）
本文提出自动证明Petri网多面体抽象的方法，通过将等价性问题编码为SMT公式，解决无限状态系统下的等价性验证，并探讨多面体简化在可达性问题中的应用。
2024-09-11 cs.LO
Dynamic Polyhedral Logic
University of Amsterdam（阿姆斯特丹大学）；National Research Council, Pisa（国家研究委员会）；University of Barcelona（巴塞罗那大学）；TSU Razmadze Mathematical Institute（拉兹马泽数学研究所）
该研究提出时空多面体可达性逻辑，扩展动态拓扑逻辑并公理化相关h-动态可达空间，证明其针对预期可逆动力系统类的可靠性与完备性。
2026-08-27 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
Logics of polyhedral reachability
本文针对含类Until空间模态词的多面体可达性逻辑，提出公理系统并通过两步证明其相对于多面体语义学的完备性，为3D网格模型检测等应用提供理论支撑。
2024-06-23 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
A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets
时间弧Petri网（TAPN）是Petri网模型的一种著名的时间扩展，并且已经针对该模型提出了几种时间自动机的网络转换。我们提出了一个直接的，基于数据库管理的算法向前可达性分析的有界TAPN扩展的运输弧，抑制弧和年龄不变。我们也给出了一个完整的证明其正确性，包括减少技术的基础上对称性和外推。最后，我们增加了一种新的状态空间减少技术的算法，引入了标记上的单调排序，并证明其可靠性，即使在存在的单调性破坏功能，如年龄不变量和抑制弧。我们实现的算法内的模型检查器TAPAAL和实验结果文件一个令人鼓舞的性能相比，验证方法，翻译TAPN模型UPPAAL时间自动机。
2012-11-27 cs.DS cs.LO
Acyclic Petri and Workflow Nets with Resets
本文提出两类带重置的无环Petri网新子类，证明其可覆盖性或可达性问题复杂度从Ackermann难/不可判定降至PSPACE完全，为相关问题求解提供了可处理的网类。
2023-11-06 cs.FL cs.LO
Optimal Label Splitting for Embedding an LTS into an arbitrary Petri Net Reachability Graph is NP-complete
对于一个给定的标号变迁系统（LTS），综合的任务是找到一个同构的可达图的非标号Petri网。即使只要求嵌入到可达图中而不是同构，也不能保证解决方案。在这种情况下，标签分割是一种选择，即重新标记LTS的边缘，使得不同标记的边缘保持不同。通过适当的标签分裂，我们总是可以获得合成或嵌入问题的解决方案。使用标签分裂，我们可以构造一个带有预期的baker-our的标签Petri网（例如，将给定的LTS嵌入其可达图中）。由于标记的Petri网可以有大量的转换，可能需要优化，限制标签分裂产生的标签的数量。我们表明，这样的限制将成为一个NP-完全问题，从可解的问题在多项式时间。
2020-02-12 cs.CC cs.DS cs.FL
Verification of Nonblockingness in Bounded Petri Nets With Minimax Basis Reachability Graphs
针对有界Petri网非阻塞性验证问题，提出基于极小极大基可达图的半结构化方法，无需构建完整可达图即可完成验证，适用范围广。
2021-06-08 cs.LO cs.SY eess.SY
Structurally Cyclic Petri Nets
一个Petri网在结构上是循环的，如果每一个配置都可以通过一个或多个步骤从它自己到达。我们证明了结构周期性在确定性多项式时间内是可判定的。为此，我们适应Kanghaju的方法一般的可达性问题的Petri网。
2015-12-20 cs.LO
Verification of Reachability Problems for Time Basic Petri Nets
基于时间的Petri网是一种用于实时系统建模的强大的形式主义，其中时间约束通过与转换相关联的标记的时间描述的时间函数来表示，表示可能的触发时间。我们介绍了一种技术，可达性分析的基础上建设的有限收缩的无限状态空间与这样一个模型。该技术构造了一个有限的符号可达图依赖于一种时间覆盖，并克服了现有的分析工具的限制，时间基本网络，反过来基于一个时间有界的检查（可能是无限的）可达树。该技术的一个关键特征是引入了时间匿名概念，该概念允许识别不影响模型演变的组件。一个运行的例子是在整个文件中使用草图的符号图的建设。图的构造算法已被自动化的Java工具集，在该文件中描述连同其主要功能和分析能力。描述一个真实世界的例子的用例已经被用来对技术和工具集进行基准测试。文中还介绍了试验的主要结果。
2014-09-09 cs.LO cs.SE
ω-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
Decision Problems for Petri Nets with Names
我们证明了nu-PN，纯名称创建和名称管理的P/T网的扩展的可判定性和不可判定性的结果。通过将具有抑制弧的网的可达性归结为可达性，给出了可达性不可判定性的一个简单证明，从而证明了nu-PN网的表达能力严格优于P/T网。我们证明了nu-PN是结构良好的转移系统。特别地，我们得到了可覆盖性和可终止性的可判定性，从而没有达到图灵机的表达能力。此外，它们是严格良结构的，因此有界性问题也是可判定的。我们考虑两个属性，宽度有界性和深度有界性，分解有界性。宽度有界性已经被证明是可判定的。我们在这里证明深度有界的不可判定性。最后，我们得到阿克曼硬度的结果，我们所有的可判定的决策问题。
2010-11-17 cs.LO
On the Home-Space Problem for Petri Nets and its Ackermannian Complexity
本文证明了Petri网半线性家空间问题的可判定性，通过建立与可达性问题的对偶性，并证明了该问题的Ackermann完备性，同时给出了最小可达标记集合的Ackermann时间构造方法。
2024-12-10 cs.LO
Applying CEGAR to the Petri Net State Equation
我们提出了一种可达性验证技术，结合Petri网状态方程（一个线性代数overapproximation的可达状态集）的概念，反例指导抽象细化。本质上，我们通过搜索状态方程的解的空间来代替通过可达状态集的搜索。我们展示了出色的性能的技术在几个现实世界的例子。该技术在可达性查询产生负面结果的情况下特别有用：虽然基于状态空间的技术在这种情况下需要完全扩展状态空间，但我们的技术通常会立即终止。此外，我们可以得到一些诊断信息，在不可达的情况下，而状态空间方法只能在可达的情况下提供见证路径。
2012-09-28 cs.DS cs.LO
Occam's Razor Applied to the Petri Net Coverability Problem
并发系统的安全性验证问题往往归结为Petri网的可覆盖性问题。这个问题在40年前就被证明是ExpSpace完备的。在并发革命的推动下，它在过去十年中重新引起了人们的兴趣。在本文中，我们提出了一个通用的和简单的方法来解决这个问题。我们的方法的灵感来自最近的方法Blondin，Finkel，Haase和Haddad。基本上，我们结合了前向不变生成技术的Petri网与结构良好的过渡系统的向后可达性。实验评估表明，我们的方法的效率。
2016-07-18 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
A "Symbolic" Representation of Object-Nets (Extended Version)
本文针对基本对象系统（EOS，一种网中嵌套Petri网的形式体系）状态空间规模大的问题，将Petri网同态扩展至EOS，利用拓扑自同构的对称性压缩状态空间，为嵌套Petri网的状态分析提供了符号化方法。
2024-10-31 cs.LO
Parameterized Analysis of Immediate Observation Petri Nets
我们介绍即时观察Petri网，一类感兴趣的研究人口协议（分布式计算模型），和酶化学网络。在这些领域中，相关的分析问题转化为参数化的Petri网问题：具有相同底层网但不同初始标记的Petri网的无限集合是否满足给定的性质。研究了直接观察Petri网的参数化可达性、可覆盖性和活性问题。我们发现，所有这三个问题是在PSPACE的计数约束，一类足够丰富的预期应用程序定义的初始标记的无限集。这是值得注意的，因为当标记集是单例时，问题已经是PSPACE困难的，即，在非参数化的情况下。我们使用这些结果来证明即时观察人口协议的正确性问题是PSPACE完全的，回答了以前的论文中留下的一个问题。
2019-03-28 cs.LO
State Space Computation and Analysis of Time Petri Nets
Petri网理论提供了一个通用的框架来描述实时反应式系统的行为，时间Petri网的引入也考虑了时间规范。本文提出了一种基于前向区域的算法来计算有界时间Petri网的状态空间：该方法与经典的状态类图不同，并且更有效。我们证明该算法是精确的可达性问题。此外，我们提出了一个翻译的计算状态空间到一个时间自动机，证明了原来的时间Petri网的时间双相似。当该方法产生单个时间自动机时，可以应用语法时钟减少方法（例如Daws和Yovine）来产生具有更少时钟的自动机。然后，我们的方法允许通过使用高效的时间自动机工具进行模型检查TTPN。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2005-05-10 cs.LO
Verification of Immediate Observation Population Protocols
群体方案（Angluin等人，PODC，2004）是由相同的移动设备组成的传感器网络的正式模型。两个设备可以交互，从而改变它们的状态。计算是满足强公平约束的无限序列的交互。如果对于设备的每个初始配置$C$，以及从$C$开始的每个计算，所有设备最终都同意仅取决于$C$的共识值，则填充协议是良好指定的。如果一个协议是良好指定的，那么它被称为计算谓词，该谓词为每个初始配置分配其共识值。在以前的文件中，我们已经表明，一个给定的协议是否是指定的问题，以及它是否计算一个给定的谓词的问题是可判定的。然而，在同一篇论文中，我们证明了这两个问题至少是硬的可达性问题的Petri网。由于所有已知的Petri网可达性算法都具有非原始递归复杂性，因此在本文中，我们将注意力限制在即时观察（IO）种群协议上，这是在（Angluin et al.，PODC，2006年）。我们表明，这两个问题是可解的IO协议在指数空间。这是第一个语法定义的，有趣的一类协议，不需要Petri网可达性的算法被发现。
2018-08-13 cs.LO
On interleaving in {P,A}-Time Petri nets with strong semantics
在强语义背景下研究了{P，A}-时间Petri网（简称{P，A}-TPN）的可达性分析.它调查的凸性的工会的状态类达到不同的交错的同一套过渡。在BB 08中，作者考虑了T-TPN模型及其收缩状态类图（CSCG），并证明了该并集不一定是凸的。然而，他们建立了一些充分条件，确保凸性。本文证明了对于{P，A}-TPN的CSCG，这个并是凸的，并且可以在不计算中间状态类的情况下计算。这些结果可以提高前向可达性分析凝聚，在相同的状态类，所有的状态类达到不同的交错的同一组转换（抽象凸联盟）。
2010-11-01 cs.FL cs.LO
Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving
带抑制弧的参数时间Petri网（PITPN）允许参数在触发范围内，从而支持时间系统的灵活性。本文提出并证明了PITPN的一种具体的和符号化的重写逻辑语义。我们将展示如何使用Maude结合SMT解决方案，为PITPN提供完善的正式分析。我们开发了一个新的通用折叠符号可达性的方法，终止时的参数状态类图的PITPN是有限的。我们解释了几乎所有的形式分析和参数合成支持的国家的最先进的PITPN工具Roméo可以在Maude与SMT。此外，我们还支持从参数化初始标记进行分析和参数合成，以及使用用户定义的执行策略进行完整的LTL模型检验和分析。在三个基准上的实验表明，我们的方法在许多情况下优于Roméo。
2023-03-15 cs.LO
Goal-Driven Unfolding of Petri Nets
在探索Petri网的运行时，展开提供了一种有效的方法来避免由于并发变迁的交织而导致的状态空间爆炸。适当阶理论允许定义包含所有可达标记的展开的有限前缀。在本文中，我们感兴趣的是一个单一的给定标记，称为目标的可达性。我们提出了一个算法，用于计算一个1-安全的Petri网，保持达到这一目标的所有最小配置的展开的有限前缀。该算法将展开技术与动态模型降阶技术相结合，通过静态分析来降低模型降阶，避免了对不必要分支的探索。我们提出了一些实验结果。
2016-11-04 cs.FL cs.LO
On Petri Nets with Hierarchical Special Arcs
我们研究的可判定性的终止性，可达性，覆盖性和死锁的Petri网赋予了一个层次的地方，并与抑制弧，复位弧和转移弧，尊重这一层次。我们还研究了当我们有这些特殊的弧，其中一些尊重层次结构，而其他人不混合时会发生什么。我们解决了上述四个问题的可判定性状态的层次，抑制，重置和转移弧的所有组合，除了两个组合的终止问题。对于这两种组合，我们表明，终止问题是很难决定线性递归序列的积极性-一个长期存在的开放问题。
2017-07-04 cs.FL cs.LO
Reachability in Vector Addition Systems is Ackermann-complete
向量加法系统和等价Petri网是一种成熟的并发模型。向量加法系统的核心算法问题是可达性问题，它询问是否存在从一个给定配置到另一个给定配置的运行。我们解决了它的复杂性是阿克曼完全的，从而关闭了45年的问题。特别是，我们证明了这个问题是$\mathcal{F}_k$ -困难的向量加法系统的状态在维度$6k$，其中$\mathcal{F}_k$是$k$ -th复杂性类的层次结构的快速增长的复杂性类。
2022-10-25 cs.FL cs.LO
Stubborn Set Reduction for Two-Player Reachability Games
本文提出基于顽固集的偏序归约理论，用于双人可达性博弈，剪除两玩家交错行为，证明正确性，并实例化到加权Petri网博弈，在TAPAAL中实现，案例研究显示高效。
2021-03-17 cs.LO
On the Parameterized Complexity of Synthesizing Boolean Petri Nets With Restricted Dependency (Technical Report)
$τ$ -合成问题在于判定给定的有向标记图$A$是否同构于$τ$型布尔Petri网$N$的可达图。在肯定决策的情况下，应构建$N$。对于许多布尔类型的网，问题是NP完全的。本文论述了一个特殊的变形$τ$ -合成的目标净$N$施加限制：我们调查\emph{dependency $d$-restricted $τ$-synthesis (DR$τ$S)}的每个地方的$N$可以影响和最多的$d$过渡的影响。对于类型$τ$，如果$τ$ -合成是NP完全的，则DR $τ$ S也是NP完全的。在本文中，我们表明，由$d$参数化的DR $τ$ S在XP中。此外，我们证明了它是$W[2]$ -硬，对于许多布尔类型，允许无条件的相互作用$set$和$reset$。
2020-07-24 cs.CC cs.LO
Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests
针对带嵌套零检测的VASS可达性问题，本文得出Ackermann型上界，并提出统一方法以相同复杂度解决半线性性、可分离性等相关问题，填补了普通VASS部分问题的复杂度研究空白。
2025-05-19 cs.FL cs.LO
Senescent Ground Tree Rewrite Systems
已知具有状态的基础树重写系统具有不可判定的控制状态可达性问题。从最近引入的范围有界的多栈下推系统的灵感，我们定义衰老地面树重写系统。这些是具有状态的基础树重写系统的限制，使得树的节点在已经见证了先验固定数量的控制状态改变之后不再被重写。以及推广范围有界的多栈下推系统，我们表明-通过减少和重置Petri网-这些系统有一个阿克曼完全控制状态可达性问题。然而，正规树集的可达性仍然是不可判定的。
2013-11-19 cs.FL cs.LO
On the Reachability Problem for Two-Dimensional Branching VASS
本文研究了二维分支向量加法系统（BVASS）的可达性问题，证明了该问题在二维下是可判定的，并证明其可达集具有可计算的半线性表示。
2025-06-27 cs.FL cs.LO
Approaching the Coverability Problem Continuously
Petri网的可覆盖性问题在并发共享内存程序的验证中起着核心作用。然而，它的高EXPSPACE完全复杂性在现实世界的实例中遇到时构成了挑战。在本文中，我们开发了一种新的方法来解决这个问题，这主要是基于应用前向覆盖连续Petri网作为修剪标准内的向后覆盖框架。我们的方法的基石是最近开发的多项式时间算法的可达性在连续Petri网到SMT的有效编码。我们证明了我们的方法在文献标准基准测试中的有效性，这表明我们的方法比任何现有的工具决定了更多的实例，而且通常更快，特别是在大型实例上。
2016-01-09 cs.FL cs.LO
Reachability in Fixed VASS: Expressiveness and Lower Bounds
本文研究了固定 VASS 且仅初始配置可变时的可达性问题，证明固定 VASS 能完全表达自然数初始段算术，并揭示了一元配置下的弱归约及二元配置下五计数器 VASS 的 PSPACE-hard 下界。
2023-10-25 cs.FL cs.LO
Reasoning about Data Repetitions with Counter Systems
我们研究线性时间时态逻辑解释数据字多属性。我们将原子公式限制为连续位置中属性值的相等性和未来或过去属性值的重复性。我们证明了逻辑的可满足性问题和计数器系统的可达性决策问题之间的对应关系。我们表明，允许/不允许原子公式表示重复的值在过去对应的可达性/覆盖性问题的Petri网。这给了我们几个可满足性问题的2 EXPSPACE上界。我们证明匹配下界减少从一个新引入的一类计数器系统的可达性问题。这个新类是向量加法系统的简洁版本，其中计数器通过指针访问，这在其他上下文中是一个潜在的有用功能。我们进一步加强了数据逻辑和计数器系统之间的对应关系，通过描述逻辑的片段，扩展和变体的复杂性。例如，我们精确地描述了逻辑中允许的属性数量与计数器系统中所需的计数器数量之间的关系。
2016-07-29 cs.LO
Improving Reachability in Vector Addition Systems through Pumpability
Shanghai Jiao Tong University（上海交通大学）
本文研究了固定维度向量加法系统（VAS）的可达性问题，通过改进的泵性分析，得出了d维VAS可达性问题的F_{d-2}上界，优于传统VASS的F_d上界，并在低维VAS中取得新的上界结果。
2026-04-27 cs.FL cs.LO
Bridging the Gap Between Plain VASS and Branching VASS
University of Bordeaux, CNRS, Bordeaux INP（波尔多大学）；University of Warsaw（华沙大学）
本文研究分支VASS的可达性问题，证明其可达集是VASS的截面，并利用新的良拟序和融合性质，得出5维BVAS可达集有效半线性的结论。
2026-09-15 cs.FL cs.LO
Taking Complete Finite Prefixes To High Level, Symbolically
University of Oldenburg（奥尔登堡大学）；Université Paris-Saclay（巴黎萨克雷大学）；INRIA（法国国家信息与自动化研究所）；LMF CNRS（CNRS LMF实验室）；ENS Paris-Saclay（巴黎萨克雷高等师范学院）
本文提出高阶Petri网的完整有限前缀概念，扩展了Esparza等人算法，并通过原型实现评估了该方法在新型基准家族中的效果，同时识别了具有无限可达标记的更广泛网类。
2024-09-11 cs.FL cs.LO
Separators in Continuous Petri Nets
本文针对连续Petri网提出局部闭分离器，使不可达性可由多项式时间计算的分离器见证，且分离器验证属于NC，并进一步通过改造Petri网高效证明凸多面体集合间的不可达性。
2024-02-20 cs.FL cs.LO
Bounded LTL Model Checking with Stable Models
本文介绍了异步并发系统的有界模型检验，作为回答集编程的一个很有前途的应用领域。作为异步系统的通信自动机，1-安全Petri网的推广模型，使用。它示出了如何1-安全的Petri网和对网络的行为的要求可以被翻译成一个逻辑程序，这样的有界模型检验问题的网可以通过计算相应的程序的稳定模型来解决。稳定模型语义的使用导致有界可达性和死锁检测任务的紧凑编码，以及线性时序逻辑的有界模型检验的更一般的问题。给出了所设计的翻译的正确性证明，并给出了使用该翻译和Smodels系统的一些实验结果。
2003-05-23 cs.AI cs.LO
The Emptiness Problem for Valence Automata over Graph Monoids
这项工作的研究，在自动机的存储机制，允许可判定性的空虚问题。这个问题是正式使用价自动机，一个抽象的自动机模型，其中的存储机制是由幺半群。对于各种存储机制中的每一种，可以选择一个（通常是无限的）幺半群$M$，使得$M$上的价自动机等价于具有这种存储类型的（单向）自动机。事实上，许多重要的存储机制可以通过有限图定义的幺半群来实现，称为图幺半群。示例包括下推堆栈、部分盲计数器（其表现得像Petri网位置）、盲计数器（其可以获得负值）及其组合。因此，我们研究的图幺半群的空性问题的价自动机是可判定的。图幺半群实现的一个特殊模型是具有下推堆栈的Petri网。对于这些，可判定性是一个长期存在的开放性问题，我们在这里不回答它。然而，如果排除对应于该模型的子图，则可以实现特征化。此外，我们提供了一个描述的存储机制，决策仍然开放。这导致了一个模型，自然推广了下推Petri网和Reinhardt引入的优先级多计数器机。被证明是可判定的情况构成了一个自然的和显然是新的扩展的Petri网与可判定的可达性。最后表明，该模型可以与另一个这样的扩展Atig和Ganty：我们提出了进一步的可判定性结果，包括这两个Petri网扩展。
2017-10-20 cs.FL cs.LO math.GR
Approximate Computation of Reach Sets in Hybrid Systems
混杂系统中最重要的问题之一是{ \em可达性问题}。即使对于{ \em linear}混合系统的子类，可达性问题也是不可判定的.有鉴于此，在混合动力系统领域的主要焦点一直是找到{ \em有效}半决策程序，这个问题。这样的算法方法涉及找到计算方法和表示的连续变量的到达集内的混合系统的离散状态。本文在简要介绍混杂系统和可达性问题的基础上，提出了一种求解混杂系统中连续变量可达集的计算方法。此外，我们还描述了一个新的算法，用多面体过近似的线性动力学和多面体初始集的连续变量的可达集。我们说明这些算法与典型有趣的例子。
2002-02-07 cs.LO cs.SE
The Tractability Border of Reachability in Simple Vector Addition Systems with States
本文全面刻画了一元编码下 VASS 可达性的易处理性边界，证明了 3-SLPS 中可达性为 NP 困难，并提出了二进制配置下 2-SLPS 可达性的多项式时间算法。
2024-12-21 cs.FL cs.LO
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction
本文研究了实时的【形】系统的安全性验证与综合问题。我们介绍实时的【形】程序，这些程序由可以执行离散和实值变量赋值的指令组成。它们足够通用，可以捕获有趣的时间系统类，如时间自动机，秒表自动机，时间（d）Petri网和混合自动机。我们提出了一种使用轨迹抽象细化的半算法来解决实时的【形】程序的可达性验证问题和参数综合问题。所有提出的算法已经实施，我们已经进行了一系列的实验，比较我们的新方法的性能，以国家的最先进的工具，在经典的可达性，鲁棒性分析和参数合成定时系统。我们表明，我们的新方法提供了解决方案，这些问题是无法解决的，目前最先进的工具。
2020-07-21 cs.FL cs.LO cs.SY
Symbolic and Structural Model-Checking
本文提出结合SMT过近似、无记忆采样欠近似和结构化简规则，使模型检验复杂度与网结构而非状态空间成正比，并在2020年模型检验竞赛中赢得可达性查询和死锁检测。
2021-12-18 cs.DC cs.FL cs.LO
