Technical Report: Model-Checking for Resource-Bounded ATL with Production and Consumption of Resources
文献中已经提出并研究了几种表示资源约束下联盟能力的逻辑。已有的工作表明，如果只考虑资源的消耗，或者系统中任意路径上产生或消耗的资源总量是有界的，那么几种标准逻辑（如资源有界联合逻辑（RB-CL）和资源有界交替时序逻辑（RB-ATL））的模型检验问题是可判定的.然而，对于具有无限资源生产和消费的联盟逻辑，只知道一些不可判定性结果。本文证明了资源无限生产和无限消耗的RB-ATL的模型检验问题是可判定的，但是EXPSPACE困难的.我们还调查了一些易于处理的情况下，并提供了一个详细的比较，资源逻辑RAL的一个变种，连同新的复杂性结果。
2015-04-25 cs.LO cs.MA
PEQcheck: Localized and Context-aware Checking of Functional Equivalence (Technical Report)
重构不得改变程序的功能。然而，并不是所有的重构都满足这个要求。因此，必须明确检查重构不会改变功能。由于很少有一个正式的规格说明程序的行为，我们利用原来的程序作为功能规范。然后，我们检查原始程序和重构后的程序在功能上是否等价。为此，我们采用一个共同的想法，减少等价性检查程序验证。为了提高效率，我们的等价性检查PEQcheck构造一个验证任务，每个重构的代码段，而不是一个功能，通常由以前的工作。此外，PEQcheck考虑代码段的上下文。例如，只有被修改的和活的变量才需要是等效的，只读变量可以在原始代码段和重构的代码段之间共享。此外，我们的评估证明，本地化和上下文感知检查执行的\peqcheck确实可以是有益的。
2021-03-22 cs.LO cs.PL
Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems (technical report)
我们提出了一个通用的框架，建模和验证的认识属性参数化的多智能体系统，通过真实的公告进行通信。在我们的框架中，代理的数量或某些资源的数量被参数化（即先验未知），相应的验证问题询问给定的认知属性是否为真，而不管参数的实例化。例如，在一个泥泞的儿童拼图中，人们可以问每个孩子是否最终都会发现他是否泥泞，而不管孩子的数量。我们的框架是定期模型检验（RMC）为基础的，其中同步有限状态自动机（相当于一元二阶逻辑的话）被用来指定系统。我们提出了一个公共声明逻辑的扩展作为规约语言。特别感兴趣的是增加了所谓的迭代公共公告运营商，这是至关重要的推理知识参数化系统。虽然运营商的模型检验问题不可判定的，我们表明，这成为一个适当的“消失关系”时，可判定的。此外，我们展示了如何Angluin的L* 算法学习有限自动机可以应用到找到一个消失的关系，这是保证终止，如果它是正规的。我们已经实现了该算法，并将其应用于这样的例子，如泥泞的儿童拼图，俄罗斯卡问题，大数挑战。
2021-03-08 cs.FL cs.LO cs.MA
Formal Verification of Safety Properties Using Interpolation and k-induction
本技术报告介绍了使用SAT/SMT求解器的两种符号模型检验算法的实现，即基于插值的模型检验和基于k-归纳的模型检验。并对这两种模型检验算法进行了比较分析。
2022-07-04 cs.LO
Efficient Implementation of Rewriting Revisited Technical Report
最近，已经引入了许多技术，允许（自动化）的术语重写系统（TRS）的运行时复杂性的分类。在早期的工作中，作者已经表明，对于合流TRS，最内层多项式运行时复杂性导致定义的函数的多时间可计算性。本文将上述结果推广到完全重写。根据我们以前的工作，我们利用图重写。我们给出了一个新的证明充分重写，允许一个精确的控制复制的资源图重写。总之，我们完整地描述了重写的图灵机（简称TM）上的实现。我们表明，TRS的运行时复杂性和TM的运行时复杂性是多项式相关的。我们的结果加强了重写系统的复杂性是真实地表示通过推导的长度的证据。此外，我们的结果允许分类的非确定性多时间计算的基础上的重写系统的运行时复杂性分析。
2011-06-08 cs.CC cs.LO
HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
HornStr 是首个将正则模型检验的不变式合成转化为字符串上的约束 Horn 子句问题的求解器，支持 L* 和基于 SAT 的自动机学习，并自动验证 MU 谜题，生成超 30000 个新基准。
2025-05-23 cs.FL cs.LO
Technical Report: Exploring Automatic Model-Checking of the Ethereum specification
本研究针对以太坊3SF共识协议的可问责安全性，基于其Python规范用TLA+形式化并结合多层手动抽象，通过Apalache等工具实现小规模实例的穷举验证，未发现安全违规，证明了手动抽象对模型检测效率的提升作用。
2025-01-16 cs.DC cs.LO
Model Checking Resource Bounded Systems with Shared Resources via Alternating Büchi Pushdown Systems
资源受限的多智能体系统的验证一般是不可判定的。在许多这样的设置中，资源对于代理是私有的。本文研究了基于交替时序逻辑（ATL）的资源逻辑在共享资源下的模型检验问题。资源可以被消耗和生产到任何数量。我们表明，模型检验问题是不可判定的，如果两个或两个以上的这样的无界资源。我们的主要技术成果是，在一个单一的共享资源的情况下，问题变得可判定。虽然直观，可判定性的证明是不平凡的。我们减少模型检验的问题交替Büchi下推系统。一个中间结果连接到一般的基于自动机的验证：我们表明，模型检验计算树逻辑（CTL）（紧凑）交替Büchi下推系统是可判定的。
2015-08-14 cs.LO
Modular Mix-and-Match Complementation of Büchi Automata (Technical Report)
不确定Büchi自动机（BA）的可补性是自动机理论中的一个重要问题，在形式化验证中有着广泛的应用，如程序的终止性分析、模型检验以及某些逻辑的判定过程等。我们建立在最近的工作的想法BA确定李等。并提出了一个新的模块化算法BA互补。我们的算法允许结合几个BA互补程序在一起，一个程序的一个子集的BA的强连接组件（SCC）。以这种方式，可以利用特定SCC的结构（例如当它们固有地弱或确定性时）并使用更有效的专用算法，而不管整个BA的结构如何。我们给出了一个一般的框架，部分互补程序可以插入，它的实例化与几个算法。一般来说，该框架可以产生具有Emerson-Lei接受条件的补集，该补集通常可以更紧凑。使用该算法，我们能够建立一个指数更好的新的上限$O(4n)$补充最近推出的电梯自动机类。我们实现了该算法的原型，并进行了一系列全面的实验上的一个大的基准测试，表明我们的框架补充以及最先进的，它可以作为未来的高效BA互补和包含检查算法的基础。
2023-01-05 cs.FL cs.LO
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)
我们考虑的问题，自动验证一个参数化的概率并发系统的家庭终止的概率为1的所有实例对抗对抗的竞争对手。一个参数化的族定义了一个无限状态系统：对于每个数n，这个族由一个实例和n个有限状态进程组成。与安全性相比，活性的参数化验证目前仍然被认为是极具挑战性的，特别是在模型中存在概率的情况下。一个主要的挑战是提供一个足够强大的象征性框架。一个著名的符号框架的参数化验证的非概率并发系统是定期模型检验。虽然该框架最近扩展到概率系统，将公平性的框架-通常是至关重要的验证终止-一直特别困难，由于存在无限数量的公平性约束（每个过程一个）。我们的主要贡献是一个系统的，正则保持，编码有限的公平性（一个现实的公平性的概念，提出了由Henzinger）定期模型检验的概率参数化系统的框架。我们的编码减少了终止有限的公平性，以验证参数化的终止没有公平性的概率系统在定期模型检验（验证框架已经存在）。我们表明，我们的算法可以验证终止许多有趣的例子，从分布式算法（赫尔曼的协议）和进化生物学（莫兰过程，细胞周期开关），这并不符合标准的公平概念。据我们所知，我们的算法是第一个全自动的方法，可以证明这些例子的终止。
2017-10-30 cs.DC cs.FL cs.LO
VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report)
本技术报告包含与我们在ASPLOS'21上发表的相同标题的工作相关的材料。我们从第二节开始。本文详细介绍了本文的核心创新点Await模型检验（AMC）。AMC的正确性证明可以在Sec. 2.接下来，我们将讨论SEC中的三个研究案例。3、介绍在现有代码库中应用VSync时发现的错误和遇到的挑战。最后，在第4我们描述了我们评估的设置细节，并报告了进一步的实验结果。
2021-02-12 cs.LO
Parameterized Verification of Quantum Circuits (Technical Report)
Uppsala University（乌普萨拉大学）；Mälardalen University（马拉尔登大学）；Brno University of Technology（布尔诺理工大学）；Aalborg University（奥尔堡大学）；National Taipei University of Technology（台北科技大学）
本文提出了一种自动框架用于验证参数化量子电路的输入输出正确性与等价性，采用同步加权树自动机模型并提供决策算法，通过实验展示了框架的高效性与表达力。
2025-12-02 cs.FL cs.LO
Simple Strategies in Multi-Objective MDPs (Technical Report)
RWTH Aachen University（亚琛工业大学）；UMONS – Université de Mons（蒙斯大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
我们考虑在马尔可夫决策过程（MDP）上同时验证多个期望奖励目标。这使得能够通过获得帕累托前沿在多个目标之间进行权衡分析。我们专注于易于使用和实施的战略。也就是说，策略是纯的（没有随机化），并且具有有限的记忆。我们表明，检查一个点是否可以实现一个纯静态策略是NP完全的，即使是两个目标，我们提供了一个MILP编码来解决相应的问题。有界记忆情形可以通过乘积构造化为平稳情形。使用\Storm和Guidelines的实验结果表明了我们的算法的可行性。
2020-02-17 cs.AI cs.LO
Complementing Emerson-Lei Elevator Automata (Technical Report)
Brno University of Technology（布尔诺理工大学）；Key Laboratory of System Software (Chinese Academy of Sciences), ISCAS（中国科学院系统软件重点实验室）；Slovak University of Technology in Bratislava（布拉迪斯拉发斯洛伐克工业大学）
本文提出 Emerson-Lei 电梯自动机，推广了 Büchi 电梯自动机到更丰富的接受条件，并给出一种补全算法，其渐近复杂度显著优于已知最佳算法，实验表明比 Spot 工具更高效。
2026-06-26 cs.FL cs.LO
Reducing CMSO Model Checking to Highly Connected Graphs
给定计数一元二阶（CMSO）语句$ψ$，CMSO $[ψ]$问题定义如下。CMSO $[ψ]$的输入是图形$G$，目标是确定是否存在$G\models ψ$。我们的主要定理指出，对于每一个CMSO语句$ψ$，如果CMSO $[ψ]$在“全局高度连通图”上的多项式时间内可解，那么CMSO $[ψ]$在多项式时间内（在一般图上）可解。我们证明了我们的定理在参数化算法的设计中的效用。具体来说，我们表明，技术问题的具体成分的一个强大的方法，设计参数化算法，递归的理解，可以取代我们的主要定理的黑盒调用。我们还表明，我们的定理可以很容易地部署到显示固定的参数化的易处理性的广泛的问题，其中输入是一个图形$G$和任务是找到一个连接的诱导子图的$G$，使“几个”顶点在这个子图有邻居以外的子图，此外，子图具有CMSO定义的属性。
2018-02-05 cs.CC cs.DS cs.LO
Efficient Query Answering over Conceptual Schemas of Relational Databases : Technical Report
我们开发了一个查询应答系统，在工作的核心是一个想法的查询应答重写。为此，我们扩展了DL DL-Lite的能力，以支持n元关系，获得DL DLR-Lite，这仍然是多项式的数据的大小。我们设计了一种灵活的方式映射的概念级的关系级，它提供了一个类似SQL的查询语言查询语言的概念模式的用户。重写技术增加了传统查询应答技术的价值，允许制定更简单的查询，具有推断用户查询中未明确说明的附加信息的能力。概念模式的形式化和开发的推理技术允许检查数据库和概念模式之间的一致性，从而提高了信息系统的可信度。
2009-02-11 cs.DB cs.LO
Automated Mapping of UML Activity Diagrams to Formal Specifications for Supporting Containment Checking
业务分析师和领域专家经常使用与技术和平台无关的高级模型来勾画软件系统的行为。开发人员将用技术细节来完善和丰富这些高级模型。因此，随着时间的推移，细化的模型可能会偏离原始模型，特别是当两种模型独立演化时。在这种情况下，我们专注于行为模型;也就是说，我们的目标是确保细化的低级别行为模型符合相应的高级别行为模型。基于现有的形式化验证技术，我们提出包含检查作为一种手段，以评估系统的行为所描述的低级别模型是否满足已指定的高级别同行。主要障碍之一是如何减轻创建行为模型的正式规范以及一致性约束的负担，这是一项手动完成的繁琐且容易出错的任务。本文提出的方法旨在通过将行为模型视为验证输入，并将行为模型自动映射到可直接由模型检查器使用的形式属性和描述上，来缓解上述挑战。我们讨论了我们的方法中的各种挑战，并展示了我们的方法在说明性场景中的适用性。
2014-04-03 cs.LO cs.SE
Bounded Quantifier Instantiation for Checking Inductive Invariants
本文提出有界视界量词实例化方法，限制实例化项深度以保证SMT求解器终止，能有效检查归纳不变量，且界限1时可自动模拟插桩，无需修改代码。
2019-08-20 cs.LO cs.PL
A Uniform Framework for Handling Position Constraints in String Solving (Technical Report)
本文提出一个统一框架，通过将位置字符串约束归约为基于特殊有限自动机 Parikh 映像的整数冲突检查，避免词方程编码，使求解复杂度降至 NP 完全甚至 PTime，并在 Z3-Noodler 中显著提升性能，同时可扩展处理部分 not-contains 问题。
2025-04-10 cs.FL cs.LO
Monadic Decomposition in Integer Linear Arithmetic (Technical Report)
一元可分解性是变量独立性的概念，它询问一阶理论中的给定公式是否可以表示为理论中一元谓词的布尔组合。最近，Veanes等人在SMT的上下文中展示了一元可分解性的有用性（即输入公式是无量词的），并发现了各种有趣的应用，包括字符串分析。然而，检查一元可分解性通常是不可判定的。某些理论的可判定性是已知的（例如，Presburger算术，Tarski的实闭域），但关于它们的计算复杂性的结果很少。本文研究了整数线性算术在SMT下的一元可分解性。我们表明，这个决策问题是CONP-完全的，当monadically可分解，一个公式承认在最坏的情况下分解的指数大小。我们提供了一个新的应用程序，我们的结果字符串约束求解长度约束。然后，我们扩展我们的结果变元分解，谓词可以承认多个自由变量（相对于一元分解）。最后，我们给出了整数线性算术中的量词消去的一个应用，其中量词块中的变量，如果是独立的，可以用指数（而不是标准的双指数）爆破消除。
2020-04-26 cs.LO
Regular Symmetry Patterns (Technical Report)
对称性约简是一种用于缓解模型检验中状态爆炸问题的方法。然而，在并发系统中自动识别对称性在计算上是昂贵的。我们提出了一个符号框架，用于捕获参数化系统（即有限状态系统的无限家族）中的对称模式：两个正则字转换器分别代表参数化系统和对称模式。该框架包含了各种类型的对称关系，从较弱的概念（例如模拟前序）到最强的概念（即同构）。我们的框架具有两个算法特性：（1）对称性验证：给定换能器，我们可以自动检查它是否是给定系统的对称模式，以及（2）对称性合成：我们可以自动生成换能器形式的给定系统的对称模式。此外，我们的符号语言允许额外的约束，对称模式需要满足容易地纳入验证/合成。我们展示了这些属性如何帮助识别对称模式的例子，如用餐哲学家协议，自稳定协议，优先资源分配协议。在某些情况下（例如，格里斯的咖啡可以问题），我们的技术自动合成一个安全保护有限近似，然后可以验证安全性仅使用有限状态模型检查器。
2015-10-28 cs.LO
Generalised Multiparty Session Types with Crash-Stop Failures (Technical Report)
会话类型支持通信系统的规范和验证。然而，他们的理论通常假设过程永远不会失败。为了解决这个问题，我们提出了一个广义多方会话类型（MPST）理论与崩溃停止故障，其中进程可以崩溃任意。我们的新理论验证了更多的协议和过程w.r.t.以前的工作。我们将最小的语法变化应用于标准会话π-演算和类型：我们对崩溃及其处理进行语义建模，并在行为安全属性上使用广义MPST类型系统参数。我们涵盖了完全可靠和完全不可靠的会话之间的频谱，通过可选的可靠性假设，并证明了类型安全性和协议一致性的崩溃停止故障的存在。引入崩溃停止失败会产生重要的后果：编写处理所有崩溃场景的正确进程可能很困难。然而，我们的广义MPST理论允许我们驯服这种复杂性，通过模型检验，以验证多方会话是否满足所需的行为属性，例如死锁自由或活性，即使在崩溃的存在。我们使用mCRL 2模型检查器实现我们的方法，并从文献中扩展的例子进行评估。
2023-02-21 cs.LO cs.PL
Automatic Program Instrumentation for Automatic Verification (Extended Technical Report)
本文提出将程序插桩作为统一验证范式，以自动变换方式消除规约语言中后端求解器难以处理的结构，并将数组聚合形式化为幺半群同态，在 MonoCera 工具中实现并验证其有效性。
2023-05-26 cs.LO cs.SE
On the Complexity of Verification of Time-Sensitive Distributed Systems: Technical Report
针对时间敏感分布式系统（TSDS）的描述和分析，提出了一种具有显式时间的多集重写语言。目标通常使用明确的时间限制来指定。一个好的跟踪是一个无限的跟踪，其中的目标是永远满足，尽管可能的干扰，从环境。在我们之前的工作（FORMATS 2016）中，我们讨论了TSDS的两个理想属性，可实现性（存在良好的迹）和生存性（此外，所有可接受的迹都是好的）。在这里，我们考虑两个额外的属性，可恢复性（所有兼容的跟踪都不会到达不归点）和可靠性（系统总是可以使用良好的跟踪继续运行）。继（FORMATS 2016）之后，我们重点关注一类称为递进计时系统（PTS）的系统，直观地说，在有限的时间段内只能执行有限数量的操作。我们证明了这类系统的可恢复性和可靠性的性质相吻合，是PSPACE-完全的。此外，如果我们施加一个约束的时间（在有界模型检查），我们表明，PTS的可靠性属性是在$Π_2^p$类的多项式层次结构，一个子类的PSPACE。我们还证明了有界生存性是NP-困难和coNP-困难的。
2021-09-14 cs.CC cs.LO
Decision Procedures for Sequence Theories (Technical Report)
本文研究序列理论的可判定性，证明基于布尔代数字母表和参数自动机可保持可判定性，并开发了序列求解器 SeCo 以验证其有效性。
2023-07-31 cs.LO
String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report)
字符串分析是推理程序如何操作字符串的问题。它有许多应用程序，包括自动检测跨站点脚本（XSS）。流行的字符串分析技术包括符号执行，其核心使用字符串（约束）求解器。这样的求解器通常会推理以字符串理论表达的约束，并将连接运算符作为原子约束。近年来，研究人员开始认识到在串接弦理论中引入替换所有算子和有限转换的重要性。这样的字符串操作通常对于Web应用程序中的XSS漏洞推理至关重要，特别是对消毒功能和隐式浏览器转换（例如innerHTML）进行建模。在本文中，我们提供了第一个字符串求解器，可以原因涉及连接和有限转换的约束。此外，它对几个重要的片段（例如直线片段）具有完整性和终止性保证。在本文中解决的主要挑战是禁止最坏情况下的理论的复杂性。为此，我们提出了一种方法，利用简洁的交替有限自动机作为字符串约束的简洁符号表示。交替不仅在表示换能器的布尔组合时提供了空间上的指数节省，而且还提供了简洁表示换能器和级联的否则昂贵的组合的可能性。关于AFA语言的空性的推理需要在指数大小的图中进行状态空间探索，为此我们使用模型检验算法（例如IC3）。我们已经实现了我们的算法，并证明了它的效力，来自XSS和文献中的其他例子的基准。
2020-10-29 cs.LO
