Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes

命题和模态包含逻辑中的模型检验与有效性

Model Checking and Validity in Propositional and Modal Inclusion Logics

命题包含逻辑和模态包含逻辑是属于基于团队语义的逻辑家族的形式主义。本文研究了这些逻辑的模型检验和有效性问题。我们确定这两个问题的复杂性界限，包括宽松和严格的团队语义。通过这样做，我们接近完成该计划，其最终目的是分类的中心推理问题的复杂性模态和命题依赖，独立性和包含逻辑。

Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability

We study the computational complexity of model checking and satisfiability problems of polyadic modal logics extended with permutations and Boolean operators on accessibility relations. First, we show that the combined complexity of the model checking problem for the resulting logic is PTime-complete. Secondly, we show that the satisfiability problem of polyadic modal logic extended with negation on accessibility relations is ExpTime-complete. Finally, we show that the satisfiability problem of polyadic modal logic with permutations and Boolean operators on accessibility relations is ExpTime-c…

描述逻辑SHI中知识库可满足性检验的无割ExpTime表

Cut-Free ExpTime Tableaux for Checking Satisfiability of a Knowledge Base in the Description Logic SHI

我们给出了第一个无割ExpTime（最优）Tableau决策过程，用于检查描述逻辑SHI中的知识库的可满足性，它扩展了描述逻辑ALC的传递角色，逆角色和角色层次。

单变量直觉命题逻辑的模型检验问题是AC1-complete

The model checking problem for intuitionistic propositional logic with one variable is AC1-complete

我们证明了单变量直觉命题逻辑的模型检验问题对于对数空间一致AC 1是完备的。作为基本工具，我们使用直觉主义逻辑和海廷代数之间的联系，并探讨其复杂性的理论方面。对于单变量超直觉逻辑，我们得到了模型检验问题的NC 1-完全性。

时序逻辑路径检测的复杂性

On the Complexity of Temporal-Logic Path Checking

在LTL或MTL等时态逻辑中，给定一个公式，一个基本问题是在给定的有限字上计算公式的复杂性。对于LTL，这项任务的复杂性最近被证明是在NC。本文给出了LTL的一种定量（或度量）扩展MTL的NC算法，并给出了LTL的一元片段UTL的NCC算法。在撰写本文时，MTL是具有NC路径检查算法的最具表现力的逻辑，UTL是LTL的最具表现力的片段，其路径检查算法比完整的LTL更有效（服从标准复杂性理论假设）。然后，我们建立LTL路径检查和平面电路之间的连接，我们利用它来表明，在确定LTL路径检查的精确复杂性的任何进一步的进展将立即需要更有效的评估算法比已知的某一类平面电路。这种连接进一步暗示了LTL路径检查的复杂性取决于所允许的布尔连接词：添加布尔异或产生一个具有P-完全路径检查问题的时态逻辑。

COOL-MC 中面向模态不动点逻辑的通用模型检测

Generic Model Checking for Modal Fixpoint Logics in COOL-MC

本文提出参数化模型检测工具 COOL-MC，支持多种 μ-演算实例，并通过归约奇偶博弈或惰性局部算法进行检测和基准评估。

混合时空逻辑用于汽车应用：建模与模型检查

Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking

本文提出一种混合时空逻辑（HSTL）用于高速公路驾驶安全，通过定义语义和三种模型检查算法，优化搜索空间以提高性能。

平面结构上计数时态逻辑的模型检验

Model-checking Counting Temporal Logics on Flat Structures

我们研究了几个扩展的线性时间和计算树的时间逻辑与量词，允许计数经常某些属性举行。对于大多数这些扩展，模型检验问题是不可判定的，但我们表明，可判定性可以恢复考虑平坦的Kripke结构，每个状态属于最多一个简单的循环。大多数决策程序是基于（平面）计数器系统的结果，其中计数器用于实现计数运算符的评估。

单计数器博弈模型的模型检验定量交替时序逻辑

