Model Checking on Interpretations of Classes of Bounded Local Cliquewidth

从基于宽度的模型检验到基于宽度的自动定理证明

From Width-Based Model Checking to Width-Based Automated Theorem Proving

本文提出一个通用框架，将大量基于宽度的模型检验算法转换为用于测试图论猜想在有限宽度图类上有效性的算法，改进了理论上的上界。

静态模型检验中的抽象与精化

Abstraction and Refinement in Static Model-Checking

解释是建立程序的静态分析的一般方法。它是由P.和R. \cite{cc}中的Cousot。在本文中，我们提出了一个通用的抽象解释领域的模型检验的应用。动态检查通常更容易使用，因为它的概念已经建立并且广为人知。但它们通常仅限于状态空间有限的系统。在另一部分，某些故障不能动态检测，即使通过跟踪状态空间的历史。事实上，寻找正确的测试用例的经典问题是远远不够的，并进一步限制了动态检查器的能力。静态检查的优点是它们比动态检查器工作在更抽象的级别上，并且可以验证所有输入的系统属性。问题，很难保证对模型属性的违反对应于具体系统中的故障。我们提出了一种方法，在该方法中，我们动态生成反例使用的抽象解释技术。

Twin-width I: tractable FO model checking

Inspired by a width invariant defined on permutations by Guillemot and Marx [SODA '14], we introduce the notion of twin-width on graphs and on matrices. Proper minor-closed classes, bounded rank-width graphs, map graphs, $K_t$-free unit $d$-dimensional ball graphs, posets with antichains of bounded size, and proper subclasses of dimension-2 posets all have bounded twin-width. On all these classes (except map graphs without geometric embedding) we show how to compute in polynomial time a sequence of $d$-contractions, witness that the twin-width is at most $d$. We show that FO model checking, th…

关于有界树秩类、其解释及高效稀疏化

On classes of bounded tree rank, their interpretations, and efficient sparsification

本文提出有界树秩图类的分解及其高效计算，并扩展至有界扩展类；通过刻画树秩2可解释类，实现首个推广Gajarský结果的解释反转稀疏化算法。