Quantitative Computation Tree Logic Model Checking Based on Generalized Possibility Measures
本文研究了广义可能性计算树逻辑模型检验，它是Y.Li，Y.Li and Z.Ma（2014）提出的可能性计算逻辑模型检验的扩展.该系统采用广义可能性Kripke结构（GPKS，简称）建模，验证性质由广义可能性计算树逻辑（GPoCTL，简称）公式描述.基于广义可能性测度和广义必要性测度，讨论了广义可能性计算树逻辑模型检验的方法，并详细说明了相应的算法及其复杂性。此外，给出了（2013）中引入的PoCTL与GPoCTL的比较。最后以恒温器为例说明了GPoCTL模型检测方法。
2014-09-23 cs.LO
Molecular Model Checking a Temporal Logic
分子计算已经成功地用于解决越来越多的复杂计算问题。然而，作为一个重要的复杂问题，模型检验在分子计算环境下还远未得到完全解决，因为它仍然缺乏方法。为了解决这个问题，一个模型检验方法提出了一个给定的时序逻辑使用分子计算检查的基本结构。通过设计新的编码和调用这个过程，我们得到了一个基于分子的方法来检查这个逻辑的所有基本结构。
2017-02-20 cs.LO
Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds
路径检查是模型检验问题的一种特殊情况，其中所考虑的模型是单个路径，在监视、测试和验证中起着重要的作用。我们证明了线性时间时序逻辑（LTL），路径检查可以有效地并行化。除了核心逻辑，我们考虑扩展的LTL与有界未来（BLTL）和过去的时间（LTL+过去）运营商。尽管这两个扩展都以指数方式提高了逻辑的简洁性，但路径检查仍然可以有效地并行化：我们对LTL、LTL+Past和BLTL+Past的算法是在AC ^1（logDCFL）\subseteq NC中。
2012-10-19 cs.LO
Model Checking and Validity in Propositional and Modal Inclusion Logics
命题包含逻辑和模态包含逻辑是属于基于团队语义的逻辑家族的形式主义。本文研究了这些逻辑的模型检验和有效性问题。我们确定这两个问题的复杂性界限，包括宽松和严格的团队语义。通过这样做，我们接近完成该计划，其最终目的是分类的中心推理问题的复杂性模态和命题依赖，独立性和包含逻辑。
2017-04-24 cs.LO
Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability
研究了可达性关系上的多元模态逻辑的模型检验的计算复杂性和可满足性问题。首先，我们证明了所得到的逻辑的模型检验问题的组合复杂性是PTime完全的。其次，我们证明了可及性关系上的否定扩展的多元模态逻辑的可满足性问题是ExpTime-完全的。最后，我们证明了可达性关系上的置换和布尔运算符的多元模态逻辑的可满足性问题是ExpTime-完全的，在必要的假设下，可以使用的可达性关系的数量是有界的常数。
2022-10-03 cs.LO
Cut-Free ExpTime Tableaux for Checking Satisfiability of a Knowledge Base in the Description Logic SHI
我们给出了第一个无割ExpTime（最优）Tableau决策过程，用于检查描述逻辑SHI中的知识库的可满足性，它扩展了描述逻辑ALC的传递角色，逆角色和角色层次。
2012-07-16 cs.LO
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-完全路径检查问题的时态逻辑。
2014-04-28 cs.LO
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
本文提出参数化模型检测工具 COOL-MC，支持多种 μ-演算实例，并通过归约奇偶博弈或惰性局部算法进行检测和基准评估。
2023-11-03 cs.LO
Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking
TU Wien（维也纳工业大学）；National Institute of Advanced Industrial Science and Technology (AIST)（国立产业技术综合研究所）；National Institute of Informatics (NII)（国立情报学研究所）
本文提出一种混合时空逻辑（HSTL）用于高速公路驾驶安全，通过定义语义和三种模型检查算法，优化搜索空间以提高性能。
2026-03-27 cs.LO
Model-checking Counting Temporal Logics on Flat Structures
我们研究了几个扩展的线性时间和计算树的时间逻辑与量词，允许计数经常某些属性举行。对于大多数这些扩展，模型检验问题是不可判定的，但我们表明，可判定性可以恢复考虑平坦的Kripke结构，每个状态属于最多一个简单的循环。大多数决策程序是基于（平面）计数器系统的结果，其中计数器用于实现计数运算符的评估。
2017-06-26 cs.LO
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完成。
2014-09-19 cs.LO
Model Checking Epistemic Halpern-Shoham Logic Extended with Regular Expressions
认知Halpern-Shoham逻辑（EHS）是一种时间-认知逻辑，它将Halpern-Shoham逻辑的区间算子与认知模态相结合。EHS的语义是基于解释系统，其标签功能定义在区间的端点上。我们表明，这个定义可以概括为允许标签功能的基础上，整个区间的正则表达式。我们证明，所有已知的EHS的积极成果，特别是吸引人的复杂性，其模型检验问题的一些片段，仍然持有其推广。我们还提出了新的逻辑EHSre操作标准Kripke结构，并具有表达能力相当于EHS与正则表达式。我们比较EHSre的表达能力与标准的时间逻辑。
2015-09-02 cs.LO
Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic (Extended Abstract)
我们调查的时间，知识和概率的模型检查逻辑的可判定性，相对于两个认知语义：时钟和同步完美召回部分观察离散时间马尔可夫链的语义。可判定性的结果是已知的某些限制逻辑关于这些语义，受到各种各样的限制，要么是无法解释的，或涉及一个长期未解决的数学问题。我们表明，温和的推广已知的可判定的情况下，足以使模型检验问题明确不可判定。特别地，对于同步完美召回，从有限到达的时态算子到无限到达的算子的推广使得模型检验不可判定。时钟语义的情况下是密切相关的时间和概率的一元二阶逻辑，已知是可判定的，除了一组测量零。我们表明，这种逻辑的两个不同的扩展，使模型检验不可判定。其中之一涉及概率项的多项式组合，另一个涉及到概率算子范围内的一元二阶量化。这些结果解释了以前工作中的一些限制。
2016-06-24 cs.LO
Model checking and model synthesisfrom partial models: a logic-based perspective
我考虑以下一般情况：一个抽象的模型M的一些“真正的”系统只是部分介绍，或部分已知的，我们必须确保实际的系统满足给定的规范，形式化的一些逻辑语言。这种情况至少有两个本质上不同的解释，导致两个本质上不同的形式逻辑和算法问题：“部分模型的模型合成”，其中M到完整模型的一些“可接受”扩展必须满足规范，和“部分模型的模型检验”，其中M到完整模型的所有“可接受”扩展必须满足规范。这些问题自然地扩展了经典的可满足性、有效性和模型检验的逻辑决策问题。在这里，我简要地讨论这两个问题的背景下，经典，模态和时间逻辑。我做了一些观察，状态一些开放的问题，并概述了一个一般的表格式的程序，解决了几个著名的模态和时序逻辑，包括有限的部分模型的无约束模型合成的问题。K、LTL、CTL、ATL。
2020-12-22 cs.LO
Symbolic model checking of tense logics on rational Kripke models
本文引入了有理Kripke模型类，研究了基本时态逻辑Kt的符号模型检验及其在该类模型中的一些扩展。有理Kripke模型基于（通常是无限的）有理图，顶点由某些正则语言中的单词标记，转换由异步双头有限自动机（也称为有理转换器）识别。在理性Kripke模型中，每个原子命题都在一组规则的状态中求值。证明了Kt的每个公式在每个有理Kripke模型中都有一个有效的可计算正则扩张，从而证明了有理Kripke模型中Kt的局部模型检验和全局模型检验是可判定的.这些结果被提升到Kt的一些扩展。我们研究并部分确定了模型检验过程的复杂性。
2008-10-30 cs.LO
Model checking memoryful linear-time logics over one-counter automata
我们研究的复杂性的LTL与寄存器（也称为冻结LTL）和一阶逻辑的数据相等性测试在一个计数器自动机的模型检查问题。我们考虑几类一计数器自动机（主要是确定性与非确定性）和几个逻辑片段（限制寄存器或变量的数量和使用命题变量的控制位置）。逻辑能够存储计数器值，并在以后根据当前计数器值对其进行测试。我们证明了在确定性单计数器自动机上的模型检验是PSPACE完备的，具有无限和有限的接受运行。通过对非确定单计数器自动机的分析，证明了在不确定单计数器自动机上，直到算子仅限于最终算子的模型检验冻结LTL是不可判定的，即使只使用一个寄存器且不使用命题变量.作为我们证明的推论，这也适用于数据相等性测试仅限于两个变量的一阶逻辑。这使得一个事实，即一计数器自动机的几个验证问题是已知的相对较低的复杂性是可判定的，并且两个逻辑的有限可满足性是可判定的。我们的研究结果铺平了道路，模型检查记忆（线性时间）逻辑在其他类别的操作模型，如反向有界计数器机。
2010-01-18 cs.LO
Probabilistic Model Checking for Propositional Projection Temporal Logic
命题投影时序逻辑（Propositional Projection Temporal Logic，PPTL）是一种用于硬件和软件系统中时间段推理的有用形式，可以处理顺序和并行组合。本文基于离散时间马尔可夫链，研究了PPTL的概率模型检验方法，用于检验任意线性时间性质。我们首先定义一个范式图，表示为NFG_inf，捕捉PPTL公式的无限路径。由于离散时间马尔可夫链是确定性的概率模型，我们进一步根据Safra的构造方法给出了确定和最小化非确定性NFG_inf的算法。
2010-11-05 cs.LO
Logical Step-Indexed Logical Relations
Appel和McAllester的“step-indexed”逻辑关系已被证明是一种简单而有效的技术，用于推理具有语义上有趣的类型（如通用递归类型和通用引用类型）的语言中的程序。然而，使用步骤索引模型的证明通常涉及繁琐，容易出错和证明模糊的步骤索引算法，因此重要的是要开发干净，高级，等式证明原则，避免提及步骤索引。在本文中，我们展示了如何以一种抽象而优雅的方式推理二进制步进索引逻辑关系。具体来说，我们定义了一个逻辑LSLR，它的灵感来自于Plotkin和Abadi的参数化逻辑，但也支持递归定义的关系，通过模态“后来”的运营商从Appel，Melliès，Richards，和Quillon的“非常模态模型”的文件。我们在LSLR编码的逻辑关系的推理相关的程序调用的值系统F扩展一般递归类型。利用这种逻辑关系，我们得到了一组有用的规则，我们可以证明上下文等价和近似结果，而不计步骤。
2011-06-06 cs.LO cs.PL
Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics
虽然在扩展完整布尔基的逻辑中进行推理是困难的，但限制于模态语言的合取片段有时允许即使在存在最大不动点的情况下也进行易于处理的推理。一个这样的例子是EL家族的描述逻辑;在这里，有效的推理是基于满意度检查在适当的小模型，表征公式的模拟。然而，众所周知，并不是每一种合取模态语言都有一个易于处理的推理问题。自然的问题是，这些易处理的片段有多常见，以及如何识别它们。在这项工作中，我们提供了足够的条件，在一般的方式，考虑未标记的Tableau规则，为一个给定的模态逻辑的易处理性。我们工作的框架内的coalgebraic逻辑作为一个统一的语义设置。除了恢复已知的结果描述逻辑，如EL和FL 0，我们获得了新的关联和非关联模态逻辑的最大不动点的合取片段。最值得注意的是，我们发现了游戏逻辑和交替时间μ演算的易处理片段。
2014-06-06 cs.LO
Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic
我们调查的时间，知识和概率的模型检查逻辑的可判定性，相对于两个认知语义：时钟和同步完美召回部分观察离散时间马尔可夫链的语义。可判定性的结果是已知的某些限制逻辑关于这些语义，受到各种各样的限制，要么是无法解释的，或涉及一个长期未解决的数学问题。我们表明，温和的推广已知的可判定的情况下，足以使模型检验问题明确不可判定。特别地，对于同步完美召回，从有限到达的时态算子到无限到达的算子的推广使得模型检验不可判定。时钟语义的情况下是密切相关的时间和概率的一元二阶逻辑，已知是可判定的，除了一组测量零。我们表明，这种逻辑的两个不同的扩展，使模型检验不可判定。其中之一涉及概率项的多项式组合，另一个涉及到概率算子范围内的一元二阶量化。这些结果解释了以前工作中的一些限制。
2015-11-10 cs.LO
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard
带有归纳谓词的分离逻辑公式之间的蕴涵，也称为符号堆，已经被证明对于一大类归纳定义是可判定的。最近，提出了一个2-EXPTIME算法，并建立了一个EXPTIME硬界限，但没有精确的下限是已知的。在本文中，我们证明了决定谓词原子之间的蕴涵是2-EXPTIME困难的。证明是基于减少从指数空间有界交替图灵机的成员问题。
2020-04-16 cs.LO
Model Checking Linear Temporal Logic with Standpoint Modalities
本文提出带立场模态的线性时序逻辑的五种语义及通用模型检测算法，并证明三种情况下问题为PSPACE完全，区别于可满足性的EXPSPACE完全。
2025-02-27 cs.LO
Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes
University of Bremen（不来梅大学）；LIRMM, Univ Montpellier, CNRS（蒙彼利埃大学，法国国家科学研究中心，计算机科学与微技术实验室）
研究在排除拓扑 minor 的图类上，证明不相交路径逻辑的模型检查问题固定参数可处理，并指出其在子图闭类上的可处理性。
2026-02-16 cs.LO
Inducing syntactic cut-elimination for indexed nested sequents
本文通过建立标记相继式与索引嵌套相继式的对应关系，为索引嵌套相继式演算引入句法切割消去证明，并首次为中间逻辑构造了无切割的索引嵌套相继式演算。
2018-11-23 cs.LO
Temporal Logic and Model Checking for Operator Precedence Languages
在过去的几十年中，大量的研究工作一直致力于扩展模型检验的成功，从传统的有限状态机和各种版本的时态逻辑领域的上下文无关语言的适当子类和适当的时态逻辑的扩展。据我们所知，这些尝试只涵盖了结构化语言，即结构在句子中立即“可见”的语言，如树语言或明显的下推语言。本文提出了一种新的时态逻辑，它适用于表示和自动验证操作符先后次序语言的性质。这个“历史悠久”的语言家族最近被证明具有基本的代数和逻辑特性，使其适合于模型检验应用，但打破了可见结构语言的障碍（事实上，其发明者Floyd的最初动机只是为了支持有效的解析，即构建语言句子的“隐藏语法树”）。我们证明，我们的逻辑至少是表达类似的逻辑定义为可见的下推语言，但涵盖了一个更强大的家庭，我们设计了一个程序，在我们的逻辑公式建立一个自动机识别满足公式的句子，其大小是在最指数的公式的长度。
2018-09-10 cs.LO
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模型检验方法。
2014-01-19 cs.LO
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提供了一种解决这些问题的可判定片段的方法。
2017-05-09 cs.LO
A Decision Procedure for Guarded Separation Logic: Complete Entailment Checking for Separation Logic with Inductive Definitions
我们开发了一个双指数决策过程的可满足性问题的保护分离逻辑-一个新的片段的分离逻辑具有用户提供的归纳谓词，布尔连接词，分离连接词，包括限制（保护）版本的否定，魔术棒，和septraction。此外，我们表明，上述任何连接词的警卫下降导致一个不可判定的片段。我们进一步应用我们的决策过程的原因蕴涵在流行的符号堆片段的分离逻辑。特别是，我们获得了一个双指数决策过程之间的蕴涵（无量词）符号堆与有界树宽（SLIDbtw）的归纳谓词定义-分离逻辑的最具表现力的可判定片段之一。再加上最近显示的2 ExpTime-hardness在所述片段中的蕴涵，我们得出结论，SLIDbtw的蕴涵问题是2 ExpTime-complete-从而关闭了以前开放的复杂性差距。
2021-04-20 cs.LO
Equivalence Checking By Logic Relaxation
我们介绍了一个新的框架的等价性检查（EC）的布尔电路的基础上的一般技术称为逻辑松弛（LoR）。LoR的本质是放松要求解的公式，并计算新行为集的超集S。也就是说，S包含所有新的满足由于松弛而出现的分配，并且不包含满足原始公式的分配。集合S是由称为部分量词消去的过程生成的。如果所有可能的坏行为都在S中，那么原始公式就不可能有它们，因此这个公式所描述的性质成立。欧共体对《规则》的吸引力是双重的。首先，它有助于生成强大的归纳证明。其次，证明不等价归结为检查放松公式中存在的一些不良行为，即在原始公式的更简单版本中。我们给出了一些实验证据，支持我们的方法。
2016-07-11 cs.LO
Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability
带投影算子Delta（G_Delta）的哥德尔逻辑是一种重要的多值逻辑和中介逻辑。与经典逻辑相比，G_Delta的有效性和可满足性问题不是直接对偶的。然而，我们提供了一个统一的，计算处理这两个问题的前束公式，通过描述适当的翻译成组的顺序条款，可以进行连锁决议。为了有效性，Herbrand定理的一个版本允许我们显示标准Skolemization的可靠性。对于可满足性的翻译涉及到一个新的，扩展Skolemization方法。
2012-03-05 cs.LO
A MALL Geometry of Interaction Based on Indexed Linear Logic
本文为乘法-加法线性逻辑构建基于索引线性逻辑的交互几何，扩展了Haghverdi-Scott范畴框架，利用索引处理加法消割的叠加、擦除和收缩，并证明执行公式沿消割不变，收敛到无割证明的指称。
2020-07-28 cs.LO
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对可数状态马尔可夫链。
2011-11-14 cs.LO
Checking Satisfiability of Hyperproperties using First-Order Logic
本文提出FOLHyper工具，通过将超属性问题转化为一阶逻辑公式，实现对超属性可满足性的自动检查，扩展了HyperLTL的分析范围。
2025-12-29 cs.LO
Model Checking Spatial Logics for Closure Spaces
计算的空间方面在计算机科学中变得越来越相关，特别是在集体自适应系统领域和处理分布在物理空间中的系统时。传统的形式化验证技术非常适合于分析程序的时间演化，然而，空间的属性通常没有显式地考虑。我们提出了一个基于拓扑的方法来形式化验证的空间属性依赖于物理空间。我们定义了一个适当的逻辑，它源于模态逻辑的拓扑解释传统，可以追溯到塔斯基等早期逻辑学家，其中模态描述了邻近性。我们提升的拓扑定义更一般的设置封闭空间，也包括离散的，基于图形的结构。我们扩展的框架与空间包围运营商，传播运营商和一些集体运营商。后者被解释为任意的点集，而不是空间中的单个点。我们定义了有效的模型检验程序，无论是个人和集体的空间片段的逻辑，并提供了一个概念验证工具。
2016-10-07 cs.LO
Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
本文针对可实例化于多类车站的通用联锁逻辑，结合 Dafny 编码、模板不变式与参数化模型检验器生成的不变式，实现关键安全性质的自动化参数化验证。
2024-02-29 cs.LO
Model Checking with Probabilistic Tabled Logic Programming
我们提出了一个公式的问题的概率模型检验的概率逻辑程序的查询评价之一。据我们所知，我们的公式是第一个，它涵盖了丰富的概率模型和概率时态逻辑。现有的概率逻辑编程系统的推理算法定义良好，只有有限数量的解释查询。这个限制禁止概率模型检查器的编码，其中解释对应于被模型检查的系统的执行。为了克服这个限制，我们提出了一个更一般的推理算法，使用有限的生成结构（类似于自动机）来表示家庭的解释。推理算法直接从有限的生成结构计算可能无限的解释集合的概率。我们已经实现了我们的推理算法在XSB Prolog中，并使用这种实现来编码各种时态逻辑的概率模型检查器，包括PCTL和GPL（其中包含PCTL*）。我们的实验结果表明，尽管他们的编码的高度声明性的性质，以这种方式构建的模型检查器与他们的本地实现是有竞争力的。
2012-04-20 cs.LO
SCTL: Towards Combining Model Checking and Proof Checking
模型检验和自动定理证明是形式化方法的两大支柱。本文从自动定理证明的角度研究模型检验，旨在将自动定理证明的表达性和模型检验的完全自动性结合起来。本文的重点是Kripke模型的时序逻辑性质的验证。本文的主要贡献是：首先定义了一个允许多元谓词符号的扩展计算树逻辑，然后以Kripke模型为参数，为该逻辑设计了一个证明系统，然后设计了一个用于该演算的证明搜索算法和一个新的自动定理证明器来实现它。验证过程是完全自动的，并且在属性不成立时产生一个反例，或者证书实验结果比较以及现有的国家的最先进的工具，在一些基准，包括应用到空中交通管制和设计选择，导致这种效率进行了讨论。
2017-09-30 cs.LO
The model checking problem for intuitionistic propositional logic with one variable is AC1-complete
我们证明了单变量直觉命题逻辑的模型检验问题对于对数空间一致AC 1是完备的。作为基本工具，我们使用直觉主义逻辑和海廷代数之间的联系，并探讨其复杂性的理论方面。对于单变量超直觉逻辑，我们得到了模型检验问题的NC 1-完全性。
2011-09-15 cs.CC cs.LO
L2C2: Logic-based LSC Consistency Checking
实时序列图（LSC）已被提出作为一个基于对象间的规范和反应式系统的可视化程序设计语言。在本文中，我们引入了一个基于逻辑的框架来检查LSC规范的一致性。一个LSC模拟器已经在逻辑编程中实现，利用记忆化的深度优先搜索策略，以显示LSC中的反应系统将如何响应一组外部事件序列。定义了一个正式的符号来指定外部事件序列，用并行运算符和测试控件扩展了正则表达式。并行运算符允许在LSC中同时测试交织的并行外部事件;而测试控件为用户提供了一种新的方法来指定和测试某些时间属性（例如，CTL公式）。我们的框架还提供了一个状态转换图或故障跟踪证明一致性检查结果。
2010-02-16 cs.LO
Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents
Technische Universität Dresden（德累斯顿工业大学）
本文提出一种新的嵌套序列证明搜索方法，用于直觉时序逻辑，支持有限反模型提取。通过引入基于同态的回路检查方法，限制了证明搜索中推导的高度。由于某些推理规则不可逆，算法构建的是称为'计算树'的广义结构，展示了如何从计算树中提取证明和反模型。
2026-03-31 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
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。
2017-09-06 cs.LO
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）是错误的。
2014-11-28 cs.LO
Real-Time Model-Checking: Parameters everywhere
本文研究离散时间自动机上逻辑TCTL的模型检验和参数综合问题，其中参数在模型（时间自动机）和属性（时态公式）中都允许.我们的结果如下。在消极的一面，我们表明，模型检验问题的TCTL扩展参数是不可判定的离散时间自动机只有一个参数时钟。不可判定性结果需要逻辑上的等价性。在积极的一面，我们表明，模型检验和参数合成问题成为可判定的一个片段的逻辑是不允许的平等。我们的方法是基于自动机理论的原则和扩展我们的方法来表示时间自动机使用Presburger算法的运行持续时间。
2007-02-27 cs.LO
Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains
本文针对量子连续时间马尔可夫链，提出结合代数与数值方法的连续随机逻辑模型检验方案，确立了CSL的可判定性并保证计算效率，还给出示例演示方法应用。
2025-11-10 cs.LO
Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
近年来，基于区间时态逻辑的模型检验作为基于标准点时态逻辑（如LTL、CTL、CTL* 等）的模型检验的可行替代方案而出现。像往常一样，系统的行为通过（有限）Kripke结构来建模。然而，虽然被解释为“逐点”的时间逻辑描述了系统如何逐状态地演变，以及系统状态的谓词属性，但那些被解释为“逐区间”的时间逻辑表达了计算延伸的属性，跨越了一系列状态。假设一个命题字母在一个计算延伸（间隔）上保持不变，当且仅当它在每个分量状态上保持不变（同质性假设）。一个自然的问题出现了：用间隔代替点作为主要的时间实体有什么好处，或者这只是一个品味问题？本文研究了Halpern和Shoham的区间时态逻辑（HS）在模型检验中的表达能力，并与LTL、CTL和CTL* 进行了比较。为此，我们考虑HS的三种语义变体：基于状态的变体，由Montanari等人引入，它允许时间在过去和将来都分支，基于计算树的一个，它只允许时间在将来分支，基于轨迹的变体，它不允许时间分支。这些变体相互比较，并与上述标准逻辑进行比较，得到一个完整的画面。特别是，我们表明，HS与跟踪为基础的语义是相当于LTL（但至少指数更简洁），HS与计算树为基础的语义是相当于有限的CTL*，和HS与基于状态的语义是无法比拟的所有这些（LTL，CTL和CTL*）。
2018-09-24 cs.LO
Model Checking for Modal Dependence Logic: An Approach Through Post's Lattice
在本文中，我们研究了一个扩展版本的模态依赖逻辑，允许任意布尔连接词。模态依赖逻辑最近由Jouko Väänänen通过依赖原子dep（.）扩展模态逻辑而引入。本文研究了模型检验问题的计算复杂性。对于任意布尔函数的完整分类，我们使用Emil Post介绍的Lattice方法。对逻辑语言的所有片段进行这种分类，允许模态$\Diamond$和$\Box$、依赖原子和任意布尔函数的逻辑符号。
2013-03-26 cs.CC cs.LO
Statistical Model Checking : An Overview
随机系统的定量属性通常在逻辑中指定，允许将满足某些时间属性的执行度量与阈值进行比较。随机系统的模型检验问题通常是通过数值方法来解决的，该方法迭代计算（或近似）满足相关子公式的路径的精确测量;算法本身取决于被分析的系统类别以及用于指定属性的逻辑。解决模型检验问题的另一种方法是对系统进行多次运行的\emph{simulate}，并使用\emph{hypothesis testing}来推断样本是否提供了满足或违反规范的\emph{statistical}证据。在这篇简短的论文中，我们调查了统计方法，并概述了其在效率，一致性和简单性方面的主要优势。
2010-05-08 cs.LO
Model checking strategy-controlled systems in rewriting logic
本文针对 Maude 内置 LTL 模型检测器无法验证策略控制规约的问题，提出策略感知扩展，并结合表达力分析、应用示例和性能比较验证其有效性。
2024-01-15 cs.LO
Model Checking Logical Actions in Magic Tricks
本文提出魔术模型检测（MTMC）技术，将纸牌魔术的逻辑正确性问题归约为模型检测问题，以验证魔术设计是否符合预期。
2024-02-21 cs.CY cs.LO
Complexity of the Model Checking problem for inquisitive propositional and modal logic
本文研究了探究命题逻辑 InqB 和探究模态逻辑 InqM 的模型检测问题复杂性，基于 Yang 的思想证明了这两个问题均为 AP-完全。
2024-03-28 cs.LO math.LO
A Simple Probabilistic Extension of Modal Mu-calculus
概率系统是人工智能领域的一个重要课题。作为规约语言，逻辑PCTL现在是概率属性推理的默认逻辑。在本文中，我们提出了一个自然和简洁的概率扩展μ演算，另一个突出的逻辑在并发理论。我们研究了与PCTL的关系。有趣的是，表现力与PCTL高度正交。所提出的逻辑捕获了一些有用的属性，不能在PCTL中表示。研究了模型检验和可满足性问题，证明了模型检验问题是UP和co-UP问题，可满足性检验可以归结为求解奇偶对策问题.这也与PCTL相反，PCTL的可满足性检查仍然是一个悬而未决的问题。
2015-05-08 cs.LO
Predicate and relation liftings for coalgebras with side effects: an application in coalgebraic modal logic
我们研究了在存在副作用的情况下的共代数模态逻辑来验证行为等价性，即，当余代数存在于（余）Kleisli范畴或Eilenberg-Moore范畴中时。我们的目标是开发一个基于索引类别/纤维化的一般框架，这是常见的上述类别。特别是，我们展示了如何从关系提升（一种特殊的索引态射）的行为等价的coalgebraic概念，我们给出了一个一般的配方来构建这样的提升在上述三种情况下。最后，我们应用这个框架来获得（加权）语言等价和条件双相似性的逻辑特征。
2022-02-04 cs.LO
Non-idempotent intersection types in logical form
交集类型是分析函数式程序和非函数式程序的运算和指称性质的重要工具。其中，非幂等交集类型提供了有关术语和程序评估的精确定量信息。然而，与简单类型或二阶类型不同，交集类型不能被认为是一个逻辑系统，因为应用规则（或交集规则，取决于系统的表示）涉及一个条件，表示前提的证明满足一个非常强的一致性条件：底层的条件项必须相同。使用早期的工作引入索引版本的线性逻辑，我们表明，非幂等类型可以给出一个逻辑形式的系统中，公式表示遗传索引家庭的交叉类型。
2019-11-05 cs.LO
