基于图的MSO分布式模型检验

动态数据库驱动系统的近期有界验证（扩展版）

Recency-Bounded Verification of Dynamic Database-Driven Systems (Extended Version)

我们提出了一个形式主义模型数据库驱动的系统，称为数据库操作系统（DMS）。DMS的操作通过向数据库中添加新元素、从关系中删除元组以及向关系中添加元组来修改关系数据库的当前实例。由动作修改的元素由（完整的）一阶查询选择。DMS是一个高度表达的模型，可以被认为是一个简洁的表示一个无限状态的关系转换系统，在文献中提出的类似的模型。我们提出了一元二阶逻辑（MSO-FO）的原因出现沿运行的数据库实例的序列。不出所料，DMS对MSO-FO的线性时间模型检验问题是不可判定的。针对可判定性，提出了DMS的欠近似模型检验，其中欠近似参数为“新近界”。在$k$ -最近-有界运行中，只有当前活动域中最近的$k$元素可以被操作修改。可以通过增加新近度的界限来验证更多的运行。我们的主要结果表明，最近有界的模型检验的DMS对MSO-FO是可判定的，通过减少的可满足性问题的MSO嵌套的话。

递归方案、MSO逻辑与U量词

Recursion Schemes, the MSO Logic, and the U quantifier

本文证明了对递归方案生成的树，在MSO逻辑基础上增加受限的U量词（表示对任意大有限集为真）后，模型检验问题仍可判定，且该逻辑具有反射性和有效选择性质。

定高树的MSO性质的核化及其结果

Kernelizing MSO Properties of Trees of Fixed Height, and Some Consequences

固定一个整数h>=1。在宇宙中的彩色树的高度最多h，我们证明，任何图的决策问题所定义的MSO公式与r量词，存在一组内核，每个大小由一个初等函数的r和颜色的数量。这产生了两个值得注意的结果。考虑在高度为h的着色树的宇宙中具有一维MSO解释的任何图类G（等价地，G是灌木深度为h的一类）。首先，类G承认一个MSO模型检验算法，其运行时间有一个基本的公式大小的依赖。其次，在G上，FO和MSO的表达能力一致（这扩展了Elberfeld，Grohe和Tantau在2012年的结果）。

Local certification of MSO properties for bounded treedepth graphs

The graph model checking problem consists in testing whether an input graph satisfies a given logical formula. In this paper, we study this problem in a distributed setting, namely local certification. The goal is to assign labels to the nodes of a network to certify that some given property is satisfied, in such a way that the labels can be checked locally. We first investigate which properties can be locally certified with small certificates. Not surprisingly, this is almost never the case, except for not very expressive logic fragments. Following the steps of Courcelle-Grohe, we then look f…

一元二阶逻辑复杂度的下界

Lower Bounds for the Complexity of Monadic Second-Order Logic

Courcelle在1990年提出的著名定理指出，在一元二阶逻辑（MSO）中可定义的图的任何性质都可以在线性时间内在任何一类有界树宽的图上确定，或者换句话说，MSO在线性时间内在任何此类图上都是固定参数易处理的。从逻辑的角度来看，Courcelle定理为MSO-模型检验的易处理性建立了一个充分条件或上界。而这样的逻辑复杂性的上限已经在文献中得到了极大的关注，几乎没有什么是已知的相应的下限。本文建立了一元二阶逻辑复杂度的一个强下界。特别是，我们表明，如果C是任何一类图，这是封闭的下采取子图，其树宽是不是有界的多对数函数（事实上，$\log^c n$为一些小c足够），然后MSO-模型检验是棘手的C（在一个适当的假设下，从复杂性理论）。

低秩MSO

Low rank MSO

该研究引入低秩MSO这一图性质描述新逻辑，证明其在弱稀疏图类、有界VC维图类及所有图上分别与分隔符逻辑、翻转连通性逻辑、翻转可达性逻辑表达能力等价，并指出无向图中其可表达性质可多项式时间判定。

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

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

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

图神经网络与MSO

Graph neural networks and MSO

本文通过构造可捕获树上MSO可定义节点性质的分布式自动机，重新证明实数循环图神经网络与分级模态替换演算在MSO限制下表达能力等价，并讨论接受条件变体。

关于一元二阶逻辑的参数化难解性

On the Parameterised Intractability of Monadic Second-Order Logic

