arXiv 1304.63012013-04-23cs.LO

关于平计数器系统的正则性质的复杂性

On the Complexity of Verifying Regular Properties on Flat Counter Systems

Stéphane Demri, Amit Kumar Dhar, Arnaud Sangnier

摘要：

在计数器系统验证的近似方法中，其中之一是模型检验其平坦展开。不幸的是，除了可达性查询或过去的LTL模型检查问题的复杂性表征，这种业务模型并不总是很好地研究。在本文中，我们描述的复杂性的模型检测问题的平面计数器系统的规约语言，包括一阶逻辑，线性μ演算，无限自动机，和相关的形式主义。我们的研究结果跨越不同的复杂性类（主要是从PTime到PSpace），它们适用于计数器值的算术约束系统允许的语言。就证明技术而言，我们提供了一种集中于主要问题的统一方法。

英文摘要：

Among the approximation methods for the verification of counter systems, one of them consists in model-checking their flat unfoldings. Unfortunately, the complexity characterization of model-checking problems for such operational models is not always well studied except for reachability queries or for Past LTL. In this paper, we characterize the complexity of model-checking problems on flat counter systems for the specification languages including first-order logic, linear mu-calculus, infinite automata, and related formalisms. Our results span different complexity classes (mainly from PTime to PSpace) and they apply to languages in which arithmetical constraints on counter values are systematically allowed. As far as the proof techniques are concerned, we provide a uniform approach that focuses on the main issues.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

对从 MLTL 公式到正则表达式的转换的形式化验证

Formally Verifying a Transformation from MLTL Formulas to Regular Expressions

本文在 Isabelle/HOL 中形式化验证了将 MLTL 公式转换为等价正则表达式的 WEST 算法的正确性，并通过代码导出实验验证了现有 WEST 工具。

2025-01-29cs.LO

项重写系统抽象的时间正则性

Verifying Temporal Regular Properties of Abstractions of Term Rewriting Systems

树自动机完备化是一种用于证明系统的安全性的算法，这些系统可以由项重写系统建模。这种表示和验证技术适用于证明无限系统的属性，如加密协议或最近的Java字节码程序。该算法通过重写初始项来计算一个树自动机，它表示可达项集的（正则）过逼近。这种方法是有限的，缺乏信息重写之间的关系的条款。实际上，通过重写的关系项在同一等价类中：在树自动机中有相同的状态被识别。我们的目标是产生一个自动机嵌入一个抽象的重写关系足以证明时间属性的长期重写系统。我们建议扩展该算法，以产生一个自动机有更多的等价类，以区分一个长期或一个子项从其继任者w.r.t.重写基变换用于识别词项的等价类，而ε-变换表示词项之间的重写关系。从完成的自动机，它是可能的自动建立一个Kripke结构抽象的重写序列。Kripke结构的状态是树自动机的状态，并且转换关系由ε-转换的集合给出。Kripke结构的状态由使用基跃迁识别的项的集合来标记。在这个Kripke结构上，我们定义了正则线性时态逻辑（R-LTL）来表达属性。然后可以使用标准模型检验算法来检验这些属性。LTL和R-LTL之间的唯一区别是谓词被可接受的术语的规则集合替换。

2010-03-25cs.LO

满足Ω-正则稠密时间性质的概率时间自动机

Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties

概率时间自动机（Probably Timed Automata，PTAs）是一种扩展了离散概率分布的时间自动机（Timed Automata，TA），它作为一种数学模型，广泛应用于随机和时间行为。在这项工作中，我们考虑的问题，模型检查的线性\emph{dense-time}性质在{PTA}。特别是，我们研究了线性密集时间属性，可以编码的TA与无限的验收criterion.First，我们表明，模型检查PTA对确定性TA规格的问题可以通过产品建设解决。基于乘积结构，证明了确定性TA规格问题的计算复杂性是EXPTIME-完全的。然后我们证明了当放宽到一般的（非确定性的）TA时，模型检测问题变得不可判定，我们的结果大大扩展了TA的稠密时间特性和非确定性。

2018-06-13cs.FLcs.LO

FAR-Cubicle -一种新的Cubicle可达性算法

FAR-Cubicle - A new reachability algorithm for Cubicle

我们提出了一个全自动的算法来验证参数化软件系统的安全性。该算法基于IC 3和Lazy Annotation。我们在Cubicle中实现了它，Cubicle是一个用于验证基于数组的系统的安全属性的模型检查器。高速缓存一致性协议和互斥算法是这种系统的已知示例。我们的算法迭代地建立一个抽象的可达性图，从反例中提炼出可达状态集。精炼是通过反例近似。我们展示了该算法的有效性和局限性，以及由此产生的权衡。

2018-11-20cs.LO

基于$ω$ -正则线性时间特性的非确定概率信道系统

