模态$μ$模型检验博弈的描述复杂性

模态依赖逻辑的模型检验：一种基于Post格的方法

Model Checking for Modal Dependence Logic: An Approach Through Post's Lattice

在本文中，我们研究了一个扩展版本的模态依赖逻辑，允许任意布尔连接词。模态依赖逻辑最近由Jouko Väänänen通过依赖原子dep（.）扩展模态逻辑而引入。本文研究了模型检验问题的计算复杂性。对于任意布尔函数的完整分类，我们使用Emil Post介绍的Lattice方法。对逻辑语言的所有片段进行这种分类，允许模态$\Diamond$和$\Box$、依赖原子和任意布尔函数的逻辑符号。

模态μ演算模型检测的高效证据生成（扩展版）

Efficient Evidence Generation for Modal $μ$-Calculus Model Checking (extended version)

本文提出两步法求解带附加信息的参数化布尔方程系统，先解核心再利用信息，以高效生成模态μ演算模型检测的证据，并证明正确性及实现验证。

模态Mu-演算的一个简单概率推广

A Simple Probabilistic Extension of Modal Mu-calculus

概率系统是人工智能领域的一个重要课题。作为规约语言，逻辑PCTL现在是概率属性推理的默认逻辑。在本文中，我们提出了一个自然和简洁的概率扩展μ演算，另一个突出的逻辑在并发理论。我们研究了与PCTL的关系。有趣的是，表现力与PCTL高度正交。所提出的逻辑捕获了一些有用的属性，不能在PCTL中表示。研究了模型检验和可满足性问题，证明了模型检验问题是UP和co-UP问题，可满足性检验可以归结为求解奇偶对策问题.这也与PCTL相反，PCTL的可满足性检查仍然是一个悬而未决的问题。

具有同步和完全回忆语义的认知μ演算的模型检验

Model-checking an Epistemic μ-calculus with Synchronous and Perfect Recall Semantics

我们证明了模型检验问题对于认知μ演算的一个片段是可判定的。该片段允许自由变量的范围内的认知模态的限制形式，避免构建公式体现任何形式的共同知识。我们的演算包含已知的可判定的片段的认识CTL/LTL。它的模态变体可以表示两人博弈中的获胜策略，其中一个玩家具有不完美信息和不可观察的目标，并且，通过适当的编码，具有不完美信息和完美召回的ATL的模型检验问题的可判定实例可以编码为这种认知μ-演算的模型检验问题的实例。

合取余代数不动点逻辑中的包容检验

Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics

虽然在扩展完整布尔基的逻辑中进行推理是困难的，但限制于模态语言的合取片段有时允许即使在存在最大不动点的情况下也进行易于处理的推理。一个这样的例子是EL家族的描述逻辑;在这里，有效的推理是基于满意度检查在适当的小模型，表征公式的模拟。然而，众所周知，并不是每一种合取模态语言都有一个易于处理的推理问题。自然的问题是，这些易处理的片段有多常见，以及如何识别它们。在这项工作中，我们提供了足够的条件，在一般的方式，考虑未标记的Tableau规则，为一个给定的模态逻辑的易处理性。我们工作的框架内的coalgebraic逻辑作为一个统一的语义设置。除了恢复已知的结果描述逻辑，如EL和FL 0，我们获得了新的关联和非关联模态逻辑的最大不动点的合取片段。最值得注意的是，我们发现了游戏逻辑和交替时间μ演算的易处理片段。

基于一阶模态模型检验的博弈推理

Reasoning about Games via a First-order Modal Model Checking Approach

在这项工作中，我们提出了一个逻辑的基础上，一阶CTL，即游戏分析逻辑（GAL），以原因的游戏。我们将博弈论的模型和解的概念分别作为GAL的模型和公式。准确地说，我们将具有完美信息的广泛博弈表示为GAL模型，并通过GAL公式将纳什均衡和子博弈完美均衡表示出来。从实用的角度来看，我们提供了一个GAL模型检查器，以自动分析游戏。我们至少在两个方向上使用我们的模型检查器：找到博弈论的解决方案概念;以及分析基于AI社区标准算法的玩家，例如极大极小过程。