Model-checking Quantitative Alternating-time Temporal Logic on One-counter Game Models

我们考虑定量扩展的交替时间时序逻辑ATL/ATL称为定量交替时间时序逻辑（QATL/QATL），其中计数器的值可以比较使用等式，不等式和模约束的常数。我们解释这些逻辑在一个计数器的游戏模型，这是无限的持续时间的游戏有限的控制图，每个过渡可以增加或减少一个无界计数器的值。也就是说，这些游戏的状态空间通常是无限的。我们考虑的模型检验问题的逻辑QATL和QATL的一个计数器的游戏模型与VASS语义，我们开发的算法，并提供匹配的下界。我们的算法是基于减少的模型检验问题的模型检验游戏。这种方法使我们很容易处理扩展的逻辑语言以及无限的状态空间。该框架一方面概括了定性问题，如有限状态系统的ATL/ATL模型检验、单计数器过程上的分支时间时序逻辑CTL和CTL的模型检验以及LTL规范的可实现性问题。另一方面，QATL/QATL的模型检验问题推广了定量问题，如能源博弈（在QATL的情况下）和能源平价博弈（在QATL的情况下）的固定初始信用问题。我们的结果是积极的，因为我们表明，泛化是不是太昂贵的复杂性。作为一个副产品，我们获得了新的结果的复杂性模型检验CTL在一个计数器的过程中，并表明，决定赢家在一个计数器的游戏与LTL的目标是2 ExpSpace完成。

神经模型检验

Neural Model Checking

本研究提出结合机器学习与符号推理的神经模型检验方法，以神经网络为线性时序逻辑的形式化证明证书，经无监督训练和符号验证实现可靠的硬件形式化验证，性能优于现有主流模型检验工具。

用正则表达式扩展的认知Halpern-Shoham逻辑的模型检验

Model Checking Epistemic Halpern-Shoham Logic Extended with Regular Expressions

认知Halpern-Shoham逻辑（EHS）是一种时间-认知逻辑，它将Halpern-Shoham逻辑的区间算子与认知模态相结合。EHS的语义是基于解释系统，其标签功能定义在区间的端点上。我们表明，这个定义可以概括为允许标签功能的基础上，整个区间的正则表达式。我们证明，所有已知的EHS的积极成果，特别是吸引人的复杂性，其模型检验问题的一些片段，仍然持有其推广。我们还提出了新的逻辑EHSre操作标准Kripke结构，并具有表达能力相当于EHS与正则表达式。我们比较EHSre的表达能力与标准的时间逻辑。

模型检验概率时间认知逻辑的不可判定案例（扩展摘要）

Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic (Extended Abstract)

我们调查的时间，知识和概率的模型检查逻辑的可判定性，相对于两个认知语义：时钟和同步完美召回部分观察离散时间马尔可夫链的语义。可判定性的结果是已知的某些限制逻辑关于这些语义，受到各种各样的限制，要么是无法解释的，或涉及一个长期未解决的数学问题。我们表明，温和的推广已知的可判定的情况下，足以使模型检验问题明确不可判定。特别地，对于同步完美召回，从有限到达的时态算子到无限到达的算子的推广使得模型检验不可判定。时钟语义的情况下是密切相关的时间和概率的一元二阶逻辑，已知是可判定的，除了一组测量零。我们表明，这种逻辑的两个不同的扩展，使模型检验不可判定。其中之一涉及概率项的多项式组合，另一个涉及到概率算子范围内的一元二阶量化。这些结果解释了以前工作中的一些限制。

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

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

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

Model checking and model synthesisfrom partial models: a logic-based perspective

I consider the following generic scenario: an abstract model M of some 'real' system is only partially presented, or partially known to us, and we have to ensure that the actual system satisfies a given specification, formalised in some logical language. This scenario has at least two essentially different interpretations, leading to two, essentially different, formal logical and algorithmic problems: "Model Synthesis from Partial Models", where some 'admissible' extension of M to a full model must satisfy the specification, and "Model Checking of Partial Models", where all 'admissible' extens…

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

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

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

