Formal Modeling and SMT-Based Parameterized Verification of Multi-Case Data-Aware BPMN
我们提出了DAB --BPMN事实标准的一个数据感知扩展，它具有对case和持久数据进行操作的能力（分为只读目录和读写存储库），并在表达能力和支持安全属性的参数化验证的可能性之间进行平衡。特别是，我们从工件系统验证的文献中获得灵感，并且考虑其中与只读目录的内容无关地检查安全属性的验证问题，可能考虑目录和储存库中的活动情况和元组的无限数量。这些问题的解决使用完全实现的基于阵列的向后可达性技术属于良好的SMT模型检验的传统。我们还确定了相关类的DAB的MCMT阵列为基础的模型检查器中实现的向后可达性程序是健全和完整的，然后进一步加强这些类，以确保终止。
2019-06-20 cs.LO
Liveness of Parameterized Timed Networks
研究了具有多时钟的参数化离散时间网络形式的无限状态系统的模型检验问题。我们表明，这个问题是可判定的B-或S-自动机的规格。这样的规范是非常有表现力的（他们严格submerga-regular规范），并且很容易表达复杂的活性和安全属性。我们的结果是通过使用对称广播来模拟时间的流逝，并通过解决使用k-wise交会和对称广播通信的非定时过程的参数化系统的模型检验问题而获得的。我们的可判定性证明利用自动机理论，合理的线性规划和几何推理来解决向量加法系统中的某些可达性问题，我们相信这些证明技术将有助于解决相关问题。
2016-09-14 cs.LO
Parameterized Analysis of Immediate Observation Petri Nets
我们介绍即时观察Petri网，一类感兴趣的研究人口协议（分布式计算模型），和酶化学网络。在这些领域中，相关的分析问题转化为参数化的Petri网问题：具有相同底层网但不同初始标记的Petri网的无限集合是否满足给定的性质。研究了直接观察Petri网的参数化可达性、可覆盖性和活性问题。我们发现，所有这三个问题是在PSPACE的计数约束，一类足够丰富的预期应用程序定义的初始标记的无限集。这是值得注意的，因为当标记集是单例时，问题已经是PSPACE困难的，即，在非参数化的情况下。我们使用这些结果来证明即时观察人口协议的正确性问题是PSPACE完全的，回答了以前的论文中留下的一个问题。
2019-03-28 cs.LO
Parameterized Verification of Systems with Global Synchronization and Guards
受分布式应用程序的启发，使用共识或其他协议的全球协调，我们定义了一个新的计算模型参数化系统，是基于一个通用的全球同步原语，并允许全球过渡警卫。我们的模型推广了许多现有的模型在文献中，包括广播协议和守护协议。我们表明，可达性属性是可判定的系统没有警卫，并给出充分条件下，他们仍然可判定的警卫。此外，我们调查截止的可达性属性，并提供了足够的条件，在一些情况下，我们的目标应用程序的启发小截止。
2021-05-06 cs.DC cs.FL cs.LO
Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version)
我们提出了DAB --BPMN的一个数据感知扩展，该过程在案例和持久性数据上运行（分为一个称为目录的只读数据库和一个称为存储库的读写数据库）。该模型的表达能力和支持参数化验证的安全属性的可能性之间的权衡。具体而言，从文献中的灵感验证的工件系统，我们研究的安全属性检查无关的只读目录的内容，并接受潜在的存在无限的许多元组的目录和存储库中的验证问题。我们解决这样的问题，使用一个基于数组的向后可达性过程完全实现MCMT-一个国家的最先进的基于数组的SMT模型检查。值得注意的是，我们证明了该程序是健全的和完整的检查安全的DAB，并挑选出额外的条件，保证其终止，反过来，检查安全的可判定性。
2019-06-24 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
The Complexity of Reachability in Affine Vector Addition Systems with States
该研究刻画了仿射VASS中整数可达性的复杂性，给出三分法：重置类NP完全，转移/复制类PSPACE完全，其余不可判定；标准可达性仅置换类可判定，并探讨了固定实例的复杂性任意性。
2021-07-19 cs.CC cs.FL 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
Parameterized Verification of Disjunctive Timed Networks
本文提出了一种基于新颖区域图算法的析取时间网络（DTNs）参数化验证新技术，通过解决最小时间可达性问题构建摘要时间自动机，避免了指数级截断系统的构建，并在特定时钟不变式条件下扩展了适用性。
2024-01-02 cs.FL cs.LO
Characterizing Structural Hardness of Logic Programs: What makes Cycles and Reachability Hard for Treewidth?
答案集编程（ASP）是一个问题建模和解决框架的几个问题，在KR与日益增长的工业应用。ASP也是近年来研究计算复杂性和深入理解计算难度及其来源的一个热点。这些研究导致了富有成效的表征方面的复杂性类，细粒度的见解形式的二分法风格的结果，以及详细的参数化的复杂性景观。最近，这导致了一个新的结果，建立的措施树宽，它捕获的程序的结构密度，评估的知名类正常的程序预计将稍微困难比决定可满足性（SAT）。然而，目前还不清楚如何利用ASP的这种结构性力量。本文论述了一种新的减少SAT到正常的ASP，超越了众所周知的编码：我们明确利用ASP的结构功率，从而我们次线性地减少树的宽度，这可能无法显着改善。然后，与现有的结果相比，这通过建立依赖图的周期长度（SCC大小）对树宽的所需函数依赖来以细粒度的方式表征硬度。
2023-01-18 cs.AI cs.DM cs.LO
Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems
本文研究了带离散时钟的参数化离散时间系统的模型检测复杂度，通过引入对称广播通信原语，证明了无控制器系统的安全性规范是PSPACE完全的、活性规范在EXPTIME内可判定，并揭示了带控制器系统的活性规范不可判定。
2025-06-23 cs.LO
On the Complexity of Bounded Context Switching
有界上下文切换（BCS）是一种用于发现共享内存并发程序中违反安全属性的欠近似方法。从技术上讲，BCS是一个已知为NP完全的可达性问题。我们的贡献是BCS的参数化分析。第一个结果是一个算法，当通过上下文切换的数量（cs）和内存大小（m）参数化时，该算法在O*（m^（cs）2^（cs））中求解BCS。这是通过创建更简单的问题Shuff的实例来实现的，我们通过快速子集卷积来解决该问题。基于指数时间假设，我们还提出了BCS的形式m^o（cs / log（cs））的下界。有趣的是，缩小差距意味着解决一个自FOCS'07以来一直开放的猜想。此外，我们证明了BCS承认没有多项式核。接下来，我们引入一个称为调度维度的度量，它可以捕获调度的复杂性。我们研究了调度维（sdim）参数化的BCS，并表明它可以在O*（（2 m）^（4sdim）4^t）$，其中t是线程的数量。我们考虑的问题，我们获得（匹配）的上限和下限的变种。
2017-04-24 cs.FL cs.LO
The Complexity of Flat Freeze LTL
本文研究单计数器自动机上平坦冻结LTL的模型检验问题，证明其NEXPTIME完全，并通过交替双向自动机模拟实现NP可达性算法，同时为参数定时自动机可达性提供新证明。
2019-10-15 cs.FL cs.LO
Parameterized Verification of Algorithms for Oblivious Robots on a Ring
IRIF - Univ Paris Diderot（巴黎狄德罗大学 IRIF）；Sorbonne Universités, UPMC Univ Paris 06（索邦大学 皮埃尔和玛丽·居里大学）
我们研究验证问题的自主群的移动机器人，自组织和合作，以解决全球目标。特别是，我们专注于在本文中提出的模型由铃木和山下的匿名机器人在一个离散的空间与有限数量的位置（在这里，一个环）。已经提出了大量的算法工作的环，其大小不是先验固定的，因此可以被认为是一个参数。这些算法的手工正确性证明已被证明是容易出错的，最近的注意力已经给予了正式的方法来自动证明这些应用程序。我们的工作是第一个研究的验证问题，这样的算法在参数化的情况下。我们表明，安全性和可达性问题是不可判定的机器人异步进化。在积极的一面，我们表明，安全属性是决定在同步的情况下，以及在异步的情况下，一类特定的算法。协议的几个属性也可以决定。决策过程依赖于Presburger算法公式中的编码，该公式可以通过SMT求解器进行验证。我们的方法的可行性证明了几个案例研究的编码。
2017-06-16 cs.CC cs.DC cs.DS
Fine-Grained Complexity of Safety Verification
我们研究了细粒度的复杂性的领导贡献者可达性（LCR）和有界阶段可达性（BSR），两个变种的安全验证问题的共享内存并发程序。对于这两个问题，内存是有限数据域上的单个变量。我们的贡献是新的验证算法和下界。后者基于指数时间假设（ETH），问题集覆盖和交叉组合。LCR是一个指定的领导者线程在与一定数量的同等贡献者线程交互时是否会达到不安全状态的问题。我们建议两个参数化：（1）通过数据域D的大小和领导者L的大小，以及（2）通过贡献者C的大小。我们提出了这两种情况下的算法。其关键技术是紧凑证人和动态规划。算法的运行时间为O*（（L（D+1））^（LD）* D^D）和O*（2^C），这表明两种参数化都是固定参数的。我们通过（匹配）基于ETH和Set Cover的下界来补充上界。此外，我们证明了多项式核的情况下。对于BSR，我们考虑涉及t个不同线程的程序。我们将分析限制在写权限在线程之间更改s次的计算上。BSR询问给定的配置是否可以通过这样的s阶段计算到达。当用P（线程的最大大小）和t参数化时，有趣的观察是，问题有大量的困难实例。形式上，我们表明，没有多项式核，没有压缩算法，减少数据域D的大小或阶段s的数量多项式依赖于P和t。这表明，符号方法可能更难找到这个问题。
2020-01-10 cs.DC cs.DS cs.LO
Expiring opacity problems in parametric timed automata
针对实时系统的时间泄露问题，提出过期时间不透明性定义，研究时间自动机中满足不透明性的时间界限的可计算性及相关参数化问题的可判定性。
2024-03-12 cs.CR cs.LO