探究命题逻辑与模态逻辑的模型检测问题复杂性

Complexity of the Model Checking problem for inquisitive propositional and modal logic

本文研究了探究命题逻辑 InqB 和探究模态逻辑 InqM 的模型检测问题复杂性，基于 Yang 的思想证明了这两个问题均为 AP-完全。

模态逻辑K模型检验的最小证明搜索

Minimal Proof Search for Modal Logic K Model Checking

大多数模态逻辑，如S5、LTL或ATL，都是模态逻辑K的扩展。虽然LTL和ATL的模型检验问题在过去的几十年里一直是非常活跃的研究领域，但更基本的多智能体模态逻辑K（MMLK）的模型检验问题本身作为完美信息多人游戏的正式框架具有重要的应用。我们提出了最小证明搜索（MPS），努力数为基础的算法解决的模型检验问题MMLK。我们证明了MPS的正确性之外的两个重要性质。MPS证明对于一般的代价定义是代价最小的，MPS是寻找代价最小的证明的最优算法。最优性意味着任何类似的算法要么需要探索比MPS更大或相等的状态空间，要么不能保证在每个输入上找到最小成本的证明。因此，我们的工作涉及A* 和AO* 在启发式搜索，证明数搜索和DFPN+在两个玩家的游戏，并在软件模型检验的反例最小化。

模态依赖逻辑模型检验的复杂性

Complexity of Model Checking for Modal Dependence Logic

模态依赖逻辑（Modal Dependence Logic，MDL）是由Väänänen最近提出的。它通过操作符=（）增强了基本模态语言。对于命题变量p_1，.，p_n原子式=（p_1，...，p_（n-1），p_n）直观地说明p_n的值仅由p_1，.，p_（n-1）。我们证明了Kripke结构上MDL公式的模型检验是NP完全的，并进一步考虑了通过限制允许的命题和模态连接词的集合而得到的MDL片段。事实证明，几个片段，例如，没有情态动词或没有命题连接词的句子仍然是NP完全的。我们还考虑了MDL的限制，其中每个单个依赖原子的长度由整个逻辑固定的数字限制。我们表明，这个有界MDL的模型检验问题仍然是NP完全的。我们还通过允许经典析取（由Sevenster引入）来扩展MDL，除了依赖析取之外，并表明经典析取总是至少与有界元依赖原子一样糟糕，在某些情况下甚至更糟，例如，只有两个析取的片段是NP完全的。此外，我们几乎完全分类的计算复杂性的模型检验问题的所有限制的命题和模态算子的无界以及有界MDL。

A Survey on Satisfiability Checking for the $μ$-Calculus through Tree Automata

Algorithms for model checking and satisfiability of the modal $μ$-calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and satisfiability to checking their emptiness. The first reduces directly to the solution of parity games but the second is more complicated. We review the non-emptiness checking of alternating tree automata by a reduction to solving parity games of a certain structure, so-called emptiness games. Since the emptiness problem for alternating tree automata is EXPTIME-complete, the size …

模态μ演算片段的模型检验递归算法的复杂性

Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus

Ong证明了由n阶递归方案生成的可能无限排序树的模态μ演算模型检验问题（等价于交替奇偶树自动机（APT）接受问题）是n-EXPTIME完全的。我们认为两个子类的APT和调查各自的验收问题的复杂性。主要结果是，对于APT与一个单一的优先级，问题仍然是n-EXPTIME完全的，而对于APT与一个析取转移函数，问题是（n-1）-EXPTIME完全的。Kobayashi最近的工作表明，函数式程序的资源使用验证可以简化为递归模式的模型检验。作为一个应用，我们证明了资源使用验证问题是（n-1）-EXPTIME完全的。

高维模态μ演算的模型检验

Model-Checking the Higher-Dimensional Modal mu-Calculus