有理Kripke模型上时态逻辑的符号模型检验

Symbolic model checking of tense logics on rational Kripke models

本文引入了有理Kripke模型类，研究了基本时态逻辑Kt的符号模型检验及其在该类模型中的一些扩展。有理Kripke模型基于（通常是无限的）有理图，顶点由某些正则语言中的单词标记，转换由异步双头有限自动机（也称为有理转换器）识别。在理性Kripke模型中，每个原子命题都在一组规则的状态中求值。证明了Kt的每个公式在每个有理Kripke模型中都有一个有效的可计算正则扩张，从而证明了有理Kripke模型中Kt的局部模型检验和全局模型检验是可判定的.这些结果被提升到Kt的一些扩展。我们研究并部分确定了模型检验过程的复杂性。

单计数器自动机上的有记忆线性时间逻辑的模型检验

Model checking memoryful linear-time logics over one-counter automata

我们研究的复杂性的LTL与寄存器（也称为冻结LTL）和一阶逻辑的数据相等性测试在一个计数器自动机的模型检查问题。我们考虑几类一计数器自动机（主要是确定性与非确定性）和几个逻辑片段（限制寄存器或变量的数量和使用命题变量的控制位置）。逻辑能够存储计数器值，并在以后根据当前计数器值对其进行测试。我们证明了在确定性单计数器自动机上的模型检验是PSPACE完备的，具有无限和有限的接受运行。通过对非确定单计数器自动机的分析，证明了在不确定单计数器自动机上，直到算子仅限于最终算子的模型检验冻结LTL是不可判定的，即使只使用一个寄存器且不使用命题变量.作为我们证明的推论，这也适用于数据相等性测试仅限于两个变量的一阶逻辑。这使得一个事实，即一计数器自动机的几个验证问题是已知的相对较低的复杂性是可判定的，并且两个逻辑的有限可满足性是可判定的。我们的研究结果铺平了道路，模型检查记忆（线性时间）逻辑在其他类别的操作模型，如反向有界计数器机。

命题投影时态逻辑的概率模型检验

Probabilistic Model Checking for Propositional Projection Temporal Logic

命题投影时序逻辑（Propositional Projection Temporal Logic，PPTL）是一种用于硬件和软件系统中时间段推理的有用形式，可以处理顺序和并行组合。本文基于离散时间马尔可夫链，研究了PPTL的概率模型检验方法，用于检验任意线性时间性质。我们首先定义一个范式图，表示为NFG_inf，捕捉PPTL公式的无限路径。由于离散时间马尔可夫链是确定性的概率模型，我们进一步根据Safra的构造方法给出了确定和最小化非确定性NFG_inf的算法。

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

Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics

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

概率时间认知逻辑中模型检验的不可判定情形

Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic

我们调查的时间，知识和概率的模型检查逻辑的可判定性，相对于两个认知语义：时钟和同步完美召回部分观察离散时间马尔可夫链的语义。可判定性的结果是已知的某些限制逻辑关于这些语义，受到各种各样的限制，要么是无法解释的，或涉及一个长期未解决的数学问题。我们表明，温和的推广已知的可判定的情况下，足以使模型检验问题明确不可判定。特别地，对于同步完美召回，从有限到达的时态算子到无限到达的算子的推广使得模型检验不可判定。时钟语义的情况下是密切相关的时间和概率的一元二阶逻辑，已知是可判定的，除了一组测量零。我们表明，这种逻辑的两个不同的扩展，使模型检验不可判定。其中之一涉及概率项的多项式组合，另一个涉及到概率算子范围内的一元二阶量化。这些结果解释了以前工作中的一些限制。

Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard

