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
Enriched MU-Calculi Module Checking
开放系统的模型检验问题已经在文献中得到了深入的研究，对于有限状态（模块检验）和无限状态（下推模块检验）系统，关于Ctl和Ctl*。在本文中，我们进一步研究了这个问题的μ演算丰富的名义和分次模态（混合分次μ演算），在有限状态和无限状态设置。使用自动机理论方法，我们证明了混合分级μ-演算模块检验在指数时间内是可解的，而混合分级μ-演算下推模块检验在双指数时间内是可解的.这些结果也是紧密的，因为它们匹配Ctl的已知下限。我们还研究了关于混合分级μ-演算的模块检查问题，通过展示多米诺问题的简化，我们展示了它的不可判定性。最后，我们简要概述了完全丰富的Mu演算的模型检验问题，以及通过删除至少一个额外的构造而获得的片段。
2008-07-29 cs.LO
A Survey on Satisfiability Checking for the $μ$-Calculus through Tree Automata
用于模态$μ$演算的模型检验和可满足性的算法通过将公式转换为交替奇偶校验树自动机来开始。这样，模型检验就归结为树自动机的可接受性检验和树自动机的可满足性检验。第一个直接归结为平价博弈的解，但第二个更复杂。我们回顾了交替树自动机的非空性检查，通过减少到解决某种结构的奇偶游戏，所谓的空游戏。由于交替树自动机的空性问题是EXPTIME完全的，这些游戏的大小是输入自动机状态数的指数。我们展示了如何建设的空虚游戏相结合的（固定）结构部分与（历史）确定奇偶校验字自动机。对于具有某些句法结构的树自动机，可以使用更简单的方法来处理词自动机的处理，然后词自动机可以比一般情况下渐近地更小。这些结果有直接的后果，可满足性和有效性检查（各种片段）的模式$μ$演算。
2022-08-23 cs.LO
Coalgebraic Satisfiability Checking for Arithmetic $μ$-Calculi
本文在更一般的假设下证明了余代数μ-演算可满足性检查的指数时间上界，通过通用全局缓存算法实现，并直接支持无保护公式，应用于带多项式不等式的分级μ-演算和概率μ-演算扩展。
2024-07-22 cs.LO
Constraint LTL Satisfiability Checking without Automata
本文提出了一种新的方法来判定用线性时态逻辑语言写的带有将来和过去算子的公式和属于约束系统D的原子公式的可满足性（简称CLTLB（D））。该技术基于有界可满足性的概念，并将CLTLB（D）公式编码为QF-EUD，结合了无量词等式理论和D.类似于标准LTL，其中有界模型检查和SAT求解器可以用作自动机理论方法的模型检查的替代方案，我们的方法允许用户通过SMT求解技术来解决CLTLB（D）公式的可满足性问题，而不是通过检查合适的自动机A_A的语言的空性。该技术是有效的，并已在我们的Zot形式化验证工具中实现。
2014-02-11 cs.LO
Variable and clause elimination for LTL satisfiability checking
研究了LTL公式子句范式的预处理技术。应用标记子句的机制，使我们能够重新解释LTL可满足性作为一组纯粹的命题问题，从而转移简化思想从SAT到LTL。我们证明了这一点，适应变量和子句消除，现代SAT求解器使用的一个非常有效的预处理技术。我们的实验证实，即使在时间设置的公式大小和随后的求解器运行时间的减少，可以实现大幅减少。
2013-09-30 cs.LO
MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the $\exists^*\forall^*$ Fragment
超属性是指多个计算轨迹的属性。这包括许多信息流安全策略，如观察确定性，（广义）不干扰和非推理，以及其他系统属性，如对称性或汉明距离。我们介绍MGHyper，一个自动可满足性检查和模型生成的HyperLTL表示的超属性的工具。与以往的可满足性检查器不同，MGHyper不局限于HyperLTL的可判定$\exists^* \forall^*$片段，而是为全逻辑提供了一个半判定过程。MGHyper的一个重要应用是自动检查不同超性质（以及同一超性质的不同形式化）之间的等价性，并构建反例来反驳某个声称的含义。我们描述了在MGHyper中实现的半决策过程，并报告了从文献中获得的典型超性质和随机生成的HyperLTL公式的实验结果。
2019-03-26 cs.LO
Satisfiability and Model Checking of CTL* with Graded Path Modalities
分次路径模态计算满足一个性质的路径的数量，并推广了CTL* 的存在（E）和泛（A）路径模态。生成的逻辑称为GCTL*。我们解决了GCTL* 可满足性的复杂性，即，2 ExpTime-Complete，以及GCTL* 的模型检验问题的复杂性，即，PSpace-Complete。对于CTL*，下限已经成立，因此，使用自动机理论方法，我们提供上限。这项工作的意义是双重的：GCTL* 比CTL* 更有表达力，而在计算复杂性方面没有额外的成本，并且GCTL* 具有CTL* 优于CTL的所有优点，例如，表达公平的能力。
2014-10-28 cs.LO
Checking Satisfiability of Hyperproperties using First-Order Logic
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
本文提出FOLHyper工具，通过将超属性问题转化为一阶逻辑公式，实现对超属性可满足性的自动检查，扩展了HyperLTL的分析范围。
2025-12-29 cs.LO
Fast LTL Satisfiability Checking by SAT Solvers
线性时态逻辑（LTL）的可满足性检查是检查LTL断言中可能错误的基本步骤。现存的LTL可满足性检查器使用各种不同的搜索过程。唯一的例外是基于有界模型检验的LTL可满足性检验，它没有提供一个完整的决策过程，LTL可满足性检验器没有利用过去20年在布尔可满足性求解方面取得的显著进展。在本文中，我们提出了一个新的LTL可满足性检查框架，加速使用布尔SAT求解器。我们的方法是基于变体的\emph{obligation-set method}，我们提出了在早期的工作。我们在这里描述了允许使用布尔SAT求解器来分析给定LTL公式的义务的算法。实验评估表明，新的方法提供了一个显着的性能优势。
2014-04-29 cs.DS cs.LO
Finding Connections via Satisfiability Solving
TU Wien（维也纳工业大学）；University of Southampton（南安普顿大学）
本文提出了一种基于SAT的连接演算方法，通过编码证明搜索结构来提升一阶逻辑证明的自动化水平。
2026-03-06 cs.LO
Spanning Matrices via Satisfiability Solving
本文提出将一阶连接方法编码为布尔可满足性问题，采用矩阵表示以克服树状演算的缺陷，并证明适当细化的演算可作为 Bernays-Schönfinkel 类的判定程序。
2024-02-16 cs.LO
The Complexity of Generalized HyperLTL with Stuttering and Contexts
ENS Rennes（雷恩高等师范学院）；Aalborg University（奥尔堡大学）
本文研究了包含停滞和上下文的广义超LTL的可满足性、有限状态可满足性和模型检查问题的复杂性，证明了可满足性为Σ₁¹-完全，而模型检查和有限状态可满足性则等价于二阶算术中的真值，远比可决定的超LTL模型检查问题复杂。
2026-11-02 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
SAT-Based ATL Satisfiability Checking
模型与策略的综合是软件工程中一个非常重要的问题。这里的主要内容是检查表达要实现的系统规范的公式的可满足性。提出了一种新的判定交替时序逻辑（ATL）公式可满足性的方法。该方法扩展了CTL利用SAT模单调理论求解器的方法。类似于CTL的情况下，我们的方法似乎是非常有效的。实验结果表明，我们可以快速测试的大型ATL公式，已经达到了现有的方法。
2020-02-08 cs.LO cs.MA
Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions
针对范畴论框架下的广义嵌套条件，提出基于表的半判定可满足性检验与有限模型生成方法，引入证据概念检测无限模型，采用共归纳方法证明正确性，区分两类范畴给出不同适用场景的可靠完备演算。
2024-07-09 cs.LO
Internal Calculi for Separation Logics
我们提出了一个一般的方法来公理化分离逻辑与heaplet语义没有外部功能，如名词/标签。首先，我们为无量词分离逻辑设计了第一个（内部）希尔伯特式公理化。我们实例化的方法，通过引入一个新的分离逻辑的基本特征：它配备了分离合取，谓词LS，和一个自然的保护形式的一阶量化。我们应用我们的方法，其公理化。作为我们的方法的副产品，我们还建立了这个新的逻辑的确切的表达能力，我们显示其可满足性问题的P空间完备性。
2019-10-11 cs.LO
How Easy it is to Know How: An Upper Bound for the Satisfiability Problem
针对基于线性计划语义的“知道如何”模态逻辑，本文通过消除嵌套模态并调用命题逻辑可满足性预言机，证明其公式可满足性检查属于 $Σ_2^P$。
2023-09-29 cs.LO
A Simple Probabilistic Extension of Modal Mu-calculus
概率系统是人工智能领域的一个重要课题。作为规约语言，逻辑PCTL现在是概率属性推理的默认逻辑。在本文中，我们提出了一个自然和简洁的概率扩展μ演算，另一个突出的逻辑在并发理论。我们研究了与PCTL的关系。有趣的是，表现力与PCTL高度正交。所提出的逻辑捕获了一些有用的属性，不能在PCTL中表示。研究了模型检验和可满足性问题，证明了模型检验问题是UP和co-UP问题，可满足性检验可以归结为求解奇偶对策问题.这也与PCTL相反，PCTL的可满足性检查仍然是一个悬而未决的问题。
2015-05-08 cs.LO
STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
IMT Lucca（卢卡高等研究学院）；TU Wien（维也纳工业大学）；AIT Austrian Institute of Technology（奥地利技术研究院）
研究针对网络物理系统中STL公式一致性检查难题，指出原表格法缺陷，提出新树形表格法并证明其可靠性与完备性，基于此开发STLSat工具，能判定可满足性等，评估显示其性能优于现有工具。
2026-09-18 cs.LO
Integrating deduction and model finding in a language independent setting
软件工件在我们的生活中无处不在，是家用电器、汽车、手机的重要组成部分，甚至在航空和健康科学等更重要的活动中也是如此。在这种情况下，软件故障可能会造成巨大的经济损失，或者在极端情况下，在人类生活中。软件分析是软件工程中的一个领域，它关注不同技术的应用，以证明软件工件中（相对）没有错误。在许多情况下，这些分析方法是通过遵循确保更好结果的某些方法指示来应用的。在以前的工作中，我们提出了可满足性演算的概念作为Meseguer的证明演算的模型理论对应物，为基于模型构建的各种工具提供了正式的基础。目前的工作表明如何有效的可满足性子演算，一种特殊类型的可满足性演算，可以结合证明演算，以提供基础，以某些方法的软件分析有关的建设有限的反例和证据的情况下，在一个抽象的分类设置。
2022-06-14 cs.LO cs.SE
Checking Satisfiability by Dependency Sequents
我们介绍了一种新的算法检查可满足性的基础上的演算的依赖序列（D-序列）。给定一个CNF公式F（X），一个D-T是一个记录，说明在部分赋值下，X的一组变量在公式\exists{X} [F]中是冗余的。D-序列演算基于从两个现有的D-序列形成新的D-序列的操作连接。新算法解决了SAT的量化版本。也就是说，给定一个可满足公式F，它一般不会产生一个满足F的赋值。新算法称为DS-QSAT，其中DS代表Dependency Sequent，Q代表Quantified。重要的是，类似DPLL的过程只是DS-QSAT的一种特殊情况，其中使用了非常有限的D序列。我们认为，这种限制a）对SAT求解器的可扩展性产生不利影响，b）是由于寻找一个明确的满意分配，而不仅仅是证明可满足性。我们给出了实验结果证实这些说法。
2012-07-20 cs.DM cs.LO
The Complexity of HyperQPTL
ENS Rennes（法国高等师范学院雷恩分校）；Aalborg University（奥尔堡大学）
本文研究了超QPTL和超QPTL$^+$的复杂性，发现超QPTL的可满足性为$Σ^2_1$-完全，而超QPTL$^+$的相关问题等价于第三阶算术中的真理，均为不可判定。
2026-02-23 cs.LO
Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete
IIT Bombay（印度理工学院孟买分校）；MPI-SWS（马克斯·普朗克软件系统研究所）
本文证明多变量单侧区间TPTL的可满足性检验为PSPACE完全，且其表达力严格强于MITL，但检验复杂度更低，通过归约到新的非点式交替定时自动机子类实现。
2023-09-01 cs.CL cs.FL cs.LO
MsATL: a Tool for SAT-Based ATL Satisfiability Checking
本文提出MsATL工具，结合SAT求解器与ATL模型检查器，支持判定不完美信息下ATL的可满足性及游戏合成。
2023-10-25 cs.LO cs.MA
Parametrised Complexity of Model Checking and Satisfiability in Propositional Dependence Logic
在本文中，我们开始在依赖逻辑领域的参数化复杂性的系统研究，发现它的起源于依赖逻辑的Väänänen从2007年。我们研究这个逻辑（PDL）的命题变体，并调查各种参数化相对于中央决策问题。PDL的模型检验问题是NP完全问题。本研究的主题是确定一个参数列表（公式大小，树宽，树深，团队规模，变量数）下MC成为固定参数易处理。此外，我们表明，析取的数量或依赖原子的arity（dep-arity）作为一个参数都产生paraNP-完全性的结果。然后，我们考虑的可满足性问题（SAT）显示出不同的图片：在团队规模，或deparity SAT是paraNP-完全的，而在所有其他提到的参数的问题是FPT。最后，我们介绍了一个变种的可满足性问题，要求一个给定的规模的团队，并显示这个问题的一个几乎完整的图片。
2020-06-13 cs.CC cs.LO
ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking
我们给出了第一个ExpTime（复杂性最优）的Tableau决策过程，用于检查描述逻辑SHIQ中的知识库的可满足性，当数字以一元编码时。我们的程序是基于全局状态缓存和整数线性可行性检查。
2013-12-31 cs.LO
Satisfiability Checking and Symbolic Computation
符号计算和可满足性检验被视为独立的研究领域，但它们在算术理论决策过程的开发、实现和应用方面有着共同的兴趣。尽管有这些共同点，但这两个社区目前只有微弱的联系。我们引入了一个新的项目SC-广场，以在该地区建立一个联合社区，并得到新接受的同名欧盟（H2020-FETOPEN-CSA）项目的支持。我们的目标是通过创建共同的平台，启动互动和交流，确定共同的挑战，并制定共同的路线图，加强这些社区之间的联系。这张摘要和随附的海报描述了该项目的动机和目标，并报告了第一批活动。
2016-07-23 cs.LO cs.SC
Satisfiability Checking meets Symbolic Computation (Project Paper)
符号计算和可满足性检验是两个研究领域，两者在算术理论决策过程的发展、实现和应用方面有着各自的科学重点，但也有着共同的兴趣。尽管有共同点，但这两个社区的联系相当薄弱。我们新接受的SC-square项目（H2020-FETOPEN-CSA）的目的是通过创建共同平台，启动互动和交流，确定共同挑战，以及开发从理论到工具和（工业）应用的共同路线图来加强这些社区之间的联系。在本文中，我们报告的目标和该项目的第一次活动，并正式确定了一些相关的挑战，为统一的SC广场社区。
2016-07-27 cs.LO cs.SC
Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption
本文研究子区间逻辑D在齐次性假设下的可满足性与模型检验问题，证明二者在有限结构上均为PSPACE完全，丰富了易处理区间时态逻辑家族。
2022-01-31 cs.FL 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
The Complexity of Enriched Mu-Calculi
Università di Napoli “Federico II”（那不勒斯费德里科二世大学）；TU Dresden（德累斯顿工业大学）；Microsoft Research（微软研究院）；Rice University（莱斯大学）
完全丰富演算是命题演算的逆程序、分次模态和名值的推广.虽然满足性在几个表达片段的充分丰富的演算被称为是可判定的和ExpTime完全的，它最近被证明，完整的演算是不可判定的。在本文中，我们研究的片段的充分丰富的演算，通过删除至少一个额外的结构。我们表明，在以这种方式获得的所有片段中，可满足性是可判定的和ExpTime完全的。因此，我们确定了一个家庭的可判定的逻辑是最大的（和无与伦比的）的表达能力。我们的结果是通过引入两个新的自动机模型，表明他们的空性问题是ExpTime-完全的，然后减少这些问题的相关逻辑的可满足性。我们介绍的自动机模型是双向分级交替奇偶自动机在无限树（2GAPTs）和完全丰富的自动机在无限森林（FEAs）。前者是文献中两个不可比自动机模型的常见推广。后者扩展交替自动机以类似的方式完全丰富的演算扩展标准演算。
2008-09-22 cs.CL cs.LO
On the Complexity of Dynamic Epistemic Logic
尽管动态认知逻辑（DEL）是一个很有影响力的逻辑框架，用于表示和推理信息变化，但很少有人知道其相关决策问题的计算复杂性。事实上，我们只知道，对于公告逻辑，一个片段的DEL，可满足性问题和模型检查问题分别是PSPACE-完全的，并在P.我们有助于填补这一空白，证明了事件模型的DEL语言，模型检查问题，令人惊讶的是，PSPACE-完全的。此外，我们证明了可满足性问题是NEXPTIME-完全的。在此基础上，我们给出了一个可靠的、完备的判定可满足性问题的表方法。
2013-10-23 cs.LO
On Verifying Timed Hyperproperties
我们研究的可满足性和模型检测问题的时间超属性指定的HyperMTL，HyperLTL的时间扩展。根据是否允许在不同的跟踪中交错事件，可以为定时超属性定义两种可能的语义：异步和同步。虽然可满足性问题可以决定类似于HyperLTL的语义的选择，我们表明，模型检查问题，除非规格是替代自由，是不可判定的，即使在非常有限的时间限制是允许的。在积极的一面，我们表明，模型检验HyperMTL与量词交替是可能的，在一定条件下的同步语义，或当有一个固定的时间域的长度上的界限。
2018-12-25 cs.LO
Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking
Radboud University（拉德堡德大学）；Brno University of Technology（布尔诺理工大学）
针对有限MDP上带结构约束的鲁棒奖励最优策略计算难题，本文提出结合可满足性求解器与概率模型检查的合成框架，实验证明其可行且性能媲美现有最优方法。
2025-11-15 cs.AI cs.LO
Using Symmetries to Lift Satisfiability Checking
KU Leuven（鲁汶大学）；Siemens（西门子）；Vrije Universiteit Brussels（布鲁塞尔自由大学）
本研究提出利用对称性压缩结构的两步可满足性检验方法，为带聚合的带类型一阶逻辑语句设计适配翻译，在生成式配置问题上实现大幅加速，可应用于复杂数据结构软件验证。
2023-12-14 cs.AI cs.LO
Revisiting MITL to Fix Decision Procedures
度量区间时态逻辑（Metric Interval Temporal Logic，MITL）是一种具有可判定可满足性和模型检验问题的实时时态逻辑。MITL的决策过程依赖于自动机理论方法，其中逻辑公式被转换为等效的时间自动机。由于时间自动机在互补下不封闭，MITL的决策过程首先将公式转换为否定的范式，然后再转换为时间自动机。我们发现，不幸的是，这些20岁的程序是不正确的，因为它们依赖于一个不正确的语义的R运算符。我们提出了正确的语义R，并给出了新的，正确的决策程序MITL。我们表明，可满足性和模型检验的MITL是EXPSPACE完全的，如前所述。我们还确定了一个片段的MITL，我们称之为MITL_{WI}是丰富的比MITL_{0,\infty}，我们表明，可满足性和模型检验是PSPACE完成。我们的许多结果已经在PVS中得到了形式化的证明。
2019-10-09 cs.LO
Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers
度量时态逻辑（MTL）和时间命题时态逻辑（TPTL）是线性时态逻辑（LTL）的重要实时扩展。在一般情况下，这些扩展的可满足性检查问题是不可判定的，当未来的U和过去的S模态使用。在一个经典的结果中，证明了MTL [U，S]的非准时片段MITL[U，S]的可满足性检验是可判定的，具有EXPSPACE完全复杂性。鉴于这种非准时性的概念在TPTL[U，S]的情况下不能恢复可判定性，我们提出了TPTL[U，S]的非准时性的一个推广，称为\emph{non adjacency}，并专注于它的1-变量片段1-TPTL[U，S].虽然非相邻的1-TPTL[U，S]似乎是一个非常小的片段，但它比MITL更严格地表达。作为我们的主要结果，我们证明了非相邻1-TPTL[U，S]的可满足性检验问题是可判定的，具有EXPSPACE完全复杂性。
2021-09-05 cs.LO
Model-Checking Problems as a Basis for Parameterized Intractability
大多数参数化复杂性类都是根据布尔可满足性问题（所谓的加权可满足性问题）的参数化版本来定义的。例如，Downey和Fellow的W-层次结构就是这种形式。但是也有一些类，例如A-层次，它们更自然地以一阶逻辑的某些片段的模型检验问题来表征。唐尼、费罗斯和里根是第一个在两种形式主义之间建立联系的人，他们用一阶模型检验问题来描述W-层次。我们改进了他们的结果，然后证明了A-层次和W^*-层次的加权可满足性和模型检验问题之间类似的对应关系。因此，我们获得了非常统一的许多最重要的参数化复杂性类的特征，在这两种形式主义。我们的结果可以用来给一些结构参数化复杂性理论的核心结果的新的，简单的证明。
2005-06-22 cs.CC cs.LO
The Complexity of Checking Non-Emptiness in Symbolic Tree Automata
该研究将符号树自动机的可满足性问题分解为两类理论的可满足性问题，进而得到该类自动机及其带线性算术约束扩展的判定问题的紧计算复杂度界。
2023-11-09 cs.FL cs.LO
Reasoning about Strategic Abilities in Stochastic Multi-agent Systems
本文提出概率交替时间μ演算PAMC用于随机多智能体系统策略能力推理，证明其复杂度性质并给出模型检测与可满足性检测算法，实现为开源工具且验证了有效性。
2024-12-12 cs.FL cs.GT cs.LO
Experience with Heuristics, Benchmarks & Standards for Cylindrical Algebraic Decomposition
在激发SC广场项目的论文中，[E。Abraham，在符号计算和可满足性检查之间建立桥梁，Proc. ISSAC '15，pp. 1-6，ACM，2015]作者将复杂的逻辑学的使用确定为可满足性检查社区擅长的技术，并且符号计算社区可能从中学习和繁荣。为了开始这个学习过程，我们总结了计算机代数算法柱形代数分解的启发式开发经验。我们还提出并讨论了标准和基准，作为符号计算可以从可满足性检查专业知识中蓬勃发展的另一个领域，注意到这些已被确定为CSA项目中新SC Square社区的初始行动，如[E.~ Abraham等人，SC $^2$：可满足性检查符合符号计算（项目论文）}，智能计算机数学（LNCS 9761），pp. 28- 43，Springer，2015]。
2016-09-29 cs.LO cs.SC
Bounded Satisfiability for PCTL
马尔可夫链的模型检验PCTL是多项式时间可判定的，但PCTL可满足性的判定及其有限模型性质是一个长期存在的问题。虽然一般的可满足性是一个有趣的挑战，从纯理论的角度来看，我们认为，一般的解决方案不会感兴趣的从业者：这样的解决方案可能太大，是可实现的，甚至是无限的。受有界合成技术的启发，我们转向寻求有界大小的模型的更多应用问题：我们将搜索限制在可实现的-因此相当简单的-模型。我们提出了一个程序来决定是否一个给定的PCTL公式有一个可实现的模型，减少到SMT问题。我们已经实现了我们的技术，并发现它们可以应用于健全检查的实际问题-一个程序，允许系统设计人员检查他们的公式是否有一个意外的小模型。
2012-03-30 cs.FL cs.LO
The Complexity of Fragments of Second-Order HyperLTL
本文确定了二阶 HyperLTL 多个片段的可满足性、有限状态可满足性和模型检测的复杂度，指出它们均处于解析层级及更高层级。
2025-09-16 cs.LO
Unary negation
我们研究片段的一阶逻辑和最少不动点逻辑，只允许一元否定：否定的公式，最多一个自由变量。这些逻辑概括了许多有趣的已知形式主义，包括模态逻辑和$μ$ -演算，以及合取查询和一元数据。我们证明了可满足性和有限可满足性对于两个片段都是可判定的，并且我们指出了可满足性、有限可满足性和模型检验的复杂性。我们还表明，一阶逻辑的一元否定片段是模型理论上表现良好。特别是，它享有克雷格插值和投影贝丝财产。
2013-09-23 cs.LO
Synchronous Team Semantics for Temporal Logics
University of Tübingen（蒂宾根大学）；Institut für Theoretische Informatik, Leibniz Universität Hannover（汉诺威莱布尼茨大学理论计算机科学研究所）；School of Computing Science, University of Glasgow（格拉斯哥大学计算科学学院）；Department of Computer Science, Aalborg University（奥尔堡大学计算机系）
本文为LTL和CTL提出团队语义，使其能表达超性质，研究其计算复杂度并证明带有团队语义的LTL是HyperLTL的可行替代方案。
2026-10-06 cs.LO
Parametric Interval Temporal Logic over Infinite Words
Halpern和Shoham的区间时序逻辑HS的模型检验最近已被系统地研究，它是已知的三个不同的语义下可判定。在这里，我们专注于基于轨迹的语义，其中给定（有限）Kripke结构的无限执行路径（轨迹）是主要的语义实体。在这种情况下，迹的每个有限中缀都被解释为一个区间，一个命题在区间上成立当且仅当它在每个分量状态上成立（齐性假设）。在本文中，我们介绍了一个量化的扩展HS的痕迹，称为参数HS（PHS）。新的逻辑允许表达的间隔的持续时间（长度）的参数定时约束。我们表明，检查存在的参数估值的Kripke结构满足PHS公式（模型检验），或PHS公式承认一个跟踪作为模型下的同质性假设（可满足性）是可判定的。此外，我们确定了PHS的一个片段，其中包括参数LTL和模型检验和满足性被证明是EXPSPACE完成。
2022-09-21 cs.LO
Logics and Games for True Concurrency
我们研究了基于过渡系统，Petri网和事件结构的各种偏序模型的并发性的基本数学性质，并表明这些系统的并发行为可以通过两个简单的和一般的对偶局部行为以统一的方式捕获。这种对偶性被用来定义新的μ演算和逻辑游戏，用于分析具有偏序语义的并发系统。这项工作的一些结果是：一些mu-演算的定义，在某些类的系统，诱导相同的标识作为一些最有名的互模拟等价的并发性;和定义（无限）高阶逻辑游戏的互模拟和模型检查，其中的球员的游戏给予（本地）一元二阶权力的一组元素，他们被允许发挥。更具体地说，我们表明，我们的游戏是健全的和完整的，因此，确定;此外，它们是可判定的有限情况下，并支持新的决策程序的互模拟和模型检查。由于这些mu演算和逻辑游戏概括了著名的不动点逻辑和博弈论决策程序的并发系统与交织语义，本文的结果给出了一些基础的设计一个基于逻辑的，博弈论的框架研究，在一个统一的方式，几个并发系统，无论他们是否有交织或偏序语义。
2010-11-04 cs.LO
The Complexity of Second-order HyperLTL
Bar-Ilan University（巴伊兰大学）；Aalborg University（奥尔堡大学）
本文研究了第二阶超LTL的可满足性、有限状态可满足性及模型检查问题，发现其复杂性等价于三阶算术的真实性。同时分析了两种第二阶超LTL的片段，探讨了其在限制量化范围后的复杂性变化。
2026-03-13 cs.FL cs.LO
Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem
本文针对非线性超越算术(NTA)提出了一种新的可满足性证书形式，将其转化为证书搜索问题，设计了新算法，在更多基准问题上证明了可满足性，并刻画了可证公式的范围及终止条件。
2025-03-06 cs.LO
Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations
自从Val Tannen的先驱工作简单类型的类演算和一阶重写的组合（LICS'88），许多作者都通过将其扩展到更丰富的类型类演算和重写范式，最终在演算像代数结构的演算。这些工作提供了理论基础的类型理论的证明助手的功能和谓词定义的定向高阶方程。这种定义包含了基于归纳的定义，更容易编写，并提供了更多的自动化。另一方面，检查用户定义的重写规则是强规范化和融合的，并且在与beta约简结合时保持类型检查的可判定性，则更加困难。大多数终止标准依赖于期限结构。在以前的工作中，我们扩展到依赖类型和高阶重写，“大小类型”的概念由几位作者在ML类语言的简单框架中研究，并证明了它保持了强规范化。本文件的主要贡献是双重的。首先，证明了在带尺寸标注的代数构造演算中，只要尺寸标注所产生的约束集是可满足的，并且允许最一般的解，则类型推断和类型检验问题是可判定的.其次，我们证明了一个大小代数足够丰富的捕获通常的归纳为基础的定义和更多的后来的属性。
2006-09-11 cs.LO cs.PL
Interpolation and Model Checking for Nonlinear Arithmetic
提出了一种新的基于模型的可满足性模理论插值方法。该过程使用了一种新的与SMT求解器的交互模式，我们称之为求解模模型。这要么将给定的部分模型扩展为一组断言的完整模型，要么在不存在解决方案时返回解释（模型插值）。这种交互模式非常适合SMT的模型构建可满足性（MCSAT）框架。我们用它来开发任何MCSAT支持的理论的插值程序。特别是，这种方法导致了一个有效的非线性实算术插值程序。我们评估新的程序，将其集成到一个模型检查器，并将其与最先进的非线性算法的模型检查工具进行比较。
2021-06-08 cs.LO cs.PL cs.SC
Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL*
Kansas State University（堪萨斯州立大学）
在本文中，我们提出了一个贝叶斯方法的统计模型检验（SMC）的概率超性质的逻辑HyperPCTL* 上的离散时间马尔可夫链（DTMCs）。虽然SMC的HyperPCTL* 使用序贯概率比检验（SPRT）已经探索过，我们开发了一种替代SMC算法的基础上贝叶斯假设检验。与PCTL* 相比，验证HyperPCTL* 公式是复杂的，因为它们在DTMC的多个路径上同时解释。此外，由于SMC不返回子公式的可满足性问题的精确答案，而是仅返回具有高置信度的正确答案，因此扩展非概率设置的自底向上模型检查算法并不直接。我们提出了一个递归算法的SMC的HyperPCTL* 的基础上修改贝叶斯检验，在递归可满足性结果的不确定性的因素。我们已经实现了我们的算法在Python工具箱，HyProVer，并比较我们的方法与基于SPRT的SMC。我们的实验评估表明，我们的贝叶斯SMC算法在验证时间和推导给定HyperPCTL* 公式的可满足性所需的样本数量方面都表现得更好。
2022-09-06 cs.AI cs.LO cs.MA
Reasoning about Strategies: on the Satisfiability Problem
策略逻辑（Strategy Logic，简称SL）是由Mogavero、Murano和Vardi提出的一种有用的形式主义，用于在多智能体并发游戏中明确地推理策略（作为一阶对象）。这种逻辑被证明是非常强大的，包含了所有主要的先前研究的模态逻辑的战略推理，包括ATL，ATL* 等。不幸的是，由于其高表达性，SL具有非基本可判定的模型检查问题，并且可满足性问题是不可判定的，特别是Sigma_1^1。为了得到一个可判定的子逻辑，本文引入并研究了单目标策略逻辑（SL[1G]，简称SL[1G]）。这是SL的一个语法片段，严格地包含ATL*，它包含了前束范式中的公式，每次有一个单一的时间目标，对于每个策略量化的代理。我们证明了SL[1G]与SL不同，SL[1G]具有有界树模型性质，并且它的可满足性问题在2ExpTime中是可判定的，因此并不比ATL* 的可满足性问题难.
2017-03-16 cs.LO