高维模态μ演算是μ演算的扩展，其中公式被解释为标记转换系统的状态元组。在这种逻辑中可以表达的每个属性都可以在多项式时间内进行检查，相反，每个具有互模拟不变编码到标记转换系统中的多项式时间可判定问题也可以在高维模态μ演算中定义。我们通过给出几个决策问题的例子来证明后一种联系，这些决策问题归结为对某些固定公式的高维模态μ演算的模型检验。通过这种方式，用于逻辑的通用模型检验算法然后可以经由部分评估来使用，以便获得用于这些问题的算法，这些算法可以受益于在程序验证领域中良好建立的改进，即运行中（on-the-fly）和符号技术。这项工作的目的是将这种技术扩展到其他领域，以及，在这里示例性地做了过程等价，自动机理论，解析，字符串问题，和游戏。

一种基于类型的HFL模型检验算法

A Type-Based HFL Model Checking Algorithm

高阶模态不动点逻辑（Higher-order Modal Fixpoint Logic，HFL）是模态μ演算的高阶扩展，并且比模态μ演算更严格地表达。最近的研究表明，各种程序验证问题可以自然地归结为HFL模型检验：一个给定的有限状态系统是否满足给定的HFL公式的问题。在本文中，我们提出了一种新的算法HFL模型检验：这是第一个实用的算法，它运行速度快的典型输入，尽管超指数最坏情况下的复杂性的HFL模型检验问题。我们的算法是基于小林等人。的HFL模型检验的基于类型的表征，并启发了基于饱和的算法HORS模型检验，另一个高阶扩展的模型检验。我们证明了算法的正确性，并报告的实施和实验结果。

模态$μ$ -演算的分解定理与模型检验

Decomposition Theorems and Model-Checking for the Modal $μ$-Calculus

我们证明了一个一般的分解定理的模式$μ$ -演算$L_μ$的精神Feferman和Vaught的定理不相交的工会。特别是，我们表明，如果一个结构（即，转换系统）由两个子结构$M_1$和$M_2$加上从$M_1$到$M_2$的边组成，则在$M$中的节点处的公式真仅取决于在相应子结构中的公式真，其意义在下面进行精确说明。因此，我们证明了$L_μ$的模型检测问题是固定参数易处理的（FPT）类结构的有界凯利宽度或有界DAG宽度。据我们所知，这些是$L_μ$的第一个FPT结果，它不遵循嵌入到一元二阶逻辑中。

Descriptive complexity for distributed computing with circuits

We consider distributed algorithms in the realistic scenario where distributed message passing is operated via circuits. We show that within this setting, modal substitution calculus MSC captures the expressive power of circuits. The translations between circuits and MSC-programs are linear in both directions. Furthermore, we show that the colouring algorithm based on Cole-Vishkin can be specified via logarithmic size programs.

多模态类型论的规范化

Normalization for multimodal type theory

本文证明了多模态依赖类型论MTT的规范化，通过将类型检查和转换简化为底层模态情况的模态相等性判断，提出了一种类型检查算法。

判定 van Glabbeek 分支时间谱中特征公式的复杂度

The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrum

本文研究了在 van Glabbeek 分支时间谱中，判定有限无环过程特征公式的复杂度，给出了可满足性与素性问题的复杂度结果，并探讨了多项式时间可解与计算困难的逻辑边界及公式构造的复杂度。

使用模态特征转换系统进行基于族的模型检验：保留CTL *（扩展版）

Abstract Family-based Model Checking using Modal Featured Transition Systems: Preservation of CTL* (Extended Version)