The entailment between separation logic formulae with inductive predicates, also known as symbolic heaps, has been shown to be decidable for a large class of inductive definitions. Recently, a 2-EXPTIME algorithm was proposed and an EXPTIME-hard bound was established; however no precise lower bound is known. In this paper, we show that deciding entailment between predicate atoms is 2-EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines.

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

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

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

模型检测带立场模态的线性时序逻辑

Model Checking Linear Temporal Logic with Standpoint Modalities

本文提出带立场模态的线性时序逻辑的五种语义及通用模型检测算法，并证明三种情况下问题为PSPACE完全，区别于可满足性的EXPSPACE完全。

索引线性逻辑与高阶模型检验

Indexed linear logic and higher-order model checking

在最近的工作中，Kobayashi观察到，交替树自动机A接受由高阶递归方案G生成的无限树T，可以用公式表示为递归方案G在与自动机A相关联的适当交集类型系统中的可类型性。这篇文章的目的是建立一个干净的联系，这行的工作和Bucciarelli和Ehrhard的索引线性逻辑。这是通过两个步骤实现的。首先，我们将Kobayashi的结果改写为一个等价的无穷交型系统，其中交不再是幂等的。然后，我们表明，由此产生的类型系统是一个片段的Bucciarelli和Ehrhard的索引线性逻辑的无限版本。虽然这项工作是非常初步的，并没有集成高阶模型检查的关键成分，如优先级，它揭示了一个有趣的和有前途的高阶模型检查和线性逻辑之间的联系。

在排除拓扑 minors 的图类上检查不相交路径逻辑

Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes

研究在排除拓扑 minor 的图类上，证明不相交路径逻辑的模型检查问题固定参数可处理，并指出其在子图闭类上的可处理性。

Temporal Logic and Model Checking for Operator Precedence Languages

In the last decades much research effort has been devoted to extending the success of model checking from the traditional field of finite state machines and various versions of temporal logics to suitable subclasses of context-free languages and appropriate extensions of temporal logics. To the best of our knowledge such attempts only covered structured languages, i.e. languages whose structure is immediately "visible" in their sentences, such as tree-languages or visibly pushdown ones. In this paper we present a new temporal logic suitable to express and automatically verify properties of ope…

基于可能性测度的计算树逻辑模型检验

Computation Tree Logic Model Checking Based on Possibility Measures

为了解决可能性理论中不确定信息的系统验证问题，Li和\cite{li12}引入了线性时间特性的模型检验，其中不确定性用可能性测度来建模。Xue，Lei和Li \cite{Xue09}定义了基于可能性测度的计算树逻辑（CTL），称之为可能性CTL（PoCTL）。本文是上述工作的继续。首先，我们研究了PoCTL的表现力。不同于概率CTL，它表明，PoCTL（特别是，定性PoCTL）是更强大的CTL就其表现力。详细给出了基本CTL公式与定性PoCTL公式的等价表达式。给出了一些不能用任何CTL公式表示的PoCTL公式。特别地，用PoCTL公式表示了重复可达性和持久性的一些定性性质.接着，采用CTL模型检测算法，详细讨论了PoCTL模型检测问题的解决方法及其时间复杂度。最后，通过一个实例说明了PoCTL模型检验方法。

XPL：概率变迁系统的扩展概率逻辑

XPL: An extended probabilistic logic for probabilistic transition systems

广义概率逻辑（Generalized Probabilistic Logic，GPL）是一种基于模态μ演算的时态逻辑，用于描述反应概率系统的属性。我们探讨XPL，GPL的扩展，允许在马尔可夫决策过程（MDPs）中存在的非确定性的语义。XPL的表达能力足够强，许多独立研究的问题--例如递归MDP（RMDP）的终止、MDP的PCTL* 模型检验和分支MDP的可达性--都可以转换为XPL上的模型检验。多出口RMDPs的终止是不可判定的;因此，XPL中的模型检验一般是不可判定的。我们定义了一个子类，称为可分离的XPL，其中模型检验是可判定的。可判定的问题，如1-出口RMDP的终止，MDP的PCTL* 模型检验，以及分支MDP的可达性，可以减少到模型检验可分离的XPL。因此，XPL形成了一个统一的框架，用于研究涉及具有非确定性和概率行为的系统的问题，而可分离的XPL提供了一种解决这些问题的可判定片段的方法。

