Equivalence-Checking on Infinite-State Systems: Techniques and Results
Antonin Kucera, Petr Jancar
本文介绍了一个选择最近开发的和/或使用的技术，等价检查无限状态系统，和最新的概述现有的结果（截至2004年9月）。
The paper presents a selection of recently developed and/or used techniques for equivalence-checking on infinite-state systems, and an up-to-date overview of existing results (as of September 2004).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Model-Checking Process Equivalences
过程等价是一种形式化的方法，它将程序和系统联系起来，这些程序和系统在非正式的情况下以相同的方式运行。由于没有唯一的概念，这意味着两个动态系统显示相同的行为有大量的形式过程等价，从互模拟跟踪等价，分类在线性时间分支时间谱。我们提出了一个逻辑框架的基础上表达模态不动点逻辑，它是能够定义许多过程等价关系：对于每个这样的等价有一个固定的公式，这是满足一对过程，当且仅当他们是等价的，就这个关系。我们解释了如何做模型检验，甚至象征性地，这个逻辑的一个重要片段，捕捉许多过程的等价。这允许将模型检验技术用于过程等价性检验。我们展示了如何部分评估可以用来获得决策程序的通用模型检验计划的过程等价。
Automated Verification of Quantum Protocols by Equivalence Checking
本文介绍了一种用于各种量子信息处理协议形式化验证的技术和工具。该工具采用稳定器形式化，能够表示并发量子协议，比量子电路更具有表达能力。我们还报告了使用我们的量子等价性（QEC）来分析一系列量子信息处理协议的实验结果。
On Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time
我们提出了一个拟线性时间算法来解决自然代数结构上的字问题，我们称之为正补二半格，布尔代数的一个子理论。我们使用作为一个基地的变化Hopcroft，Ullman和Aho算法的树同构，我们结合一个长期重写系统，以决定两个条款的等价。我们证明了重写系统是可终止的和汇合的，因此存在一个范式，我们的算法是计算它。我们还讨论了应用程序，并提出了一个有效的实现在Scala中。
Equivalence Checking By Logic Relaxation
我们介绍了一个新的框架的等价性检查（EC）的布尔电路的基础上的一般技术称为逻辑松弛（LoR）。LoR的本质是放松要求解的公式，并计算新行为集的超集S。也就是说，S包含所有新的满足由于松弛而出现的分配，并且不包含满足原始公式的分配。集合S是由称为部分量词消去的过程生成的。如果所有可能的坏行为都在S中，那么原始公式就不可能有它们，因此这个公式所描述的性质成立。欧共体对《规则》的吸引力是双重的。首先，它有助于生成强大的归纳证明。其次，证明不等价归结为检查放松公式中存在的一些不良行为，即在原始公式的更简单版本中。我们给出了一些实验证据，支持我们的方法。
Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code
高能效和高性能嵌入式软件的开发越来越依赖于对源代码关键部分进行复杂转换。设计师应用这种非平凡的源代码转换往往面临的问题，以确保功能等效的原始和转换后的程序。目前，他们不得不依赖于不完整和耗时的模拟。形式化的自动验证的转换程序对原来的是可取的。这就需要类似于比较数字电路的等价性检查工具。我们提出了这样一个工具来比较数组密集型相关的程序，通过组合的重要的全球性的转换，如表达式传播，循环和代数变换。当转换后的程序未能通过等价性检查时，该工具会提供有关错误可能位置的具体反馈。
Equivalence Checking and Simulation By Computing Range Reduction
我们介绍了新的方法的等价性检查和模拟的基础上计算范围减少（CRR）。给定一个组合电路$N$，CRR问题是计算如果不考虑$N$的一组输入，则从$N$的范围中消失的一组输出。重要的是，在许多情况下，即使计算$N$的整个范围是不可行的，也可以有效地找到范围缩减。通过CRR解决等价性检查有助于生成模仿“切割传播”方法的等价性证明。商业工具已经成功地使用了这种方法的有限版本。通过仿真对电路$N$进行功能验证可以被视为降低计算$N$范围的复杂性的一种方式。不是查找$N$的整个范围并检查它是否包含错误输出，而是仅针对一个输入计算这样的范围。CRR仿真提供了一种处理复杂距离计算的替代方法。其思想是排除$N$的输入子集，并计算由这种排除引起的范围减小。如果消失的输出集包含错误输出，则$N$存在错误。
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
我们提出了一个有界等价性验证技术的高阶程序与局部状态。该技术结合了完全抽象的符号环境互模拟类似的符号游戏语义，新的技术，轻量级的状态不变的注释。这产生了没有假阳性或假阴性的等效性验证技术。该技术是有界完备的，因为所有的不等式都是自动检测到足够大的界限。此外，几个硬等价证明自动或后被注释与状态不变量。我们在一个名为Hobbit的工具原型中实现了该技术，并使用一组广泛的新的和现有的示例对其进行基准测试。霍比特人可以证明许多经典的等价关系，包括所有迈耶和西伯的例子。
Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version)
半导体公司越来越多地采用一种从C/C++/SystemC的系统级设计规范开始的方法。该模型经过广泛模拟，以确保正确的功能和性能。随后，在Verilog中创建寄存器传输级（RTL）实现，可以由设计人员手动创建，也可以由高级综合工具自动创建。必须检查C和Verilog程序是否一致。在本文中，我们提出了一个两步的方法，体现在两个等价性检查工具，VERIFOX和HW-CBMC，分别在软件和RTL级验证设计。VERIFOX用于对C中的非定时软件模型与C中的高级参考模型进行等价性检查。HW-CBMC验证了一个Verilog RTL实现与一个C语言非定时软件模型的等价性。为了评估我们的工具，我们将它们应用于ARM的商业浮点运算单元（FPU）和开源双路浮点加法器。
PEQcheck: Localized and Context-aware Checking of Functional Equivalence (Technical Report)
重构不得改变程序的功能。然而，并不是所有的重构都满足这个要求。因此，必须明确检查重构不会改变功能。由于很少有一个正式的规格说明程序的行为，我们利用原来的程序作为功能规范。然后，我们检查原始程序和重构后的程序在功能上是否等价。为此，我们采用一个共同的想法，减少等价性检查程序验证。为了提高效率，我们的等价性检查PEQcheck构造一个验证任务，每个重构的代码段，而不是一个功能，通常由以前的工作。此外，PEQcheck考虑代码段的上下文。例如，只有被修改的和活的变量才需要是等效的，只读变量可以在原始代码段和重构的代码段之间共享。此外，我们的评估证明，本地化和上下文感知检查执行的\peqcheck确实可以是有益的。
On Neural Network Equivalence Checking using SMT Solvers
如果两个预训练的神经网络对相同的输入产生相似的输出，则它们被认为是等效的。神经网络的等价性检查是非常重要的，因为当需要满足额外的要求或解决安全威胁时，其在用等价的组件替换学习使能的组件中的实用性，例如当使用知识蒸馏、对抗训练等时。SMT求解器可以潜在地提供对神经网络等价性检查的问题的解决方案，其将是健全和完整的，但是正如所预期的，任何这样的解决方案都与关于要检查的神经网络的大小的显著限制相关联。这项工作提出了第一个基于SMT的编码的等价性检查问题，探讨其效用和局限性，并提出了未来的研究和改进途径，以实现更可扩展和实际适用的解决方案。我们目前的实验结果，揭示了上述问题，不同类型的神经网络模型（分类器和回归网络）和等价性标准，对一个通用的和应用程序无关的等价性检查方法。
Algorithmic metatheorems for decidable LTL model checking over infinite systems
通过算法元定理的模型检验问题P在无限状态系统，我们的意思是通用的结果，可以用来推断的可判定性（可能的复杂性）的P不仅在一个特定的类的无限系统，但在一个大家庭的类的无限系统。这样的结果通常开始于一个强大的形式主义的无限状态系统，其中P是不可判定的，并断言可判定时，通过一个额外的“语义条件”C的限制。我们证明了各种算法的元定理的问题的模型检验LTL和它的两个共同的片段LTL（Fs，Gs）和LTLdet的表达类的字/树自动转换系统，这是由有限的字和树上操作的同步有限状态转换器。我们提出了许多应用程序，在那里我们得到（以统一的方式）模型检验LTL及其片段在特定类别的无限状态系统上的许多已知和先前未知的可判定性和复杂性结果，包括下推系统;前缀可识别系统;具有离散时钟和自由计数器的反向有界计数器系统;具有有界数目的上下文切换的并发下推系统; Petri网的各种子类;弱扩展PA过程;和弱扩展地树重写系统。在所有情况下，我们都能够得到最优（或接近最优）的复杂度。最后，我们查明的确切位置在算法和分析层次的问题，检查相关的语义条件和LTL模型检验问题在所有字/树自动系统。
Effective Marking Equivalence Checking in Systems with Dynamic Process Creation
这项工作的出发点是一个框架，允许对具有动态进程创建的系统进行建模，配备了检测对称执行的过程（即，其区别仅在于过程的身份）。这允许减小状态空间，潜在地减小到指数级更小的大小，并且因为进程标识符从不被重用，所以这还允许将一些无限状态空间减小到有限大小。然而，在这种方法中，检测对称性的过程不允许计算高效的算法，主要是因为每个新计算的状态必须与每个已经达到的状态进行比较。在本文中，我们提出了一种新的方法来检测在这个框架中的对称性，将解决这个问题，从而使有效的算法。我们形式化了状态的规范表示，并确定了所分析模型的充分条件，以保证可以检测到所有对称性。对于不属于这一类的模型，我们的方法仍然是正确的，但不能保证最大限度地减少状态空间。
FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines
FastLEC通过混合引擎和优化策略，显著提升数据路径等效性检查的效率，证明速度比现有工具提高超5倍。
Equivalence Checking in Embedded Systems Design Verification using PRES+ model
本文主要研究嵌入式系统的建模和形式化验证。已经提出了许多模型来表示嵌入式系统。这些模型涵盖了广泛的风格，特点和应用领域，包括有限状态机，数据流图，通信过程和Petri网的扩展。在本报告中，我们使用了PRES+模型（基于Petri网的嵌入式系统表示）作为经典Petri网模型的扩展，该模型捕获了嵌入式系统的并发性和时序行为;它允许系统在不同的抽象级别中具有代表性，并通过允许令牌携带信息来提高表达能力。如上所述，使用PRES+建模可能便于指定输入行为，因为它支持并发性。然而，据我们所知，文献中没有报道PRES+模型的等价性检查方法。相反，存在FSMD模型的等价性检查。因此，作为第一步，我们寻求设计一种算法来将PRES+模型转换为FSMD模型，并且我们寻求在现实生活中的示例上手动执行我们的算法，并且我们必须将两个版本的PRES+模型转换为FSMD模型。然后使用现有的等价性检查器，我们已经检查了两个FSMD模型之间的等价性。
Equivalence Checking in Embedded Systems Design Verification
在这份报告中，我们专注于嵌入式系统的建模和形式化验证相关的一些方面。已经提出了许多模型来表示嵌入式系统。这些模型涵盖了广泛的风格，特点和应用领域，包括有限状态机，数据流图，通信过程和Petri网的扩展。在本报告中，我们使用了PRES+模型（基于Petri网的嵌入式系统表示）作为经典Petri网模型的扩展，该模型捕获了嵌入式系统的并发性和时序行为;它允许系统在不同的抽象级别中具有代表性，并通过允许令牌携带信息来提高表达能力。如上所述，使用PRES+建模可能便于指定输入行为，因为它支持并发性。然而，据我们所知，文献中没有报道PRES+模型的等价性检查方法。相反，存在FSMD模型的等价性检查。作为第一步，因此，我们试图设计一个算法，将PRES+模型FSMD模型。
Infinite State Model Checking by Learning Transitive Relations
通过学习传递关系，该方法扩展无限状态系统以证明安全性，结合递归分析与投影发现析取关系，并在LoAT工具中展现出强大的竞争力。
Octopus: Practical Equivalence Checking of P4 Packet Parsers
针对 P4 报文解析器，提出 Octopus 工具将其转成自动机并符号化检查等价性，可在消费级硬件上数分钟内完成非平凡解析器的等价性检查，还评估了其网络场景可用性。
Stateless Model Checking under a Reads-Value-From Equivalence
无状态模型检验是并行程序验证的标准方法之一。由于调度的非确定性创建指数级大的线程交织空间，SMC试图将此空间划分为等价类，并只探索每个类的几个代表。这种方法的效率取决于两个因素：（a）划分的粗糙度，以及（b）在每个类中生成代表的时间。出于这个原因，寻找粗划分，有效地探索是一个积极的研究挑战。在这项工作中，我们提出了RVF-SMC，一个新的SMC算法，使用一种新的\emph{reads-value-from (RVF)}分区。直觉上，如果两个交错在每个读取事件中获得的值上一致，则它们被认为是等效的，并且读取事件在它们之间诱导一致的因果排序。RVF分区是可证明的粗糙比最近的方法的基础上Mazurkiewicz和“读取”分区。我们的实验评估表明，RVF往往是一个非常有效的等价，因为底层的分区是指数比其他方法粗糙。此外，RVF-SMC生成的代表非常有效，因为减少在分区往往是符合显着的加速在模型检验任务。
A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking
本文提出一种基于多面体抽象的Petri网约简方法，结合SMT模型检验器，通过等价关系保证正确性，并在SMPT工具中实现BMC和PDR，实验验证其有效性。
Strong Equivalence for LPMLN Programs
LPMLN是一个概率扩展的答案集程序的权重方案改编自马尔可夫逻辑。我们研究了LPMLN中强等价的概念，这是一个有用的数学工具，简化了LPMLN程序的一部分，而不看它的其余部分。我们表明，在LPMLN中的强等价性的验证可以减少到等价性检查，在经典逻辑通过约简和选择规则，以及在“软”逻辑下的等价性检查这里和那里。结果使我们能够利用答案集求解器进行LPMLN强等价性检查。该研究还建议我们使用选择规则，这里和那里的逻辑和经典逻辑的LPMLN语义的一些重新表述。
CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems (Technical Report)
本文提出了一种基于上下文自由图文法的无限族有限状态标记转换系统CTL*模型检查方法，并通过实验验证了其有效性。
Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
在本文中，我们研究了一个模型的量子马尔可夫链，这是一个量子模拟的马尔可夫链，并得到取代概率的转移矩阵与量子操作。我们表明，这个模型是非常适合描述的混合动力系统，包括一个量子组件和一个经典的，虽然它具有相同的表达能力，另一个量子马尔可夫模型在文献中提出的。事实上，在量子信息处理中经常会遇到混合系统;例如，量子程序和量子协议都可以被视为混合系统。因此，我们进一步提出了一个称为混合量子自动机（HQA）的模型，可以用来描述这些从外部世界接收输入（动作）的混合系统。我们证明了HQA的语言等价问题是多项式时间可判定的。此外，我们将这个结果应用到量子马尔可夫链的迹等价问题，从而它也是多项式时间可判定的。最后，我们讨论了量子马尔可夫链的线性时间性质的模型检验，并表明可以成功地解决正则安全性的定量分析。
Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction
提出Irene框架，通过保结构符号化简在门级、混合路径和及密度核三个层次验证混合量子程序等价性，在1982个程序对中解决79.92%，并发现15个编译器缺陷。
Parity Game Reductions
奇偶博弈在模型检验和可满足性检验中起着核心作用。求解奇偶性博弈在计算上是昂贵的，除其他外，由于博弈的大小，对于模型检验问题，其可以容易地包含$10^9$顶点或更多。等价关系可以用来减少奇偶博弈的规模，从而潜在地减轻部分计算负担。我们重新考虑（治理）互模拟和（治理）口吃互模拟，我们给出了详细的证明，这些关系是等价的，有唯一的等价物，他们近似的获胜地区的奇偶游戏。此外，我们提出了基于游戏的这些关系的特征。使用这些特征，我们的等价关系的奇偶游戏，可以在文献中找到，如直接模拟等价和延迟模拟等价。为了完成概述，我们开发的直接和延迟模拟等价的共归纳特征，我们建立了一个等价的奇偶游戏格。
Deciding characteristic formulae: A journey in the branching-time spectrum
本文研究了在van Glabbeek分支时间谱中各逻辑中判定公式是否为特征公式的问题，分析了可满足性和素性问题的复杂性，并探讨了多项式时间与(co)NP或PSPACE完全问题之间的边界。
Model Checking Synchronized Products of Infinite Transition Systems
使用模型检验范式的形式化验证必须处理两个方面：系统模型是结构化的，通常是组件的产品，规范逻辑必须具有足够的表达能力，以允许可达性属性的形式化。本文研究了在这些前提下，无限转移系统可以得到什么样的结果。作为模型，我们考虑产品的无限过渡系统具有不同的同步约束。我们引入了可达同步变迁系统，即只包含可达（参数化）同步变迁的产品系统，并证明了产品系统的可达谓词扩展的一阶逻辑FO（R）的可判定性可归结为组件的FO（R）的可判定性.这个结果在以下意义上是最优的：（1）如果我们允许半有限同步，即仅在一个分量中有无穷多个转移是同步的，则乘积系统的FO（R）-理论一般是不可判定的。(2)我们不能扩展所考虑的逻辑的表达能力。已经有一个弱扩展的一阶逻辑与传递闭包，我们限制传递闭包运算符arity 1和嵌套深度2，是不可判定的异步（因此同步）产品，即无限网格。
Miter-Aware LUT Mapping: Aligning Structure and Solvability for Efficient Logic Equivalence Checking
研究逻辑等效性检查中因结构扰动等导致的问题，提出斜接感知映射框架，集成等效保留映射、高斯引导异或建模和面向求解器的查找表选择三种技术，可提升LEC效率，在数据集上有显著效果。
NP-Logic Systems and Model-Equivalence Reductions
本文研究了NP-逻辑系统之间模型等价约简的存在性，即NP中存在模型存在问题的逻辑系统。证明了在所有NP系统中，存在量化命题逻辑（\exists PF）对于多时间模型等价约简是最大的.然而，\exists PF似乎不是一个极大的NP-系统，因为存在一个具有模型检验问题D^P-完全的NP-系统。
Verifying LTL for Infinite State Systems via Termination Analysis
提出框架MoAT，将无限状态系统的LTL模型检验归约为公平终止问题，并利用终止分析工具KoAT和LoAT进行验证，实验表明与现有工具性能相当。
A Framework to Handle Linear Temporal Properties in (ω-)Regular Model Checking
自从几年前这个话题出现以来，关于定期模型检验的工作主要致力于状态可达性和安全性的验证。虽然人们知道，线性时间属性也可以在这个框架内检查，很少有人做了工作，以解决相应的细节。本文解决了这个问题的背景下，定期模型检验的基础上编码的状态由有限或无限的话。它工作的确切结构，在这两种情况下使用，并提出了一个部分解决方案的问题所产生的事实，无限计算的无界配置可能永远不会包含相同的配置两次，从而使循环检测的问题。
The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrum
本文研究了在 van Glabbeek 分支时间谱中，判定有限无环过程特征公式的复杂度，给出了可满足性与素性问题的复杂度结果，并探讨了多项式时间可解与计算困难的逻辑边界及公式构造的复杂度。
Compositional model checking of concurrent systems, with Petri nets
组合性和进程等价性都是进程代数的标准概念。复合性意味着一个复合系统的行为只依赖于其组成部分的行为，即没有涌现行为。过程等价意味着系统的显式状态空间让位于其交互模式：环境可以通过交互获得的信息。Petri网是一个经典的，但被广泛使用和理解的并发模型。然而，它们经常被描述为非组合模型，并且工具倾向于处理整体的、全局指定的模型。本教程论文集中在Petri网与边界（PNB）：1-安全网的合成，图形代数，以及其应用程序中的可达性检查工具彭罗斯。该算法的特点是使用组合性和进程等价，一个强大的组合，可以利用，以提高性能的检查可达性和覆盖性在几个常见的例子，其中Petri网模型现实的并发系统。
Parametric Interval Temporal Logic over Infinite Words
Halpern和Shoham的区间时序逻辑HS的模型检验最近已被系统地研究，它是已知的三个不同的语义下可判定。在这里，我们专注于基于轨迹的语义，其中给定（有限）Kripke结构的无限执行路径（轨迹）是主要的语义实体。在这种情况下，迹的每个有限中缀都被解释为一个区间，一个命题在区间上成立当且仅当它在每个分量状态上成立（齐性假设）。在本文中，我们介绍了一个量化的扩展HS的痕迹，称为参数HS（PHS）。新的逻辑允许表达的间隔的持续时间（长度）的参数定时约束。我们表明，检查存在的参数估值的Kripke结构满足PHS公式（模型检验），或PHS公式承认一个跟踪作为模型下的同质性假设（可满足性）是可判定的。此外，我们确定了PHS的一个片段，其中包括参数LTL和模型检验和满足性被证明是EXPSPACE完成。
Functional Reduction to Speed Up Bounded Model Checking
FRAIG-BMC通过功能简化减少冗余，提升边界模型检查的效率和性能。
Automatic Verification of Timed Concurrent Constraint Programs
时间并发约束（Timed Concurrent Constraint，tccp）是并发约束编程（Concurrent Constraint Programming，cc）范式的扩展，它允许我们指定时间至关重要的并发系统，例如反应式系统。可以有无限多个状态的系统可以在tccp中指定。模型检验是一种能够自动验证具有大量状态的有限状态系统的技术。在过去的几年里，一些研究已经调查了如何扩展模型检验技术的系统具有无限数量的状态。在本文中，我们提出了一种方法，利用tccp的计算模型。基于约束的计算允许我们定义一种方法，将模型检验算法应用于（一类）无限状态系统。我们扩展的经典算法的模型检验LTL的一个特定的逻辑定义的验证tccp和tccp结构，我们在这项工作中定义的建模程序的行为。我们定义了一个限制的时间，以得到一个有限的模型，然后我们开发了一些说明性的例子。据我们所知，这是第一个为tccp定义模型检验方法的方法。
A Constructive Equivalence between Computation Tree Logic and Failure Trace Testing
形式化验证的两个主要系统是模型检验和基于代数模型的测试。模型检验基于某种形式的时态逻辑，例如线性时态逻辑（LTL）或计算树逻辑（CTL）。CTL是一种强大而现实的逻辑，它能够表达进程的最有趣的属性，如活性和安全性。基于模型的测试基于进程的某些操作语义（例如跟踪、故障或两者）及其关联的前序。除了互模拟之外，最细粒度的前序（主要是理论上的重要性）是基于故障跟踪的。我们表明，这两个最强大的变种是等价的，也就是说，我们表明，对于任何故障跟踪测试存在一个CTL公式相当于它，反之亦然。我们所有的证明都是构造性的和算法性的。我们的结果允许一个大系统的部分被指定为逻辑，而其他部分被指定为代数，从而结合了最好的两个（逻辑和代数）的世界。
Regular Model Checking with Regular Relations
常规模型检验是一种用于无限状态系统的探索技术，其中状态空间表示为正则语言，并且转换关系使用无限（或有限）字符串上的有理关系来表示。我们扩展了常规的模型检验范例，允许使用更强大的过渡关系：类的正规关系，其中的理性关系是一个严格的子集。我们使用语言的一元二阶逻辑无限字符串来指定这样的关系，并采用流串换能器（SST）作为一个合适的计算模型。我们介绍了无限字符串的不确定性SST，并表明它们精确地捕捉MSO中定义的关系。我们进一步探讨了有效地进行定期模型检验所需的omega-NSST的理论属性。特别是，我们建立了定期的类型检查问题的omega-NSST是可判定的PSPACE。由于正则语言在正则关系下的后像可能不是正则的（甚至是上下文无关的），因此在这种设置下不能有效地执行迭代计算该后像的方法。相反，我们利用的事实，即定期的关系是封闭的组合，这与我们的可判定性的结果，定期模型检验与定期的关系提供了一个基础。
Counterexample Generation for Infinite-State Chemical Reaction Networks
反例生成是模型检验过程中不可缺少的一部分。在随机模型检验中，反例生成是一个具有挑战性的问题，因为它是不够的，找到一个单一的轨迹，违反了给定的性质。相反，一个潜在的大集合的痕迹有足够的概率违反的性质需要found.This本文考虑反例生成化学反应网络（CRN）模型与潜在的无限状态空间。提出了一种基于SMT求解的有界模型检验的CRN反例生成方法。它旨在找到给定模型的一小组违反属性的路径，使得它们共同具有高于给定阈值的总概率。一个独特的挑战是由于CRN的高度连接的状态空间，其中一个反例只是所有违反属性的路径的一个很小的子集。为了解决这些挑战，本文提出了一些优化，包括分而治之的技术，以扩大大型CRN模型的反例生成方法。本文报道了一些无限状态CRN模型的实验结果。
Trees over Infinite Structures and Path Logics with Synchronization
我们提供了无限树结构的模型检测问题的可判定性和不可判定性的结果。这些树结构由无限关系结构的元素序列构建。更准确地说，我们处理的关系结构M的树迭代在Shelah-Stupp的意义。与经典的MSO逻辑模型检验可判定的结果相反，我们证明了只允许路径量词和链量词的逻辑树模型检验问题的可判定性（其中链是路径的子集），因为它们出现在分支时间逻辑中;然而，同时树被等层关系丰富（如果顶点u、v在相同的树层上，则在顶点u、v之间保持）。我们将树逻辑与用于表达底层结构M的属性的逻辑干净地分离。我们说明的范围内的可判定性的结果表明，两个轻微的扩展框架导致不可判定性。特别地，这适用于Muchnik-Walukiewicz意义上的（更强的）树迭代。
Efficient Loop Conditions for Bounded Model Checking Hyperproperties
有界模型检验（BMC）是一种通过增量式地探索系统状态空间来发现缺陷的有效技术。为了通过有限的结构推理无限的轨迹并最终获得完整性，BMC结合了重新访问先前观察到的状态的循环条件。本文着重于开发循环条件BMC的HyperLTL-时间逻辑的hyperproperties，允许表达重要的政策，在并发系统的安全性和一致性，等等。循环条件HyperLTL比LTL更复杂，因为不同的轨迹可能会不一致地在不相关的时刻循环。HyperLTL的现有BMC方法仅考虑线性展开，而没有任何循环能力，这排除了找到小的无限迹线和获得完整的技术。我们调查循环条件HyperLTL BMC，其中HyperLTL公式可以包含多达一个量词交替。我们首先提出了一个一般的完全自动机为基础的技术，这是基于最大展开的界限。然后，我们引入替代的基于模拟的算法，允许有效地利用短循环，生成SAT查询，其满足性保证了原始模型检验问题的结果。我们还报告了使用Z3 py的BMC技术的原型实现的经验评估。
On (Omega-)Regular Model Checking
检查无限状态系统通常通过将无限状态集编码为正则语言来完成。计算这样一个规则的表示，比如说，一个系统的可达状态集需要加速技术，可以计算无限数量的转换的效果。在已经提出的加速技术中，可以找到特定的和通用的技术。特定技术利用被分析的特定类型的系统，例如，操纵队列或整数的系统，而通用技术仅假设转换关系由有限状态转换器表示，其必须迭代。在本文中，我们调查的可能性，使用通用技术的情况下，只有特定的技术已被利用到目前为止。发现现有的通用技术往往是不适用的情况下，很容易处理的特定技术，我们已经开发出一种新的方法来迭代换能器。这种新方法建立在早期工作的基础上，但利用了许多新的概念和算法思想，通常在实验的帮助下诱导，这使其具有广泛的范围以及良好的性能。
The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction
在模型检验中，偏序约简（POR）是一种减小状态空间大小的有效方法。顽固集是POR的一个已建立的变体，在过去的31年中有许多应用。顽固集的早期工作之一表明，几个条件的组合的减少是足以保持口吃的痕迹等价，使顽固集适合线性时间属性的模型检验。在本文中，我们确定了一个缺陷的推理和显示与一个反例，口吃迹等价不一定保留。我们提出了一个解决方案连同更新的正确性证明。此外，我们分析在哪些形式主义这个问题可能会发生。对实际实现的影响是有限的，因为它们都计算理论的正确近似。
Quasilinear Equivalence Checking for Detector Error Models
提出探测器错误模型（DEM）的等式理论，通过拟线性时间归约系统实现结构等价性判定，并应用于量子编译器验证与优化。
Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete
Sénizergues（1998，2005）证明了两个具有限制静默动作的下推自动机是否弱双相似。我们提供了第一个已知的复杂性上界这个著名的问题，在等效设置的一阶文法。这ACKERMANN上限是最佳的，我们还表明，强双相似性是连续递归的自动机的状态数是固定的。
Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems
本文解决了无限状态系统概率验证的长期开放问题，证明了针对无状态概率下推系统（pBPA）的概率计算树逻辑（PCTL）模型检测一般是不可判定的。
Fully Abstract Normal Form Bisimulation for Call-by-Value PCF
本文为传值调用 PCF 提出首个完全抽象的范式互模拟，通过融合应用式、环境互模拟与博弈语义的 LTS 实现程序等价检查，并开发有界工具验证了文献示例与新案例。
Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
REAL工具通过高效消除Ramsey量词，在LIRA中实现快速消除，应用于存活性检查和单子分解等程序验证问题。
Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2
我们提出了一种算法RTL设计的形式化验证方法，它结合了时序逻辑等价性检查和交互式定理证明。一个Verilog模块的中间模型是用Restricted Systemic C（RAC）手工编码的，RAC是一个C的原始子集，由Systemic C的整数和定点寄存器类模板扩充。该模型被设计为尽可能的抽象和紧凑，但足够忠实的RTL允许有效的等价性检查与商业工具。然后，它会自动转换为ACL 2的逻辑，从而能够根据正式的体系结构规范对正确性进行机械检查。在本文中，我们描述了RAC语言，翻译过程，以及一些技术，方便正式分析所产生的ACL2代码。
A Metric Encoding for Bounded Model Checking (extended version)
在有界模型检验中，系统模型和被检验的属性都被转换成一个布尔公式，由SAT求解器进行分析。我们介绍了一种新的编码技术，这是特别优化的管理定量未来和过去的度量时间运营商，通常发现在硬实时的系统的属性。编码是简单和直观的原则上，但它是更复杂的存在下，典型的有界模型检验技术，向后和向前的循环用于表示一个最终的周期性无限域的有限结构。我们报告和评论的新的编码技术，并进行了广泛的实验，以评估其可行性和有效性。
Model Checking CSL for Markov Population Models
针对无限状态连续时间马尔可夫链的马尔可夫种群模型，提出了一种完整的连续随机逻辑（CSL）模型检验算法，能够有效验证概率可达性、生存性、振荡等生物系统关键性质。
Tree Regular Model Checking for Lattice-Based Automata
树规则模型检验（TRMC）是分析无限状态系统的一系列技术的名称，其中状态由项表示，状态集由树自动机（TA）表示。TRMC的核心问题是判断一组坏状态是否可达。计算表示可达状态集合（的过近似）的TA的问题是不可判定的，但是存在基于树换能器的完成或迭代的有效解决方案。不幸的是，TRMC框架无法有效地捕获系统的复杂结构及其某些功能。作为示例，对于JAVA程序，项的结构主要用于捕获系统的状态的结构。相反，Java程序的整数必须用Peano数编码，这意味着任何代数运算都可能由数千个重写规则的应用程序表示。在本文中，我们提出了格树自动机（LTA），树自动机的扩展版本，其叶子配备了格。LTA允许我们表示可能无限的解释术语集。这些术语能够以有效的方式表示复杂的域和相关操作。我们还将经典的布尔运算扩展到LTA。最后，作为一个主要的贡献，我们引入了一个新的基于完成的算法计算可能无限的可达解释条款在有限的时间。
Weakly acyclic diagrams: A data structure for infinite-state symbolic verification
针对OBDDs无法处理无限状态系统的局限，提出弱无环图（WADs）这一OBDDs泛化结构，保留其算法优势并支持无限语言表示，可用于多种无限状态系统的符号模型检测。
Model-checking parametric lock-sharing systems against regular constraints
本文研究参数化锁共享系统在强公平性下的无限行为验证问题，证明其在嵌套锁使用下可判定且为 Exptime 完全，并在 spawn 参数有界时对固定秩奇偶自动机性质给出 Ptime 算法。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。