变量系统允许通过使用特征（配置选项）标记变量功能来有效地构建许多自定义变量。在许多应用中，其质量保证和形式化验证至关重要。基于族的模型检验通过利用变量之间的共性，允许在单次运行中同时验证变分系统的所有变量。然而，它的计算成本仍然在很大程度上取决于变体的数量（通常是巨大的）。在这项工作中，我们将展示如何实现有效的基于家庭的模型检验的CTL* 的时间属性，使用可变性抽象和现成的（单系统）工具。我们使用变异抽象派生抽象的基于族的模型检验，其中的变异模型的变分系统被替换为一个抽象的（更小的）版本，称为模态特征的过渡系统，它保留了普遍的和存在的时间属性的满意度，在CTL* 表示。模态特征变迁系统包含两类变迁，分别称为may变迁和must变迁，它们分别由保守（过近似）抽象和它们的对偶（欠近似）抽象定义。可变性抽象可以与变量集合的不同划分相结合，以推断用于变分系统的合适的分而治之验证计划。我们说明了几个变分系统的这种方法的实用性。

判定特征公式：在分支时间谱中的旅程

Deciding characteristic formulae: A journey in the branching-time spectrum

本文研究了在van Glabbeek分支时间谱中各逻辑中判定公式是否为特征公式的问题，分析了可满足性和素性问题的复杂性，并探讨了多项式时间与(co)NP或PSPACE完全问题之间的边界。

模态μ演算的有界博弈论语义

Bounded game-theoretic semantics for modal mu-calculus

我们引入了一个新的博弈论语义（GTS）的模态μ演算。我们所谓的有界GTS取代奇偶游戏与替代评估游戏，只有有限的路径出现，无限的路径是不需要的，即使当考虑的过渡系统是无限的。新的游戏提供了替代方法的各种建设的框架中的μ演算。例如，它们已经成功地用作一种方法的基础，这种方法导致逻辑的自然公式大小游戏。虽然我们的主要重点是介绍新的GTS，我们也考虑一些应用程序来演示其用途。例如，我们考虑一个自然的模型转换过程，减少模型检查游戏，检查一个单一的，固定的公式在构建的模型，我们还使用GTS识别新的替代变种的μ演算与PTime模型检查。

线性混合系统定量μ演算的模型检验

Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems

研究了一类混杂系统上模态μ演算的定量扩展的模型检测问题。定性模型检验已被证明是可判定的，并实现了几类系统，但这是不是在这种情况下自然出现的定量问题。最近，定量形式主义，substrate经典的时间逻辑，并允许有趣的定量现象的测量被引入。我们展示了如何一个强大的定量逻辑，定量μ演算，可以在初始化的线性混合动力系统的任意精度模型检查。为此，我们开发了新的技术，连续状态空间的离散化的基础上，一类特殊的战略模型检查游戏，并提出了减少一类反奇偶校验游戏。

何时素公式是特征公式？

When Are Prime Formulae Characteristic?

本文提出一般充分条件，保证模态逻辑中特征公式恰为一致且素公式，并证明该条件适用于多种行为关系，包括 van Glabbeek 谱系中的所有语义。

作为完全行为规范理论的具有最大不动点的Hennessy-Milner逻辑

Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory

有两种根本不同的方法来指定和验证系统的属性。逻辑方法利用规范给出的时间或模态逻辑的公式，并依赖于有效的模型检验算法;行为方法利用各种等价或细化检查方法，提供的规格是在相同的形式主义实现。在本文中，我们提供的最大不动点的Hennessy-Milner逻辑的逻辑形式主义和析取模态转换系统的行为形式主义之间的翻译。我们还介绍了一个新的操作商的上述等价的形式主义，这是伴随的结构组成，并允许合成缺失的规范从部分实现。这是一个实质性的推广商确定性模态过渡系统中定义的早期文件。

模型检验高阶不动点逻辑的复杂性

The Complexity of Model Checking Higher-Order Fixpoint Logic