A Decision Procedure for Guarded Separation Logic: Complete Entailment Checking for Separation Logic with Inductive Definitions

We develop a doubly-exponential decision procedure for the satisfiability problem of guarded separation logic -- a novel fragment of separation logic featuring user-supplied inductive predicates, Boolean connectives, and separating connectives, including restricted (guarded) versions of negation, magic wand, and septraction. Moreover, we show that dropping the guards for any of the above connectives leads to an undecidable fragment. We further apply our decision procedure to reason about entailments in the popular symbolic heap fragment of separation logic. In particular, we obtain a doubly-ex…

基于逻辑松弛的等价性检验

Equivalence Checking By Logic Relaxation

我们介绍了一个新的框架的等价性检查（EC）的布尔电路的基础上的一般技术称为逻辑松弛（LoR）。LoR的本质是放松要求解的公式，并计算新行为集的超集S。也就是说，S包含所有新的满足由于松弛而出现的分配，并且不包含满足原始公式的分配。集合S是由称为部分量词消去的过程生成的。如果所有可能的坏行为都在S中，那么原始公式就不可能有它们，因此这个公式所描述的性质成立。欧共体对《规则》的吸引力是双重的。首先，它有助于生成强大的归纳证明。其次，证明不等价归结为检查放松公式中存在的一些不良行为，即在原始公式的更简单版本中。我们给出了一些实验证据，支持我们的方法。

带Delta的前向Gödel逻辑的定理证明：有效性和不可满足性检验

Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability

带投影算子Delta（G_Delta）的哥德尔逻辑是一种重要的多值逻辑和中介逻辑。与经典逻辑相比，G_Delta的有效性和可满足性问题不是直接对偶的。然而，我们提供了一个统一的，计算处理这两个问题的前束公式，通过描述适当的翻译成组的顺序条款，可以进行连锁决议。为了有效性，Herbrand定理的一个版本允许我们显示标准Skolemization的可靠性。对于可满足性的翻译涉及到一个新的，扩展Skolemization方法。

第一届自 * 系统逻辑与模型检验研讨会论文集

Proceedings First Workshop on Logics and Model-checking for Self-* Systems

本卷包含了第一次自 * 系统逻辑和模型检验研讨会（MOD* 2014）的会议记录。该研讨会于2014年9月12日在意大利Bertinoro举行，是iFM 2014（第11届集成形式方法国际会议）的卫星活动。研讨会的重点是展示形式化方法对现代复杂系统的适用性，具有高度的自适应性和可重构性，通过汇集研究人员和从业人员，推动逻辑和模型检验的最新发展。

一种带频率算子的概率时态逻辑及其模型检验

A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking

概率计算树逻辑（PCTL）和连续随机逻辑（CSL）通常分别用于描述离散时间和连续时间的概率属性规范。在PCTL和CSL中，执行满足某些时态性质的可能性可以通过其基本计算树逻辑（CTL）中路径量词的概率扩展来定量表示，但它们的路径公式在CTL中是通过相同的运算符来表示的。由于这个原因，它们都不能表示具有定量时间属性的公式，例如“某些属性在路径上超过80%的时间点（在某个有界区间内）保持不变”的形式。本文引入了一个新的时态算子来表达事件频率的概念，并在CTL \star的基础上定义了概率频率时态逻辑（PFTL）。因此，我们可以很容易地表示概率系统中的行为的时间属性。然而，它是很难开发一个完整的PFTL模型检查，由于丰富的表现力。相应地，我们开发了一个模型检测算法的CTL类片段的PFTL对有限状态马尔可夫链，和一个近似的模型检测算法的有界线性时序逻辑（LTL）类片段的PFTL对可数状态马尔可夫链。