Courcelle的一个著名的结果指出，如果C是一类有界树宽的图，则一元二阶逻辑的模型检验是C上的固定参数线性时间参数化算法。一个直接的问题是，这是否是最好的，或者结果是否可以扩展到无限树宽的类。在本文中，我们表明，在树的宽度，定理不能进一步推广。更具体地说，我们证明了，如果C是一类图，这是封闭的着色，并满足一定的构造性条件，使得C的树宽度是不是有界的log^{16}（n），那么MSO_2-模型检验是不是固定参数易处理的，除非满足性问题SAT命题逻辑可以解决在次指数时间。如果C的树宽不是多项式有界的，那么MSO_2-模型检验不是固定参数的易处理的，除非多项式时间层次中的所有问题，因此特别是NP中的所有问题，可以在次指数时间内解决。

分布式知道如何的模型检测问题是 $\Delta^p_2$-完全的

The Model Checking Problem for Distributed Knowing How is $Δ^p_2$-Complete

研究了分布式知道如何的模型检测问题的复杂性，证明该问题是 $\Delta^p_2$-完全的。

超越MSO的简化算法元定理：树宽与邻域多样性

Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity

本文研究了MSO逻辑扩展在树宽和邻域多样性图上的计算复杂性，提出多项式时间算法并展示了通过CSP形式化的新方法。

云中的分布式CTL模型检验

Distributed CTL Model Checking in the Cloud

最近广泛使用的“大数据”平台要求形式化验证社区更广泛地采用。事实上，形式化验证需要高性能的数据处理软件，用于从来自被分析系统的空前数量的数据中提取知识。由于基于云的计算资源已经变得易于访问，因此验证技术和工具有机会经历深刻的技术转型，以利用新的可用架构。这使得人们对并行化和分布式验证技术越来越感兴趣。在本文中，我们介绍了一种分布式的方法，利用通常使用的技术，由“大数据”社区，使验证的计算树逻辑（CTL）公式非常大的状态空间，使用分布式系统和云计算设施。基准规范上进行的几个测试的结果，从而显示所提出的方法的方便。

拜占庭失效原子提交协议的认知模型检验

Epistemic Model Checking of Atomic Commitment Protocols with Byzantine Failures

Halpern和Fagin提出的基于知识的程序的概念为设计、分析和优化分布式系统提供了一种有用的形式主义。本文将两阶段提交协议描述为一个基于知识的程序，然后通过模型检验和反例引导精化的迭代过程，找到了在拜占庭故障背景下具有同步可靠通信的完美召回语义的程序的具体实现。我们模拟了几种不同类型的拜占庭故障，并验证了不同的策略来对抗和减轻它们。我们解决了一些在以前的文献中没有考虑过的问题，即，在什么情况下发送者可以知道它的传输已经成功，以及在什么情况下代理可以知道协调者正在欺骗，并且找到这些问题的具体答案。本文还介绍了一种基于时间-认知模型检验技术的方法，该方法可以用来验证分布式协议的最短和最长执行时间以及导致它们的场景。

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling

We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph: a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification prob…

无限结构上的树与同步路径逻辑

Trees over Infinite Structures and Path Logics with Synchronization

我们提供了无限树结构的模型检测问题的可判定性和不可判定性的结果。这些树结构由无限关系结构的元素序列构建。更准确地说，我们处理的关系结构M的树迭代在Shelah-Stupp的意义。与经典的MSO逻辑模型检验可判定的结果相反，我们证明了只允许路径量词和链量词的逻辑树模型检验问题的可判定性（其中链是路径的子集），因为它们出现在分支时间逻辑中;然而，同时树被等层关系丰富（如果顶点u、v在相同的树层上，则在顶点u、v之间保持）。我们将树逻辑与用于表达底层结构M的属性的逻辑干净地分离。我们说明的范围内的可判定性的结果表明，两个轻微的扩展框架导致不可判定性。特别地，这适用于Muchnik-Walukiewicz意义上的（更强的）树迭代。

A small-step approach to multi-trace checking against interactions

Interaction models describe the exchange of messages between the different components of distributed systems. We have previously defined a small-step operational semantics for interaction models. The paper extends this work by presenting an approach for checking the validity of multi-traces against interaction models. A multi-trace is a collection of traces (sequences of emissions and receptions), each representing a local view of the same global execution of the distributed system. We have formally proven our approach, studied its complexity, and implemented it in a prototype tool. Finally, w…

同步属性的计算树逻辑

Computation Tree Logic for Synchronization Properties