高阶不动点逻辑（Higher-Order Fixpoint Logic，HFL）是简单类型λ演算和模态λ演算的混合。这使得它成为一个高度表达的时态逻辑，能够表达模态λ演算中无法表达的程序的各种有趣的正确性属性。本文给出了其模型检验问题的复杂性结果。特别是，我们认为这些片段的HFL只使用类型的有界阶k和arity m。我们建立k倍指数时间完备性的模型检验每个这样的片段。对于上界，我们使用不动点消除，以获得可达性游戏，是单指数的大小的公式和k倍指数的大小的底层过渡系统。这些博弈可以在确定性线性时间内求解。作为一个简单的结果，我们得到一个指数时间上界的表达复杂性的每个这样的片段。下界是由交替（k-1）重指数空间有界图灵机的字问题的一个简化而建立的。由于有固定的机器的类型，其字的问题已经很难相对于k倍指数时间，我们得到，作为一个推论，k倍指数时间完整性的数据复杂性的片段的HFL，提供m超过3。这也产生了表达能力的层次结构。

模态μ演算的一个命名证明系统

A Proof System with Names for Modal Mu-calculus

不动点是语义学、抽象解释和程序逻辑中的一个重要组成部分。它们添加到逻辑中可以增加相当大的表达能力。一个普遍的问题是如何定义这种逻辑的证明系统。在这里，我们将研究模态逻辑与不动点的证明系统。我们提出了一个Tableau证明系统，用于检查公式的有效性，它使用名称来跟踪不动点变量的展开，如Jungteerapanich所设计的。

Bounded Game-Theoretic Semantics for Modal Mu-Calculus and Some Variants

We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. For example, they have already been successfully used as a basis for an approach leading to a natural formula size game for the logic. While our main focus is introducing the new GTS, we also consider some application…

使用探针和模态μ演算自动验证实时观测器

Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus

一个经典的方法模型检查的时间属性，如那些表示使用时间扩展的时间逻辑是依赖于使用观察员。在这种情况下，一个主要的问题是证明观察者的正确性。从本质上讲，这归结为证明：（1）每一个与属性相矛盾的轨迹都可以被观察者检测到;而且（2）观察者是无害的，这意味着它不能干扰被观察的系统。在本文中，我们描述了一种自动测试实时观测器的正确性的方法。这种方法是通过自动化通常被称为视觉验证的方法来获得的，在该方法中，通过检查其状态空间的图形表示来执行系统的正确性。我们的方法已经实现的工具蒂娜，时间Petri网的模型检查工具箱。

定量μ演算的模型检验对策

Model Checking Games for the Quantitative mu-Calculus

我们研究了模态逻辑和模态μ演算的定量扩展，并研究了逻辑和游戏之间的紧密联系是否可以从定性逻辑提升到定量逻辑。事实证明，如果以适当的方式定义定量μ演算，尊重逻辑运算符之间的对偶性质，那么它的模型检验问题确实可以通过奇偶博弈的定量变体来表征。然而，这些定量游戏有相当不同的性质比他们的经典同行，特别是他们，在一般情况下，不确定的位置。逻辑和博弈之间的对应是双向的：定量转换系统上的公式的值与相关的定量博弈的值一致，相反，定量平价博弈的值在定量μ演算中是可定义的。

知道如何有多容易：可满足性问题的一个上界

How Easy it is to Know How: An Upper Bound for the Satisfiability Problem

针对基于线性计划语义的“知道如何”模态逻辑，本文通过消除嵌套模态并调用命题逻辑可满足性预言机，证明其公式可满足性检查属于 $Σ_2^P$。

具有同步和完全回忆语义的认知μ演算的模型检验

Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics

我们确定了一个子问题的模型检查问题的认知μ演算是可判定的。在这个子问题的实例中，公式允许在认知模态的范围内以限制的形式存在自由变量，以避免体现任何形式的共同知识。我们的子问题包含已知的可判定片段的认知CTL/LTL，可以表示获胜策略，在两个玩家的游戏中，一个玩家有不完美的信息和不可观察的目标，并与一个合适的编码，可判定的实例的模型检查问题的ATLiR。

基于SMT的算符优先语言符号模型检测

SMT-based Symbolic Model-Checking for Operator Precedence Languages

针对现有POTL显式状态模型检测方法可扩展性差的问题，本文提出首个基于SMT的符号化方法，将POTL公式与程序模型编码为SMT公式，通过求解器以有界模型检测方式搜索反例轨迹，实验验证了方案有效性。