一阶模型检验问题中的二分法和对偶性

Dichotomies and Duality in First-order Model Checking Problems

我们研究的复杂性的模型检验问题，固定的模型A，在一定的片段L的一阶逻辑。这些有时被称为L的表达式复杂性。我们得到各种复杂性分类定理，这些逻辑L的范围在模型A，在二分法猜想的约束满足问题的精神-这本身可以被看作是模型检验问题的存在合取正一阶逻辑。

用一阶逻辑检查超属性的可满足性

Checking Satisfiability of Hyperproperties using First-Order Logic

本文提出FOLHyper工具，通过将超属性问题转化为一阶逻辑公式，实现对超属性可满足性的自动检查，扩展了HyperLTL的分析范围。

闭包空间的模型检验空间逻辑

Model Checking Spatial Logics for Closure Spaces

计算的空间方面在计算机科学中变得越来越相关，特别是在集体自适应系统领域和处理分布在物理空间中的系统时。传统的形式化验证技术非常适合于分析程序的时间演化，然而，空间的属性通常没有显式地考虑。我们提出了一个基于拓扑的方法来形式化验证的空间属性依赖于物理空间。我们定义了一个适当的逻辑，它源于模态逻辑的拓扑解释传统，可以追溯到塔斯基等早期逻辑学家，其中模态描述了邻近性。我们提升的拓扑定义更一般的设置封闭空间，也包括离散的，基于图形的结构。我们扩展的框架与空间包围运营商，传播运营商和一些集体运营商。后者被解释为任意的点集，而不是空间中的单个点。我们定义了有效的模型检验程序，无论是个人和集体的空间片段的逻辑，并提供了一个概念验证工具。

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

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

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

面向通用联锁逻辑的验证：Dafny 与参数化模型检验的结合

Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking

本文针对可实例化于多类车站的通用联锁逻辑，结合 Dafny 编码、模板不变式与参数化模型检验器生成的不变式，实现关键安全性质的自动化参数化验证。

基于概率表逻辑程序设计的模型检验

Model Checking with Probabilistic Tabled Logic Programming

我们提出了一个公式的问题的概率模型检验的概率逻辑程序的查询评价之一。据我们所知，我们的公式是第一个，它涵盖了丰富的概率模型和概率时态逻辑。现有的概率逻辑编程系统的推理算法定义良好，只有有限数量的解释查询。这个限制禁止概率模型检查器的编码，其中解释对应于被模型检查的系统的执行。为了克服这个限制，我们提出了一个更一般的推理算法，使用有限的生成结构（类似于自动机）来表示家庭的解释。推理算法直接从有限的生成结构计算可能无限的解释集合的概率。我们已经实现了我们的推理算法在XSB Prolog中，并使用这种实现来编码各种时态逻辑的概率模型检查器，包括PCTL和GPL（其中包含PCTL*）。我们的实验结果表明，尽管他们的编码的高度声明性的性质，以这种方式构建的模型检查器与他们的本地实现是有竞争力的。

SCTL：面向结合模型检验和证明检验

SCTL: Towards Combining Model Checking and Proof Checking

模型检验和自动定理证明是形式化方法的两大支柱。本文从自动定理证明的角度研究模型检验，旨在将自动定理证明的表达性和模型检验的完全自动性结合起来。本文的重点是Kripke模型的时序逻辑性质的验证。本文的主要贡献是：首先定义了一个允许多元谓词符号的扩展计算树逻辑，然后以Kripke模型为参数，为该逻辑设计了一个证明系统，然后设计了一个用于该演算的证明搜索算法和一个新的自动定理证明器来实现它。验证过程是完全自动的，并且在属性不成立时产生一个反例，或者证书实验结果比较以及现有的国家的最先进的工具，在一些基准，包括应用到空中交通管制和设计选择，导致这种效率进行了讨论。