我们提出了一个逻辑，扩展CTL（计算树逻辑）与运营商表示同步属性。如果一个属性在所有具有一定长度的路径中都成立，则该属性在系统中是同步的。新的逻辑是通过使用与CTL相同的路径量词和时态运算符来获得的，但允许量词的顺序不同。这个小的语法变化导致一个逻辑，可以表达非正规的属性，其中已知的扩展MSO路径长度相等是不可判定的。我们证明了我们的变体CTL是可判定的，模型检测问题是在Delta_3 ^P = P ^{NP ^NP}中，并且是DP-困难的。我们类似地考虑量词交换CTL的扩展，我们提出的运营商定义使用的基本运营商的CTL * 表示发生无限多个同步点。证明了模型检验问题仍然存在于Delta_3 ^P中，如果允许Next算子，则CTL和新逻辑的区分能力一致，从而可以在模型检验之前使用经典的互模拟商进行状态空间约简。

具有知识、不完全信息、完全回忆和通信联盟的交替时序逻辑的模型检验

Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions

我们提出了一个变体的ATL与分布式知识运营商的基础上同步和完善的召回语义。这种逻辑中的联盟模式是基于对完整历史的部分观察，并结合了联盟成员之间的合作形式，其中代理基于该联盟的系统历史的分布式知识发布其行动。我们表明，模型检验是可判定的这种逻辑。该技术利用两个变种的游戏与不完美的信息和部分可观察的目标，以及一个子集的建设，用于识别状态的历史是无法区分的考虑联盟。

Spin中的模型检验Paxos

Model Checking Paxos in Spin

我们提出了一个正式的分布式共识算法模型，在可执行的规约语言Promela扩展了一种新类型的警卫，称为计数警卫，需要实现过渡，依赖于多数表决。我们的形式化利用的抽象，从减少定理适用于特定的案例研究。我们应用模型检查自旋自动验证模型的有限实例，并提取的协议的选举阶段中使用的法定人数的大小的先决条件。

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

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

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

惰性有界声明式分布式系统的有时终止性验证

Verification of Sometimes Termination of Lazy-Bounded Declarative Distributed Systems

针对通常不可判定的 DDS 模型检测问题，本文通过调整数据源边界、消息表达能力与通道类型，识别出有时终止性验证的可判定情形。

算法元定理的进展

Advances in Algorithmic Meta Theorems

本文综述了算法元定理的最新进展，重点介绍FO在遗传图类上的模型检测突破、单子稳定与单子依赖图类的组合结构理论、twinwidth宽度度量，以及介于FO与CMSO之间的新逻辑对无关顶点技术和递归理解等方法提供的统一视角。

Tarmo：一个简化的有界模型检验框架

Tarmo: A Framework for Parallelized Bounded Model Checking

本文研究了共享内存环境和工作站集群环境下的有界模型检验（BMC）并行化方法。我们提出了一个通用的框架，并行BMC命名为Tarmo。我们的框架可以与BMC的任何增量SAT编码一起使用，但对于本文中的结果，我们仅使用当前最先进的完整PLTL编码。使用这种编码允许我们检查安全性和活性属性，这与早期分发BMC时仅限于安全属性的工作相反。尽管我们的重点是BMC后，它已被翻译成SAT，现有的分布式SAT求解器并不适合我们的应用程序。这是因为解决BMC问题不是解决一组独立的SAT实例，而是解决多个相关的SAT实例，增量编码，其中每个实例的可满足性对应于特定长度的反例的存在。我们的框架包括一个通用的共享子句数据库的架构，允许SAT求解线程之间轻松共享子句解决各种这样的实例。我们提出了广泛的实验结果与我们的Tarmo实现的多个变体。我们的共享内存变体比传统的单线程方法具有更好的性能，这是许多用户可以受益于多核和多处理器技术的广泛应用的结果。此外，我们证明了我们的框架可以部署在一个典型的工作站集群，其中几个多核机器通过网络连接。

教程：使用mCRL2设计分布式软件

Tutorial: Designing Distributed Software in mCRL2

本教程介绍使用mCRL2语言和工具集，通过模型检查创建并行软件行为模型、用模态公式指定需求并验证，以发现罕见错误并指导互斥协议设计。

多媒体系统的随机模型检测

Stochastic Model Checking for Multimedia