连续空间的几何模型检测

Geometric Model Checking of Continuous Space

本文提出连续空间上的SLCS几何语义，引入基于多面体的模型检测器PolyLogicA，并在现实规模三维模型上验证可行性，同时给出刻画逻辑等价性的双模拟几何定义。

依赖逻辑的计算方面

Computational Aspects of Dependence Logic

本文主要研究模态依赖逻辑.它是由Jouko Vääanänen在2007年引入的，作为一阶的扩展（分别为。模态）逻辑的依赖运算符=（）。一阶（resp.）命题）变量x_1，...，x_n，=（x_1，...，x_n）直观地说明x_n的值由x_1，.，x_n-1。我们认为片段的模态依赖逻辑通过限制允许模态和命题连接词的集合。我们对这些片段的可满足性和模型检查问题的复杂性进行了分类。对于可满足性，我们获得了从P over NP，Sigma_P^2和PSPACE到NEXP的复杂度，而对于模型检查，我们只根据它们的易处理性对片段进行分类，即我们在P中显示NP-完全性或包含性。对于这个扩展，我们再次分类的复杂性模型检查问题的片段。在这里，我们获得了从P over NP和coNP到PSPACE的复杂度。最后，我们分析了一阶依赖逻辑、独立友好逻辑及其二元片段。我们证明了两个变量的依赖逻辑的可满足性是NEXP-完全的，而两个变量的独立友好的逻辑，它是不可判定的，并使用这一点来证明，后者也比前者更有表现力。

ITL模型检验的复杂性：区间逻辑HS的一些行为良好的片段

Complexity of ITL model checking: some well-behaved fragments of the interval logic HS

模型检验已成功地应用于许多计算机科学领域，包括人工智能、理论计算机科学和数据库。大多数提出的解决方案利用经典的，基于点的时序逻辑，而很少的工作已经做了区间时序逻辑设置。最近，人们提出了有限Kripke结构上Halpern和Shoham的时间区间HS模态逻辑的非初等模型检验算法（在齐性假设下）和它的两个有意义片段的EXPSPACE模型检验过程.在本文中，我们表明，更有效的模型检验程序可以开发一些表达足够的片段HS。

多下推系统分支时间特性的模型检验是困难的

Model checking Branching-Time Properties of Multi-Pushdown Systems is Hard

我们解决了多下推系统的共享内存并发程序的模型检验问题。我们认为在这里布尔程序与有限数量的线程和递归过程。众所周知，这类程序的模型检验问题是不可判定的。在本文中，我们调查的可判定性和这个问题的复杂性的假设下，有界的上下文切换定义的Qadeer和Zeroof，和相位有界的La Torre等人提出的。对时间逻辑，特别是分支时间逻辑，如模态$μ$ -演算或CTL的模型检验这样的系统很少受到关注。众所周知，与模态$μ$ -演算密切相关的奇偶博弈对于有界相位系统类是可判定的（因此对于有界上下文切换也是如此），但具有非初等复杂性（赛斯）。一个自然的问题是，这种高复杂性是否是不可避免的，有什么方法来绕过它。本文解决这些问题，不幸的是，有点令人惊讶的是，它表明，分支模型检验的MPDS本质上是一个很难的问题，没有简单的解决方案。我们证明了在相位限制下的MPDS上的奇偶博弈是非初等的。我们的主要结果表明，模型检验的$k$上下文有界MPDS对一个简单的CTL片段，由公式，其时间运营商来自集合${\EF, \EX}$，有一个非初等的下界。

随机多智能体系统中的策略能力推理

Reasoning about Strategic Abilities in Stochastic Multi-agent Systems

本文提出概率交替时间μ演算PAMC用于随机多智能体系统策略能力推理，证明其复杂度性质并给出模型检测与可满足性检测算法，实现为开源工具且验证了有效性。

Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity

We study the expressivity and complexity of model checking linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining hyperproperties, i.e., properties which relate multiple execution traces. TeamLTL has been introduced quite recently and only few results are known regarding its expressivity and its model checking problem. We relate the expressivity of TeamLTL to logics for hyperproperties obtained by extending LTL with trace and propositional quantifiers (HyperLTL and HyperQPTL). By doing so, we obtain a number of model checking re…

单计数器过程的分支时间模型检验

Branching-time model checking of one-counter processes

单计数器进程（OCP）是下推进程，只对一元堆栈字母表进行操作。研究了基于OCP的模型检验计算树逻辑（CTL）的计算复杂性。一个PSPACE上界是继承自该问题的模态μ演算。首先，我们分析的周期性行为的CTL在OCP和推导出一个模型检验算法，其运行时间是指数的控制位置和语法概念的公式，我们称之为直到深度。因此，模型检验固定OCP对CTL公式与一个固定的深度，直到在P。这概括了第一作者，Mayr，和到CTL的片段EF的表达复杂性的结果。其次，我们证明了在一定的OCP上，CTL模型检验是PSPACE困难的。第三，我们表明，已经存在一个固定的CTL公式，模型检验的OCP是PSPACE困难的。对于后者，我们使用了复杂性理论的两个结果：（i）将中国余数表示中的自然数转换为二进制表示是在对数空间一致的NC ^1中;（ii）PSPACE是AC ^0-可串行化的。我们证明，我们的方法可以用来回答进一步的开放性问题。

奇偶对策的不动点迭代算法

The Fixpoint-Iteration Algorithm for Parity Games

众所周知，模态μ演算的模型检验问题归结为求解奇偶博弈的问题，反之亦然。后者是实现的Walukiewicz公式，满足了一个节点在平价游戏如果玩家0赢得了游戏从这个节点。因此，他们定义了她的获胜区域，并且模态μ演算的任何模型检验算法，适当地专用于Walukiewicz公式，产生用于解决奇偶博弈的算法。在本文中，我们研究的效果，采用最直接的μ演算模型检验算法：不动点迭代。这也是为数不多的算法之一，如果不是唯一的一个，最初不是为奇偶博弈解决而设计的。虽然一项实证研究很快表明，这并不能产生一个在实践中运行良好的算法，但从理论上讲，这是有趣的，原因有两个：首先，它在几乎所有游戏家族上都是指数级的，这些游戏家族被设计为非常特定的算法的下限，这表明不动点迭代与所有这些算法都有联系。其次，不动点迭代不计算位置获胜策略。请注意，Walukiewicz公式只定义了获胜区域;为了使该算法计算获胜策略，还需要一些额外的工作。我们表明，这些是特殊的指数空间的战略，我们称之为最终位置，我们展示了如何位置的，可以从他们中提取。

迈向标记转移系统的现实大型随机模型及其0-1律

Towards realistic large random models of labeled transition systems and their 0-1 laws

本文利用随机图论创建大型标记转移系统概率模型，结合经验数据赋予现实参数值，分析其在LTL和CTL下渐近行为，得出收敛律或0-1律，讨论确定极限的理论复杂度并给出算法，为理解LTS行为及随机图论在模型检查中的应用提供基础。

多面体可达性逻辑

Logics of polyhedral reachability

本文针对含类Until空间模态词的多面体可达性逻辑，提出公理系统并通过两步证明其相对于多面体语义学的完备性，为3D网格模型检测等应用提供理论支撑。

直觉主义模态逻辑的一种余代数语义

A Coalgebraic Semantics for Intuitionistic Modal Logic

本文利用 Esakia 空间到 Priestley 空间包含的右伴随，为带 $\Box$ 的直觉主义模态逻辑建立余代数语义，并应用于互模拟、自由模态 Heyting 代数对偶及余代数直觉主义逻辑理论。

典范模型与模态团队逻辑的复杂性

Canonical Models and the Complexity of Modal Team Logic

该研究通过引入典范模型将模态团队逻辑MTL的可满足性简化为模型检验，并证明其复杂性为TOWER(poly)完全问题，同时刻画了有界模态深度片段的初等层级复杂性。