Foundations for Entailment Checking in Quantitative Separation Logic (extended version)

Quantitative separation logic (QSL) is an extension of separation logic (SL) for the verification of probabilistic pointer programs. In QSL, formulae evaluate to real numbers instead of truth values, e.g., the probability of memory-safe termination in a given symbolic heap. As with \SL, one of the key problems when reasoning with QSL is \emph{entailment}: does a formula f entail another formula g? We give a generic reduction from entailment checking in QSL to entailment checking in SL. This allows to leverage the large body of SL research for the automated verification of probabilistic pointer…

模态逻辑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+在两个玩家的游戏，并在软件模型检验的反例最小化。

Temporal-Logic Query Checking over Finite Data Streams

This paper describes a technique for inferring temporal-logic properties for sets of finite data streams. Such data streams arise in many domains, including server logs, program testing, and financial and marketing data; temporal-logic formulas that are satisfied by all data streams in a set can provide insight into the underlying dynamics of the system generating these streams. Our approach makes use of so-called Linear Temporal Logic (LTL) queries, which are LTL formulas containing a missing subformula and interpreted over finite data streams. Solving such a query involves computing a subfor…

L2C2：基于逻辑的LSC一致性检查

L2C2: Logic-based LSC Consistency Checking

实时序列图（LSC）已被提出作为一个基于对象间的规范和反应式系统的可视化程序设计语言。在本文中，我们引入了一个基于逻辑的框架来检查LSC规范的一致性。一个LSC模拟器已经在逻辑编程中实现，利用记忆化的深度优先搜索策略，以显示LSC中的反应系统将如何响应一组外部事件序列。定义了一个正式的符号来指定外部事件序列，用并行运算符和测试控件扩展了正则表达式。并行运算符允许在LSC中同时测试交织的并行外部事件;而测试控件为用户提供了一种新的方法来指定和测试某些时间属性（例如，CTL公式）。我们的框架还提供了一个状态转换图或故障跟踪证明一致性检查结果。

通过嵌套序列发展直觉时序逻辑的回路检查与反模型提取

Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents

本文提出一种新的嵌套序列证明搜索方法，用于直觉时序逻辑，支持有限反模型提取。通过引入基于同态的回路检查方法，限制了证明搜索中推导的高度。由于某些推理规则不可逆，算法构建的是称为'计算树'的广义结构，展示了如何从计算树中提取证明和反模型。

利用逻辑谜题中的不对称性：使用ZDD对动态认知逻辑进行符号模型检测

Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic

本文提出用ZDDs替代BDDs对动态认知逻辑中的Kripke模型进行符号编码，并在三个经典多智能体谜题上验证了该方法可显著降低模型检测的内存使用。

技术报告：资源约束的ATL模型检验及资源的生产和消耗

Technical Report: Model-Checking for Resource-Bounded ATL with Production and Consumption of Resources

文献中已经提出并研究了几种表示资源约束下联盟能力的逻辑。已有的工作表明，如果只考虑资源的消耗，或者系统中任意路径上产生或消耗的资源总量是有界的，那么几种标准逻辑（如资源有界联合逻辑（RB-CL）和资源有界交替时序逻辑（RB-ATL））的模型检验问题是可判定的.然而，对于具有无限资源生产和消费的联盟逻辑，只知道一些不可判定性结果。本文证明了资源无限生产和无限消耗的RB-ATL的模型检验问题是可判定的，但是EXPSPACE困难的.我们还调查了一些易于处理的情况下，并提供了一个详细的比较，资源逻辑RAL的一个变种，连同新的复杂性结果。

基于交替Büchi下推系统的共享资源有界系统的模型检验

Model Checking Resource Bounded Systems with Shared Resources via Alternating Büchi Pushdown Systems