现代分布式系统包括一类非功能性需求很重要的应用程序。特别是，这些应用程序包括多媒体设施，实时约束是至关重要的，他们的正确运作。为了指定这样的系统，它是必要的，以描述事件发生的概率分布和随机自动机已成为一个有用的技术，通过它可以指定和验证这样的系统。然而，随机描述是非常一般的，特别是它们允许使用一般的概率分布函数，因此它们的验证可能是复杂的。在过去的几年里，模型检测已经成为一个有用的验证工具，大型系统。在本文中，我们描述了两个随机自动机的模型检测算法。这些算法考虑如何写在一个简单的概率实时逻辑的属性可以检查一个给定的随机自动机。

分布式航空电子系统可扩展性分析的组合方法

A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems

这项工作提出了一个组成的分布式集成模块化航空电子（DIMA）系统，包括空间分布的ARINC-653模块连接一个统一的AFDX网络的可扩展性分析的方法。我们在UPPAAL中将DIMA系统建模为一组秒表自动机，通过模型检验验证其可并行性。然而，直接的模型检验是不可行的，由于大的状态空间。因此，我们引入了组合分析，它检查每个分区，包括单独的通信环境。基于消息接口的概念，构建了一些消息发送者自动机来为分区的环境建模。我们定义了一个定时选择模拟关系，它支持复合消息接口的建设。通过使用假设保证推理，我们确保每个任务都满足最后期限，并且通信约束也在全球范围内得到满足。该方法被应用到一个具体的DIMA系统的分析。

基于标号迁移系统和Boole方程系统网络的部分模型检验

Partial Model Checking using Networks of Labelled Transition Systems and Boole an Equation Systems

部分模型检验是Andersen于1995年提出的一种基于过程组合的时序逻辑公式检验方法。它包括将从一个过程中获取的行为信息逐步纳入公式-一个称为“验证”的操作-以获得一个新的公式，该公式可以在较小的组合物上进行验证，该组合物中已去除了所纳入的过程。必须在每一步对公式进行简化，以便使公式保持在易于处理的规模。在本文中，我们重温部分模型检验。首先，我们扩展到网络的标记的过渡系统模型，其中包括大多数并行组合运算符，包括m-之间的n同步和并行组合使用同步接口，可在CRTOS标准。其次，我们重新制定一个简单的同步产品之间的图形表示的公式（称为公式图）和一个过程中，从而使recruenting被有效地和容易地实现，通过重用现有的工具专用于图形组合物。第三，我们提出了简化的公式作为一个组合的互模拟和减少使用布尔方程系统直接应用到公式图，从而使公式简化也可以有效地实现。最后，我们描述了在CADP（分布式进程的构建和分析）工具箱中的实现，并提出了一些实验结果，其中部分模型检验使用的内存比飞行模型检验少几百倍。

异步环境中普适上下文的行为一致性约束检测

Checking Behavioral Consistency Constraints for Pervasive Context in Asynchronous Environments

上下文一致性检查是上下文感知应用中必不可少的一部分，它是对上下文属性的特定约束的检查。为了描述和适应普适计算环境中的动态变化，上下文感知应用程序通常需要指定和检查上下文上的行为一致性约束。这个问题是具有挑战性的，主要是由于分布式和异步的普适计算环境的性质。具体而言，检查行为约束的关键问题是上下文活动的时间顺序。上下文活动通常涉及多个上下文收集设备，这些设备是完全分散的并且以异步方式交互。然而，现有的上下文一致性检查方案不工作在异步环境中，因为它们隐含地假设一个全局时钟的可用性或中继同步的交互。为此，我们提出了有序的全球活动（OGA）算法，它检测的基础上谓词检测在异步环境中的全球活动的顺序。我们的方法的本质是消息的因果关系和它的动态编码为异步环境中的逻辑向量时钟。我们实现了在异步环境中的谓词检测的中间件基础设施（MIPA），OGA算法的实现和评估。评估结果表明，行为一致性约束检查的影响，这证明了我们的工作的主要动机。实验结果还表明，OGA可以在动态普适计算环境中实现行为一致性约束的精确检测。

参数化多方会话类型

Parameterised Multiparty Session Types