从$μ$ -演算到基于奇偶博弈的交替树自动机

From $μ$-Calculus to Alternating Tree Automata using Parity Games

$μ$ -无限树上的微积分和自动机是描述无限树语言的互补方式。利用$μ$ -Calculus与交替树自动机之间的对应关系，将模式$μ$ -Calculus公式编译成交替树自动机，解决了可满足性和模型检验问题.因此提倡一个自动机模型，专门为工作模式$μ$ -微积分。与Janin和Walukiewicz提出的自动机模型相比，自动机模型的优点是能够以更简单的方式处理任意分支。这两个问题（即，模型检验和可满足性）分别通过约简到交替树自动机的相应问题，即接受问题和非空问题来解决。这些问题，反过来，解决使用奇偶性游戏的语义交替树自动机被翻译成一个获胜的战略，在一个适当的奇偶性游戏。

线性逻辑的关系语义与高阶模型检验

Relational semantics of linear logic and higher-order model-checking

在这篇文章中，我们在高阶模型检验和线性逻辑之间建立了一种新的、有点出乎意料的联系。我们的出发点是观察到，一旦嵌入到线性逻辑的关系语义中，任何高阶递归方案（HORS）的Church编码都会与相同签名的交替树自动机（ATA）的对偶Church编码结合在一起。此外，HORS和ATA的关系解释之间的相互作用确定了一组接受状态的树自动机对无限树所产生的递归方案。我们将展示如何将这一结果扩展到交替奇偶自动机（APT）通过引入线性逻辑的指数模态的参数化版本，捕获高阶模型检验中颜色（或优先级）的形式属性。我们特别展示了如何重新理解以这种方式的类型理论的方法来高阶模型检验开发的小林和Ong。我们简要地解释在最后的文件如何驱动他的分析结果在一个新的和纯粹的语义证明的可判定性的公式的一元二阶逻辑的高阶递归计划。

弥补精化模态逻辑复杂性的差距

Closing a Gap in the Complexity of Refinement Modal Logic

精化模态逻辑（Refinement Modal Logic，RML），最近由Bozzelli等人提出，模态逻辑是经典模态逻辑的扩展，它允许人们对变化的模型进行推理。在本文中，我们研究与此逻辑相关的计算复杂性问题，解决了许多悬而未决的问题。具体来说，我们研究的复杂性，满足性的存在片段的RML，Bozzelli，范Ditmarsch和Pinchinat提出的问题。我们的主要结果是一个紧PSPACE上界这个问题，我们通过引入一个新的表系统实现。作为一个直接的后果，我们得到了严格的表征的复杂性RML可满足的任何固定数量的交替的细化量词。此外，通过一个简单的减少，我们建立RML的模型检验问题是PSPACE完全的，即使是一个单一的量词的公式。

通过布尔网络研究神经网络的描述复杂性

Descriptive complexity for neural networks via Boolean networks

本文从描述复杂性角度用布尔网络刻画神经网络表达能力，建立二者间的多项式规模转换，并实现任意激活函数间的等价转换。

带数据系统上模态μ演算的可监控性：从实践到理论

Monitorability for the Modal mu-Calculus over Systems with Data: From Practice to Theory

本文研究带数据系统中模态μ演算扩展逻辑的可监控性，借助与带猜测寄存器自动机的对应关系给出监控器合成算法，并证明存在严格可监控性层级且无可判定片段能捕获全部可监控性质。

并发博弈中的理性能力

Rational Capability in Concurrent Games

本文在并发博弈结构中引入偏好与基于占优的理性概念，扩展 CL 和 ATL 以表达联盟理性强制属性的能力，并给出可满足性、模型检查复杂性及公理化结果。

LTL的探究式团队语义

Inquisitive Team Semantics of LTL

本文提出受探究逻辑启发的InqLTL团队语义，证明其带布尔否定时高度不可判定且表达力弱于带布尔否定的TeamLTL，同时找到一个可判定模型检验、可表达超性质的有意义片段。