资源受限的多智能体系统的验证一般是不可判定的。在许多这样的设置中，资源对于代理是私有的。本文研究了基于交替时序逻辑（ATL）的资源逻辑在共享资源下的模型检验问题。资源可以被消耗和生产到任何数量。我们表明，模型检验问题是不可判定的，如果两个或两个以上的这样的无界资源。我们的主要技术成果是，在一个单一的共享资源的情况下，问题变得可判定。虽然直观，可判定性的证明是不平凡的。我们减少模型检验的问题交替Büchi下推系统。一个中间结果连接到一般的基于自动机的验证：我们表明，模型检验计算树逻辑（CTL）（紧凑）交替Büchi下推系统是可判定的。

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…

基于轨迹表示的Halpern和Shoham区间时序逻辑片段的模型检验

Model Checking for Fragments of Halpern and Shoham's Interval Temporal Logic Based on Track Representatives

模型检验允许人们根据系统行为的形式模型（通常是Kripke结构）自动验证系统预期属性的规范。基于点的时态逻辑，如LTL、CTL和CTL*，描述了系统如何逐状态演化，通常用作规约语言。他们证明自己在各种应用领域相当成功。然而，属性约束的时间顺序的时间扩展的事件，以及涉及时间聚合，这是固有的间隔为基础的属性，不能正确地处理它们。区间时态逻辑（ITLs），以间隔作为其原始的时间实体，原来是非常适合的规范和验证的间隔计算属性（我们解释的所有轨道的Kripke结构作为计算间隔）。研究了Halpern和Shoham的时间区间模态逻辑（HS）的部分片段的模型检验问题。HS的特点是每对区间之间的每种可能的排序关系（所谓的艾伦关系）都有一种模态。首先，我们描述了一个EXPSPACE模型检验算法的HS片段的艾伦的关系满足，满足，开始，开始，和完成，它利用的可能性找到，为每个轨道（无限长），一个等效的有界长度的轨道代表。在检查属性时，它只需要考虑长度不超过给定界限的轨迹。我们证明了这样一个片段的模型检验问题是PSPACE困难的。最后，我们确定了其他表现良好的HS片段，这些片段的表达能力足以捕捉系统的有意义的区间特性，如互斥，状态可达性和非饥饿，其复杂性小于或等于LTL。

线性逻辑的有限语义与高阶模型检验

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

在本文中，我们解释了如何高阶模型检验和线性逻辑之间的连接最近展出的作者导致一个新的和概念上启发性的证明选择问题最初建立的Carayol和塞尔使用可折叠的下推自动机。其主要思想是从一个无限的和有色的关系语义已经制定了的的BiddayY演算，并取代它的有限对应的基础上有限素代数格。给定一个高阶递归方案G，其在模型中解释的有限性使我们能够将一个新的高阶递归方案G_phi与任何MSO公式φ联系起来，解决选择问题。

DL-PA和DCL-PC：模型检验和可满足性问题确实在PSPACE中

DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE

证明了命题控制动态逻辑DL-PA和命题控制委托联合逻辑DCL-PC的模型检验和可满足性问题都是在PSPACE中进行的。我们解释了为什么（Balbiani，Herzig，Troquard，2013）中提出的DL-PA的模型检验问题的EXPTIME-硬度证明是错误的。我们还解释了为什么在PSPACE的成员证明的模型检验问题的DCL-PC（van der Hoek，Walther，Wooldridge，2010）是错误的。

实时的模型检验：参数无处不在

Real-Time Model-Checking: Parameters everywhere

本文研究离散时间自动机上逻辑TCTL的模型检验和参数综合问题，其中参数在模型（时间自动机）和属性（时态公式）中都允许.我们的结果如下。在消极的一面，我们表明，模型检验问题的TCTL扩展参数是不可判定的离散时间自动机只有一个参数时钟。不可判定性结果需要逻辑上的等价性。在积极的一面，我们表明，模型检验和参数合成问题成为可判定的一个片段的逻辑是不允许的平等。我们的方法是基于自动机理论的原则和扩展我们的方法来表示时间自动机使用Presburger算法的运行持续时间。

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

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

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