Verifying nondeterministic probabilistic channel systems against $ω$-regular linear-time properties

有耗信道系统（Lossy Channel Systems，LCS）是一种通过不可靠的无界FIFO信道进行通信的有限状态自动机系统。为了规避不确定LCS的模型检验的不确定性，引入了概率模型，其中可以确定线性时间属性是否几乎肯定成立。然而，这样的完全概率系统不是非确定性协议的忠实模型。我们研究了一个混合模型的LCS的消息丢失被视为故障发生的一些给定的概率，系统的内部行为仍然是不确定的。因此，语义是在无限状态马尔可夫决策过程。本文的目的是讨论由线性时态逻辑（LTL）公式形式化的线性时间性质的可判定性。我们的重点是定性设置，其中一个问，例如，LTL公式几乎肯定成立还是零概率成立（如果公式描述了不良行为）。令人惊讶的是，事实证明，-在有限状态马尔可夫决策过程-LTL公式的满意度关系取决于所选择的类型的决策者，解决了不确定性。虽然所有的变量的定性LTL模型检验问题的完整类的历史相关的调度器是不可判定的，同样的问题，有限内存调度器可以解决算法。然而，可达性属性和特殊种类的经常性可达性属性的限制产生可判定的验证问题的完整类的验证，其中-这类限制的属性-是强大的有限内存的验证，甚至是他们的子类。

2006-04-11cs.LO

验证恒速率多模式系统的线性时序规约

Verifying linear temporal specifications of constant-rate multi-mode systems

本文提出面向恒速率多模式系统的 LTL 变体，并刻画其句法子片段的模型检验复杂度，得到 P 完全、NP 完全或不可判定的统一分类。

2023-04-26cs.CCcs.FLcs.LO

更多相关论文收起更多论文

Reluplex：一个高效的深度神经网络SMT求解器

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

Stanford University（斯坦福大学）

深度神经网络已经成为解决复杂现实问题的广泛使用和有效的手段。然而，将它们应用于安全关键系统的一个主要障碍是很难提供关于其行为的正式保证。我们提出了一种新的，可扩展的，有效的技术来验证深度神经网络的属性（或提供反例）。该技术基于单纯形方法，扩展到处理非凸整流线性单元（ReLU）激活函数，这是许多现代神经网络的关键组成部分。验证过程将神经网络作为一个整体来处理，而不做任何简化的假设。我们评估了我们的技术上的原型深度神经网络实现的下一代无人机机载防撞系统（ACAS徐）。结果表明，我们的技术可以成功地证明比使用现有方法验证的最大网络大一个数量级的网络的属性。

2017-05-19cs.AIcs.LO

通过安全区域的线性近似验证飞机碰撞避免神经网络

Verifying Aircraft Collision Avoidance Neural Networks Through Linear Approximations of Safe Regions

Stanford University（斯坦福大学）；University of Michigan（密歇根大学）

本文提出通过线性近似安全区域的方法来验证飞机碰撞避免神经网络的安全性，利用Reluplex工具检查是否存在不安全的建议，并通过训练神经网络发现数千个不安全的反例。

2019-03-02cs.LOcs.SYeess.SY

利用变换生成模型检验反例

Generating Counterexamples for Model Checking by Transformation

反例解释了为什么所需的时间逻辑属性无法保持。反例的产生被认为是模型检验作为一种验证技术的主要优点之一。此外，当模型检验确实成功地验证了属性时，通常不存在可用作已验证属性的证据的独立可检验见证。在此之前，我们已经展示了程序转换技术如何用于验证反应系统的安全性和活性特性。然而，没有反例或证人使用所描述的技术产生。在本文中，我们将讨论这个问题。特别是，我们展示了如何程序转换技术蒸馏可以用来促进反应系统的时间属性的反例和证人的建设。示例系统的目的是相互排斥模型进行分析，使用这些技术的安全性（相互排斥）和活性（非饥饿），与反例生成的那些属性不举行。

2016-07-08cs.LOcs.SE

拜占庭将军的反击：容错分布式算法的参数化模型检验

Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms

我们介绍了一种用于容错分布式算法（FTDA）的自动参数化验证方法。FTDA由进程数和假定的拜占庭故障进程的最大数目参数化。在我们的技术的中心是一个参数区间抽象（PIA）的区间边界是参数的算术表达式。使用PIA的数据抽象和一种新形式的计数器抽象，我们减少了参数化的问题，有限状态模型检验。我们证明了我们的方法的实际可行性，通过验证Srikanth和Toueg著名的分布式算法的几个变种。我们的半决策程序的补充和动机的不可判定性证明FTDA验证，即使在没有进程间通信。据我们所知，这是第一篇实现拜占庭FTDA参数化自动验证的论文。