对于许多应用级分布式协议和并行算法，参与者的集合、消息的数量或交互结构仅在运行时才知道。本文提出了一个多方会话的依赖类型论，它可以静态地保证类型安全的，无死锁的多方进程之间的互动，其规格由索引参数化。我们使用哥德尔系统T中的原始递归运算符来表达广泛的通信模式，同时保持类型检查的可判定性。为了对单个分布式进程进行类型化，将参数化的全局类型投影到表示所有可能的端点类型的类的通用生成器上。我们证明了终止的类型检查算法在整个系统与多方会话类型和递归类型。我们说明了我们的类型论通过非平凡的编程和验证的例子，从并行算法和Web服务用例。

具有实数与浮点数的循环图神经网络的逻辑刻画

Logical Characterizations of Recurrent Graph Neural Networks with Reals and Floats

本文在浮点数和实数两种场景下给出了循环图神经网络的精确逻辑刻画，并证明在MSO可定义属性上两者的表达能力等价，同时通过分布式自动机建立了与分布式计算模型的联系。

异步分布式系统有界综合的高效迹编码

Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems

由于组件和环境的异步交互，分布式系统的手动实现是一项容易出错的任务。有界合成自动生成一个实现的规范的分布式系统，如果存在的话。到目前为止，分布式系统的有界合成并没有利用它们的异步特性。相反，组件的并发行为由所有交织编码，然后才根据规范进行检查。我们关闭这个差距，确定真正的并发合成的异步分布式系统表示为Petri网游戏。这定义了几个交织何时可以被一个真正的并发跟踪所包含。因此，更少和更短的验证问题，必须解决在每次迭代的有界综合算法。对于Petri网游戏，实验结果表明，我们的实现使用真正的并发性优于基于检查所有交织的实现。

Twin-width VI: the lens of contraction sequences

A contraction sequence of a graph consists of iteratively merging two of its vertices until only one vertex remains. The recently introduced twin-width graph invariant is based on contraction sequences. More precisely, if one puts red edges between two vertices representing non-homogeneous subsets, the twin-width is the minimum integer $d$ such that a contraction sequence keeps red degree at most $d$. By changing the condition imposed on the trigraphs (i.e., graphs with some edges being red) and possibly slightly tweaking the notion of contractions, we show how to characterize the well-establi…

iOrgs（TM）信息系统的规范和承诺：直接逻辑（TM）和间接接地检查

Norms and Commitment for iOrgs(TM) Information Systems: Direct Logic(TM) and Participatory Grounding Checking

当涉及到组织时，事件演算的基本假设过于简单化，在这些组织中，时变属性必须被积极地维护和管理，以便继续持有，并且不需要通过另一个动作来终止属性不再持有。即，如果不采取积极措施，事态就会自动失控。同样地，基于一组接地推断的系统接地检查属性也需要扩展和修订。以前的模型检验是基于时间点确定的状态，使用非确定自动机模型进行的。这些非确定性自动机不适合iOrg，iOrg是高度结构化的，只具有松散的非确定性。iOrg信息系统已经被开发为一种技术，在该技术中，组织具有与信息技术紧密集成的人员，该信息技术使组织能够在组织上运作。iOrg将现有的实践形式化，以提供一个框架，用于使用类似于人类组织的方法来解决权限、责任、可伸缩性和鲁棒性等问题。iOrg是Web服务的自然扩展，是大规模组织计算中分布式计算和软件应用互操作的标准。-iOrgs由组织承诺构成，组织承诺是物质承诺的一种特殊情况，被定义为承诺的信息。iOrgs规范被用来说明以下几点：-即使是一个非常简单的规范推理微观理论可以产生不一致在实践中，这是不可能验证的理论的一致性，为一个实际的领域。- 提高推理的安全性。在实际推理中使用经典逻辑和概率论是不安全的。

A Mechanized Proof of Bounded Convergence Time for the Distributed Perimeter Surveillance System (DPSS) Algorithm A

The decentralized perimeter surveillance system (DPSS) seeks to provide a decentralized protocol for evenly distributing surveillance of a perimeter over time across an ensemble of unmanned aerial vehicles (UAVs) whose members may communicate only when in close proximity to each other. The protocol must also converge to an even distribution of the perimeter in bounded time. Two versions of the DPSS protocol presented in the original paper seem to converge in bounded time but only informal proofs and arguments are given. A later application of model checking to these protocols found an error in…

相似性图上的认知逻辑：共同知识、分布式知识与互知知识

Epistemic Logic over Similarity Graphs: Common, Distributed and Mutual Knowledge

本文研究基于加权图相似性模型的认知逻辑，提出八种扩展语言以刻画共同、分布式与互知知识，并分析其表达力、语义对应、证明系统及相关计算复杂性。