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
Erratum to: Model-checking continuous-time Markov chains by Aziz et al
本注释纠正了CSL的多重直到运算符的语义和算法之间的差异，如在Pr_{> 0.0025}（a until[1，2] b until[3，4] c）中，文章：模型检验连续时间马尔可夫链，Aziz，Sanwal，Singhal和Brayton，TOCL 1（1），2000年7月，pp. 162-170.
2011-02-10 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
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
Indexed linear logic and higher-order model checking
在最近的工作中，Kobayashi观察到，交替树自动机A接受由高阶递归方案G生成的无限树T，可以用公式表示为递归方案G在与自动机A相关联的适当交集类型系统中的可类型性。这篇文章的目的是建立一个干净的联系，这行的工作和Bucciarelli和Ehrhard的索引线性逻辑。这是通过两个步骤实现的。首先，我们将Kobayashi的结果改写为一个等价的无穷交型系统，其中交不再是幂等的。然后，我们表明，由此产生的类型系统是一个片段的Bucciarelli和Ehrhard的索引线性逻辑的无限版本。虽然这项工作是非常初步的，并没有集成高阶模型检查的关键成分，如优先级，它揭示了一个有趣的和有前途的高阶模型检查和线性逻辑之间的联系。
2015-03-17 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
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
Model Checking Finite-Horizon Markov Chains with Probabilistic Inference
我们重新审视马尔可夫链的符号验证有限时域可达性。流行的方法迭代计算步骤有界状态可达概率。相比之下，概率推理的最新进展建议用符号表示通过马尔可夫链的所有水平长度路径。我们问这种观点是否推进了概率模型检验的最新技术。首先，我们正式描述这两种方法，以突出其主要区别。然后，利用这些见解，我们开发了Rubicon，一个将Prism模型转换为概率推理工具Dice的工具。最后，我们证明了更好的可扩展性相比，概率模型检查器在选定的基准。总之，我们的研究结果表明，概率推理是一个有价值的除了概率模型检验投资组合-与Rubicon作为第一步集成两个角度。
2021-06-30 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
Model Checking Markov Chains Against Unambiguous Buchi Automata
本文给出了一个多项式时间算法，用于有限马尔可夫链的模型检验。
2016-03-26 cs.FL cs.LO
Accelerated Model Checking of Parametric Markov Chains
参数马尔可夫链很自然地出现在各种应用中：它们可以用于概率系统的保守分析（无论如何选择参数，系统都按照规范工作）;它们可以用于找到参数的最佳设置;它们可以用于可视化系统参数的影响;并且它们可以用于使得对于参数改变的情况容易地调整分析。不幸的是，这些进步是有代价的：参数模型检验通常很慢。为了使参数马尔可夫模型的分析规模化，我们需要三个要素：巧妙的算法，正确的数据结构和良好的工程。聪明的算法通常是主要的（或唯一的）卖点;我们面临着本文关注的问题--有效的模型检验的后一种成分。因此，我们最容易成名的是我们在与最先进的技术进行比较时经常意识到的速度。
2018-11-02 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
Probabilistic Model Checking for Continuous Time Markov Chains via Sequential Bayesian Inference
对于状态空间较大或无界的系统，概率模型检验是形式化建模及其应用中的一个具有挑战性的计算问题。数值算法需要状态空间的显式表示，而统计方法需要大量的样本来估计具有高置信度的所需属性。在这里，我们展示了如何模型检验的时间有界路径属性可以被重铸正是贝叶斯推理问题。在这个新的公式化的问题可以有效地近似使用技术从机器学习。我们的方法的灵感来自最近的结果，在统计物理学推导出封闭形式的微分方程的首次通过时间分布的随机过程。我们展示了一些非平凡的案例研究，我们的方法实现了高精度和显着的计算增益相比，统计模型检验。
2018-06-11 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
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
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
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
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 Markov Population Models by Stochastic Approximations
许多复杂的系统可以用种群模型来描述，在种群模型中，一群代理人相互作用并产生复杂的集体行为。我们考虑验证这些模型的基本数学表示的形式属性的问题，这些模型是一个连续时间马尔可夫链，通常具有巨大的状态空间。为了避免状态空间爆炸，我们依赖于随机近似技术，用一个更简单的模型代替大模型，保证概率一致。我们展示了如何有效和准确地验证随机个体代理的属性，指定的连续随机逻辑扩展与时间自动机（CSL-TA），以及如何提升这些规范的集体水平，近似的代理数量满足他们使用二阶或更高阶的随机近似技术。
2017-11-10 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
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
A Simple Probabilistic Extension of Modal Mu-calculus
概率系统是人工智能领域的一个重要课题。作为规约语言，逻辑PCTL现在是概率属性推理的默认逻辑。在本文中，我们提出了一个自然和简洁的概率扩展μ演算，另一个突出的逻辑在并发理论。我们研究了与PCTL的关系。有趣的是，表现力与PCTL高度正交。所提出的逻辑捕获了一些有用的属性，不能在PCTL中表示。研究了模型检验和可满足性问题，证明了模型检验问题是UP和co-UP问题，可满足性检验可以归结为求解奇偶对策问题.这也与PCTL相反，PCTL的可满足性检查仍然是一个悬而未决的问题。
2015-05-08 cs.LO
Model-Checking Process Equivalences
过程等价是一种形式化的方法，它将程序和系统联系起来，这些程序和系统在非正式的情况下以相同的方式运行。由于没有唯一的概念，这意味着两个动态系统显示相同的行为有大量的形式过程等价，从互模拟跟踪等价，分类在线性时间分支时间谱。我们提出了一个逻辑框架的基础上表达模态不动点逻辑，它是能够定义许多过程等价关系：对于每个这样的等价有一个固定的公式，这是满足一对过程，当且仅当他们是等价的，就这个关系。我们解释了如何做模型检验，甚至象征性地，这个逻辑的一个重要片段，捕捉许多过程的等价。这允许将模型检验技术用于过程等价性检验。我们展示了如何部分评估可以用来获得决策程序的通用模型检验计划的过程等价。
2012-10-09 cs.LO
A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators
Politecnico di Milano（米兰理工大学）；TU Wien（维也纳工业大学）
针对信息物理系统中带界时间算子的离散时间信号时序逻辑（STL）的可满足性检验需求，提出一种利用时间区间冗余加速的树形单次表算法，可拓展用于多种STL相关验证任务，性能优于现有最优编码方法。
2025-07-29 cs.LO
ExpTime Tableaux with Global Caching for the Description Logic SHOQ
我们给出了第一个ExpTime（复杂性最优）的tableau决策过程，用于检查描述逻辑SHOQ中知识库的可满足性，它扩展了基本描述逻辑ALC，具有传递角色，角色层次，名词和量化数量限制。复杂度是用一元数表示来衡量的。我们的程序是基于全局缓存和整数线性可行性检查。
2014-07-21 cs.LO