2013-02-03cs.DCcs.LO

超越$ω$ BS-正则语言：$ω$ T-正则表达式和反检查自动机

Beyond $ω$BS-regular Languages: $ω$T-regular Expressions and Counter-Check Automata

在过去的几年里，人们提出了各种各样的ω-正则语言的扩展，包括ω B-正则语言（有界扩展的ω-正则语言），ω S-正则语言（严格无界扩展的ω-正则语言）和ωBS-正则语言（ωB-正则语言和ω S-正则语言的组合）。而前两类满足广义闭包性质，即ω B-正则的补（分别为，ω S-正则）语言是一种ω S-正则（或ω B-正则）一，最后一类在补下不闭。非ωBS-正则语言的存在是某些ω BS-正则语言的补充，并且表达了反应系统的相当自然的性质，这促使人们寻找其他行为良好的扩展ω-正则语言。本文引入了一类ωT-正则语言，它包含了非ω BS-正则的有意义语言。我们首先用ω T-正则表达式来定义它。然后，我们引入了一类新的自动机（反检查自动机），并证明了（i）它们的空性问题在PTIME中是可判定的，（ii）它们具有足够的表达能力来捕获ωT-正则语言（ωT-正则语言关于反检查自动机是否是表达完备的仍然是一个悬而未决的问题）.最后，我们给出了ω T正则表达式到S1 S +U的编码。

2017-09-07cs.FLcs.LO

基于归约到有限计数器系统的异步轮次分布式算法的参数化验证

Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems

Univ Rennes, Inria, CNRS, IRISA（雷恩大学、法国国家信息与自动化研究所、法国国家科学研究中心、IRISA）；The University of Sydney（悉尼大学）

针对无限状态异步轮次分布式算法，提出归约到有限计数器系统的参数化验证方法，并证明其完备性，通过nuXmv验证了共识与领导者选举算法。

2026-06-29cs.FLcs.LO

单计数器语言的正则抽象的复杂性

Complexity of regular abstractions of one-counter languages

我们研究了以下转换的计算和逻辑复杂性：给定一个单计数器自动机（OCA）A，构造一个非确定性有限自动机（NFA）B，它识别语言L（A）的抽象：（1）向下闭包，（2）向上闭包，或（3）Parikh图像。对于帕里克图像在一个固定的字母表和向上和向下的封闭，我们发现多项式时间算法计算这样的NFA。对于Parikh图像的字母作为输入的一部分，我们找到了一个准多项式时间算法，并证明了一个完整的结果：我们构造了一个序列的OCA，承认多项式时间算法当且仅当有一个为所有的OCA。对于所有三个抽象，以前不知道是否存在适当的亚指数大小的NFA。

2016-02-10cs.FLcs.LO

基于SMT的无界软件模型检验中的自动抽象

Automatic Abstraction in SMT-Based Unbounded Software Model Checking

基于欠近似和SMT求解器的软件模型检查器在验证安全性（即可达性）属性方面非常成功。它们结合了两个关键思想-（a）“具体性”：在一个下近似的反例是一个反例，以及在原来的程序，和（b）“泛化”：一个下近似的安全性证明，由SMT求解器，是可推广到原程序的安全性证明。在本文中，我们提出了一个“自动抽象”与近似驱动的框架。我们探讨了两种迭代的方法来获得和细化抽象-“基于证明”和“基于反例”-并展示了它们如何组合成一个统一的算法。据我们所知，这是基于证明的抽象的第一个应用程序，主要用于验证硬件，软件验证。我们已经实现了一个原型的框架使用Z3，并评估它的许多基准软件验证比赛。我们的实验表明，我们的组合是非常有效的硬的情况下。

2013-06-08cs.LOcs.PL

将数组验证问题编码为无数组Horn子句

An encoding of array verification problems into array-free Horn clauses

自动验证程序的安全属性是困难的，如果程序作用于数组或其他形式的映射，则更难。存在许多方法来验证程序操作上的布尔和整数值（例如抽象的解释，反例引导的抽象细化使用插值），但转置它们数组属性已充满了困难。与大多数以前的方法相比，我们不引入一个新的抽象域或一个新的插值过程数组。相反，我们生成一个抽象的标量问题，并将其提供给一个预先存在的求解器，与可调precision.Our转换的问题表示使用霍恩条款，一个共同的格式与明确和明确的逻辑语义验证问题。我们的编码的一个重要特点是，它创建了一个非线性的霍恩问题，与树展开，即使下面的“平坦”的控制图结构通常会产生一个线性的霍恩问题，与线性展开。也就是说，我们的编码不能表示成另一个控制流图问题的编码，并真正利用霍恩子句格式的能力。我们说明了我们的方法与选择排序的功能正确性的完全自动化的证明。

2015-09-30cs.LOcs.PL