Deciding Asynchronous Hyperproperties for Recursive Programs
本文提出一种带新机制识别迹位置的异步超性质逻辑，在保持有限状态模型检测复杂度不变且更具表达力的同时，首次为递归程序超性质模型检测提供了合适方法。
2023-10-25 cs.FL cs.LO cs.PL
The Complexity of Asynchronous HyperLTL
Aalborg University（奥尔堡大学）
本文研究了异步超属性逻辑AHLTL的模型检测和可满足性问题，证明了模型检测等价于二阶算术真值，而可满足性在轨迹存在量化时为Σ₁¹-完全，在轨迹全称量化时为Σ₁¹-困难且属于Σ₂¹。
2026-10-11 cs.LO
Monitoring Hyperproperties
超属性，如非干扰性和观察确定性，将多个系统执行相互关联。它们不能用标准的时态逻辑（如LTL、CTL和CTL*）来表示，因此不能用标准的运行时验证技术来监视。HyperLTL扩展了线性时间时态逻辑（LTL），在迹上显式量化，以表达Hyperproperties。我们研究了HyperLTL公式在三种不同输入模型下的运行时验证问题：（1）并行模型，其中并行处理固定数量的系统执行。(2)无限顺序模型，其中系统执行是顺序处理的，每次一个执行。在这个模型中，传入执行的数量可能会永远增长。(3)有界顺序模型，其中跟踪按顺序处理，传入执行的数量是有界的。我们证明了对于输入模型（1）和（3），决定HyperLTL公式的可监控性是PSPACE完全的。对于输入模型（2）中的无替代HyperLTL公式，判定可监控性是PSPACE完全的。对于每个输入模型，我们都提供了实用的监控算法。我们还提出了各种优化技术。通过识别规范的属性，如自反性，对称性和传递性，我们减少了跟踪之间的比较次数。对于顺序模型，我们提出了一种技术，最大限度地减少了需要存储的痕迹的数量。最后，我们提供了一个优化，简洁地表示存储的痕迹共享共同的前缀。我们评估了我们的优化，表明这会导致更可扩展的监控，特别是显着降低内存消耗。
2018-07-02 cs.LO
Deciding branching hyperproperties for real time systems
本文研究实时系统分支超性质的判定问题，提出度量时序逻辑的分支超性质扩展HCMTL*，证明其在时间自动机上的验证不可判定，限定固定时间范围时可通过归约为有界实数域MSO问题实现可判定。
2024-05-20 cs.CR cs.LO
Deciding the Satisfiability of MITL Specifications
在本文中，我们提出了一个可满足性保持减少MITL解释有限变量连续行为的约束LTL时钟，CLTL的一个变种，是可判定的，并为一个SMT为基础的有界可满足性检查。其结果是一个新的完整的和有效的决策程序的MITL。虽然MITL的决策程序已经存在，他们采用的自动机为基础的技术似乎是很难实现在实践中，而且，据我们所知，目前还没有实现它们。一个原型工具MITL的基础上的编码在这里提出的，而不是，已经实施，并公开提供。
2013-07-17 cs.LO
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated
本文引入了一个新的一阶逻辑等式可判定片段，它严格地推广了两个已知的一阶逻辑等式可判定片段--Bernays-Schönfinkel-Ramsey（BSR）片段和Monadic片段.定义原则是在原子水平上将普遍量化的变量与存在量化的变量句法分离。因此，我们的分类既不依赖于对量词前缀的限制（如在BSR的情况下），也不依赖于对谓词符号的arity的限制（如在一元的情况下）。我们证明了新的片段表现出有限模型的属性，并推导出一个非小学的计算时间上界所需的决定在新的片段满足。对于量词前缀为$\exists^* \forall^* \exists^*$的前趋句的子片段，可满足性问题被证明是NEXPTIME完备的。最后，我们讨论了如何自动推理程序可以利用我们的结果。
2016-06-20 cs.LO
Team Semantics for the Specification and Verification of Hyperproperties
我们开发团队语义的线性时序逻辑（LTL）来表达hyperproperties，这是最近被确定为一个关键的概念，在信息流属性的验证。从概念上讲，我们认为一个异步和同步的团队语义的变体。我们研究了这种新逻辑的基本性质，并对其可满足性、路径和模型检验问题的计算复杂性进行了分类。此外，我们将研究这些基本逻辑的扩展如何对添加其他原子运算符做出反应。最后，我们比较它的表现力的HyperLTL，另一个最近推出的逻辑hyperproperties。我们的研究结果表明，团队语义下的LTL是一个可行的替代HyperLTL，它补充了HyperLTL的表达能力，并具有部分更好的算法性能。
2018-06-25 cs.CC cs.LO
Propositional Dynamic Logic for Hyperproperties
反应式系统的信息安全属性（如非干扰性）通常需要将系统的不同执行相互关联并同时遵循它们。这样的超性质在其他上下文中也可以是有用的，例如，当分析分布式系统的属性时，如线性化。由于LTL、CTL或模态μ演算等常见逻辑无法表达超性质，因此开发了超逻辑HyperLTL和HyperCTL* 来解决这个缺陷。然而，这些逻辑不能表达任意的Ω-正则性质。在本文中，我们介绍HyperPDL-三角洲，一个适应的命题动态逻辑的Fischer和Ladner的hyperproperties，为了消除这一限制。使用一个优雅的自动机理论框架，我们表明，HyperPDL-三角洲模型检验是渐近不更昂贵的HyperCTL* 模型检验，尽管它大大增加了表达能力。我们进一步研究片段的HyperPDL-三角洲方面的可满足性检查。
2020-07-17 cs.FL cs.LO
Efficient Loop Conditions for Bounded Model Checking Hyperproperties
有界模型检验（BMC）是一种通过增量式地探索系统状态空间来发现缺陷的有效技术。为了通过有限的结构推理无限的轨迹并最终获得完整性，BMC结合了重新访问先前观察到的状态的循环条件。本文着重于开发循环条件BMC的HyperLTL-时间逻辑的hyperproperties，允许表达重要的政策，在并发系统的安全性和一致性，等等。循环条件HyperLTL比LTL更复杂，因为不同的轨迹可能会不一致地在不相关的时刻循环。HyperLTL的现有BMC方法仅考虑线性展开，而没有任何循环能力，这排除了找到小的无限迹线和获得完整的技术。我们调查循环条件HyperLTL BMC，其中HyperLTL公式可以包含多达一个量词交替。我们首先提出了一个一般的完全自动机为基础的技术，这是基于最大展开的界限。然后，我们引入替代的基于模拟的算法，允许有效地利用短循环，生成SAT查询，其满足性保证了原始模型检验问题的结果。我们还报告了使用Z3 py的BMC技术的原型实现的经验评估。
2023-01-26 cs.LO
Tableau-based procedure for deciding satisfiability in the full coalitional multiagent epistemic logic
我们研究了多智能体认知逻辑CMAELCD与运营商的共同和分布式知识的所有联盟的代理。我们引入Hintikka结构的逻辑，并证明了在这样的结构中的可满足性是等同于在标准模型中的可满足性。利用这一结果，我们设计了一个增量式的基于表的决策过程中测试CMAELCD的可满足性。
2009-02-12 cs.LO cs.MA
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
Realizing Omega-regular Hyperproperties
研究了超逻辑HyperQPTL，它结合了迹关系和$ω$ -正则性的概念.我们证明了HyperQPTL是非常有表现力的，它可以表达诸如不确定性，有界等待授权，认知属性，特别是任何$ω$ -正则属性等属性。这些属性在以前研究过的超逻辑（如HyperLTL）中无法表达。与此同时，我们认为，HyperQPTL的表现力是最佳的，在某种意义上，一个更有表现力的逻辑$ω$ -正则超属性将有一个不可判定的模型检验问题。我们进一步研究了HyperQPTL的可实现性问题。我们证明了可实现性对于包含像不确定性这样的属性的HyperQPTL片段是可判定的。但是，与可满足性问题相比，命题量化确实使超逻辑的可实现性问题更难。更具体地说，具有泛存在命题量词交替后跟单个迹量词的HyperQPTL公式片段通常是不可判定的，即使片段到HyperLTL的投影具有可判定的可实现性问题。最后，我们在原型工具BoSy中实现了HyperQPTL的有界综合问题。使用带有HyperQPTL规范的BoSy，我们已经能够合成几个资源仲裁器。非线性时间超逻辑的综合问题仍然是一个未解决的问题。例如，还不知道如何从分支时间超逻辑（如HyperCTL $^*$）中给出的规范合成系统。
2021-01-18 cs.LO
The Hierarchy of Hyperlogics
超性质通过将多个迹联系起来来推广迹的性质，在信息流安全中得到了广泛的研究。最近，已经提出了一些超性质的逻辑，并且需要理解它们的可判定性和相对表达性。新的逻辑已经从标准逻辑中获得了两个主要的扩展：时态逻辑，如LTL和CTL $^*$，已经通过为迹或路径添加变量而被推广到超属性。一阶逻辑和二阶逻辑，如一元一阶序逻辑和MSO，已经用等阶谓词扩展。我们研究了两个扩展的线性时间和分支时间逻辑的频谱的影响，特别是对命题的量化逻辑。由此产生的超逻辑层次结构与经典层次结构有很大不同，这表明等级别谓词比跟踪和路径变量增加了更多的表达能力。在超逻辑的层次结构中，我们确定了可满足性问题的可判定性的新边界。具体来说，我们表明，虽然HyperQPTL和HyperCTL $^*$都是不可判定的一般，公式内的$\exists^*\forall^*$片段是可判定的。
2020-05-12 cs.LO
Hyperproperty Verification as CHC Satisfiability
本文提出将∀ᵏ∃ˡ超属性验证问题归约为约束 Horn 子句可满足性问题，通过整合对齐与归纳不变式推断、结合博弈语义下的见证函数推断，实现超属性的可靠完备验证。
2024-01-31 cs.LO
The Complexity of Generalized HyperLTL with Stuttering and Contexts
本文确定了带 stuttering 和 contexts 的广义 HyperLTL 的可满足性与模型检测复杂度，证明可满足性为 $Σ_1^1$-完全，而模型检测等价于二阶算术真值且远难于 HyperLTL。
2025-09-17 cs.FL cs.LO
An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability
提出了一种基于表格的命题动态逻辑可满足性判定算法，该算法建立一个具有祖先循环的有限根树，并在回溯过程中将子循环的额外信息传递给父循环，以区分好循环和坏循环.它很容易实现，具有并行化的潜力，因为它通过独立地探索每个tableau分支来构建一个伪模型。但它的最坏情况行为是2EXPTIME而不是EXPTIME。TWB（http：//www.example.com）中的原型实现是可用的。twb.rsise.anu.edu.au
2008-01-08 cs.LO
Bounded Variability of Metric Temporal Logic
以前的工作表明，推理与实时时序逻辑往往是简单的限制模型与有界的变化-其中不超过v事件可能会发生每V个时间单位，对于给定的v，V.推理公式与内在的有界的变化，可以采用更简单的技术，依赖于有界的变化，而不损失任何的一般性。那么，在算法上决定哪些公式具有内在的有限可变性的复杂性是什么呢？在本文中，我们研究的问题，参照度量时态逻辑（MTL）。我们证明了在稠密时间模型上，MTL公式的有界可变性是不可判定的，但其不可判定度低于一般稠密时间MTL可满足性。相反，在离散时间模型上，确定MTL有界可变性具有与可满足性相同的指数空间复杂度。为了补充这些负面的结果，我们还简要地讨论了小片段的MTL，更适合推理有界变异。
2014-07-04 cs.LO
Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
提出了一种确定实数上非线性多项式约束合取可满足性的新算法，该算法可作为非线性实数算术可满足性模理论（SMT）求解的理论求解器.该算法是适应于可满足性的柱形代数分解（CAD）的变体，其中解候选者（样本点）被增量地构造，直到找到满意的样本或者已经采样了足够的样本以得出不可满足性的结论。样本的选择由输入约束和先前的冲突指导。我们的新方法背后的关键思想是从部分样本开始;证明它不能扩展到完整样本;并从排除部分样本周围的更大空间的原因中，逐步建立成空间的圆柱代数覆盖。有相似之处的增量变化的CAD，NLSAT方法的Jovanovic和de Escha，和NuCAD算法的布朗，但我们目前的工作示例和实验结果的初步实施，以证明这些差异，和新方法的好处。
2020-11-23 cs.LO cs.SC
Bit-Precise CHC Satisfiability Using Theory-Modular Reasoning
Technion - Israel Institute of Technology（以色列理工学院）
本文提出理论模块化框架 Mosaic，结合位向量理论与整数算术理论推理判定约束 Horn 子句可满足性，其原型在比特操作基准上的性能显著优于 Spacer。
2026-08-07 cs.LO cs.PL
Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection
School of Mathematical Sciences, Peking University（北京大学数学科学学院）；Peking University（北京大学）
提出了一种判定实数上多项式公式可满足性的新算法。该算法的关键是一个新的投影算子，称为样本单元投影算子，定制的搜索驱动子句学习（CDCL）风格的搜索。虽然新算子也是CAD（柱形代数分解）类投影算子，其计算包含给定样本的单元（不一定是圆柱的），使得来自问题的每个多项式在单元上是符号不变的，但是它具有单指数时间复杂度。样本细胞投影算子可以有效地引导CDCL风格的搜索远离冲突状态。实验证明了新算法的有效性。
2020-03-04 cs.AI cs.LO cs.SC
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
给定一个无量词的Presburger算术公式，如果它有一个令人满意的解，则存在一个其大小（以比特为单位）在公式的大小上多项式有界的解。本文考虑一类特殊的无量词Presburger公式，其中大部分线性约束是差分（分离）约束，而非差分约束是稀疏的.据观察，此类事件通常发生在软件验证中。除了传统的公式大小的措施，我们推导出一个新的解决方案的范围内的参数表征的稀疏性的线性约束和非差约束的数量。特别是，我们表明，每个整数变量所需的位数是线性的非差约束的数量和对数的非零系数的数量和大小，但在其他方面是独立的线性约束的总数在公式中。导出的界限可以用于基于在有限域上实例化整数变量并将输入的无量词Presburger公式转换为等可满足的布尔公式的决策过程中，然后使用布尔可满足性求解器来检查。除了我们的主要理论结果，我们讨论了在实践中获得更严格的界限的几个优化。经验证据表明，我们的决策程序可以大大优于其他决策程序。
2008-10-07 cs.LO
On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoding
本文研究了在二进制编码位宽和常数的固定位向量理论上判定一阶量化公式可满足性的精确计算复杂性。这个问题是在EXPSPACE中的，并且是NEXPTIME困难的。我们表明，这个问题是完整的复杂性类AEXP（聚）-类的问题可判定的交替图灵机使用指数时间，但只有多项式数量的存在和普遍的状态之间的交替。
2018-05-02 cs.LO
A Faster Tableau for CTL*
最近有几个关于tableau系统的建议，用于确定在实际重要的分支时间时态逻辑（称为CTL*）中的可满足性。在本文中，我们提出了一个简化的和更传统的tableau方法建立在作者的早期理论工作。证明了结果的可靠性和完备性。一个原型的实施表明，显着提高性能的新方法的测试公式的范围。我们还看到，它比较有利的最先进的，游戏和自动机为基础的决策程序。
2013-07-17 cs.LO
Implicant based parallel all solution solver for Boolean satisfiability
本文发展了一种并行计算求解器，用于计算由多元布尔函数定义的布尔方程组的所有满意赋值。虽然有我们已知的CNF形式的布尔公式的可满足性的求解器，但这些主要是为了确定公式的可满足性而设计的，并且没有解决找到所有满意解的问题。而可满足性问题的并行求解器的开发仍然是计算机科学尚未完成的课题。本文提出的求解器旨在用并行算法表示布尔公式的所有解，即使没有CNF形式。将所提出的算法应用于布尔函数的代数范式（ANF）。该算法的基本思想是用布尔函数的一组完整的蕴涵式来表示满足的赋值，这些蕴涵式作为布尔公式的因子。该算法主要在公式的因子稀疏（即具有变量总数的一小部分）的情况下有效。这允许一次一个地计算单个因子的一组完整的蕴涵式，并在每一步减少公式。本文还提出了一个求ANF中函数正交蕴涵的完备集的算法。该算法的一个优点是所有的解都可以用蕴涵式来表示。最后，由于在每一步的小和分布式计算，以及在独立的线程计算，本文提出的求解器预计将是有用的开发一个良好的可扩展性的并行求解器的大规模问题的布尔可满足性在大量的处理器。
2017-02-06 cs.DS cs.LO
EUF$^n$: A Decidable Extension to the Theory of Equality with Uninterpreted Functions
State Key Laboratory of Complex & Critical Software Environment, National University of Defense Technology（国防科技大学复杂与关键软件环境国家重点实验室）
本研究提出带参数化组合深度的EUFⁿ理论，通过条件同余图算法证明其可判定性，可用于解决交错Dyck可达性及未解释程序验证的相关问题。
2026-08-25 cs.LO cs.PL
Flavors of Quantifiers in Hyperlogics
本文扩展超迹逻辑，引入约束与无约束两类迹量词，研究其不同模式对可满足性判定性的影响，证明若干片段等价于S1S或HyperQPTL，并给出新的可判定与不可判定结果。
2025-10-14 cs.FL cs.LO
