Extending Two-Variable Logic on Trees
最近证明了在树上解释的一阶逻辑的两个变量片段的有限可满足性问题是ExpSpace完备的。我们考虑这个逻辑的两个扩展。我们发现，添加额外的二进制符号或计数量词的逻辑不影响有限可满足性问题的复杂性。然而，结合两个扩展并添加二进制符号和计数量词会导致这种复杂性的爆炸。我们还比较了两个变量的片段的表达能力，其扩展与计数量词的树木。事实证明，这两种逻辑具有同样的表达能力，尽管在无序树的限制情况下，计数量词确实增加了表达能力。
2016-11-24 cs.LO
Trees over Infinite Structures and Path Logics with Synchronization
我们提供了无限树结构的模型检测问题的可判定性和不可判定性的结果。这些树结构由无限关系结构的元素序列构建。更准确地说，我们处理的关系结构M的树迭代在Shelah-Stupp的意义。与经典的MSO逻辑模型检验可判定的结果相反，我们证明了只允许路径量词和链量词的逻辑树模型检验问题的可判定性（其中链是路径的子集），因为它们出现在分支时间逻辑中;然而，同时树被等层关系丰富（如果顶点u、v在相同的树层上，则在顶点u、v之间保持）。我们将树逻辑与用于表达底层结构M的属性的逻辑干净地分离。我们说明的范围内的可判定性的结果表明，两个轻微的扩展框架导致不可判定性。特别地，这适用于Muchnik-Walukiewicz意义上的（更强的）树迭代。
2011-11-14 cs.LO
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
A Tree Logic with Graded Paths and Nominals
正则树文法和正则路径表达式构成了程序设计语言和类型系统中广泛使用的核心构造。然而，到目前为止，很少有研究的推理框架的路径表达式中的节点基数约束发生沿路径在一棵树。我们提出了一个逻辑能够表达沿路径，其中可能包括任意递归向前和向后导航的深度计数。计数扩展可以被看作是对直接后继节点进行计数的分级模态的推广。虽然组合的分级模态，名义上，和逆模态产生不可判定的逻辑图，我们表明，这些功能可以结合在一个树逻辑判定指数时间。
2010-05-31 cs.LO
Two-Way Unary Temporal Logic over Trees
我们考虑一个无秩、无序的有限树的时态逻辑EF+F^-1。该逻辑有两个运算符：EF，表示“在某些适当的后代继承中”，F^-1，表示“在某些适当的祖先继承中”。我们提出了一个算法，用于判定一个无秩有限树的正则语言是否可以用EF+F^-1表示。该算法使用的表征表示的森林代数。
2009-08-05 cs.LO
A Proof Tree Builder for Sequent Calculus and Hoare Logic
我们已经开发了一个基于Web的教学证明助手，证明树生成器，它可以让你从最初的目标向上应用规则在微积分和霍尔逻辑的一个简单的命令式语言。我们配备了一个基本的证明自动化功能和Z3集成我们的工具。普林斯顿大学自动推理课程的学生使用了我们的工具，并发现它很直观。证明树生成器可在https://proof-tree-builder.github.io上在线获得。
2023-03-10 cs.LO
Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees
在这项工作中，我们开发了一个广义的Hennessy-Milner逻辑（HML）的广义同步树（GST），我们称之为广义Hennessy Milner逻辑（GHML）。重要的是，这种逻辑表明GST的（弱）互模拟与同步树（ST）的普通互模拟之间存在很强的关系。我们证明，这种关系可以用来定义GST模拟ST的图像有限性。此外，我们证明了某些最大的Hennessy-Milner类的ST有对应的最大的Hennessy-Milner类的GST的GST弱互模拟。我们还表现出一些有趣的特性，这些最大的Hennessy-Milner类的GST。
2017-09-04 cs.LO
The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic are Highly Undecidable
本文证明了概率计算树逻辑（PCTL）的可满足性与有效性问题均高度不可判定，超出了算术层级，因此该逻辑不存在可靠且完备的演绎系统。
2025-04-30 cs.LO
Automata for Enriched Trees and Applications
该研究针对带附加结构的富集树提出一族自动机模型，证明其与不动点逻辑等价，实现单二阶逻辑多变体的刻画，并简化Muchnik定理证明、推导其在其他逻辑下的变体。
2025-02-21 cs.LO
Extended Computation Tree Logic
我们介绍了一个通用的扩展流行的分支时间逻辑CTL细化的时间，直到和释放操作符与形式语言。例如，语言可以确定沿着路径的时刻，直到属性可以被满足。我们考虑几类语言导致逻辑具有不同的表达能力和复杂性，其重要性是出于他们的使用模型检验，合成，抽象解释等，我们表明，即使上下文无关的语言，直到操作逻辑仍然允许多项式时间模型检查，尽管显着增加的表达能力。这使得该逻辑在验证中的应用成为一个有希望的候选者。此外，我们分析了可满足性的复杂性，并比较了这些逻辑的表达能力CTL* 和PDL的扩展。
2010-06-18 cs.LO
Deciding Entailments in Inductive Separation Logic with Tree Automata
具有归纳定义的分离逻辑（SL）是用于指定复杂递归数据结构的自然形式主义，用于操作此类结构的程序的组合验证。任何基于SL的自动验证过程的关键要素是蕴涵问题的可判定性。在这项工作中，我们减少了蕴涵问题的一个非平凡的子集SL描述树（和超越）的语言包含树自动机（TA）。我们的减少提供了严格的复杂性界限的问题，并表明在我们的片段的蕴涵是EXPTIME完成。出于实用的目的，我们利用自动机理论的最新进展，如包含检查非确定性TA避免明确的确定性。我们实现了我们的方法，并提出了有前途的初步实验结果。
2014-02-11 cs.LO
Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?
本文研究树语义下带命题量词的模态与时态逻辑的复杂性，证明限制于EX的tQCTL已是Tower困难，并在N有界树上为AExpPol完全，同时推广到多种模态逻辑。
2022-08-04 cs.LO
Sequent Calculus in the Topos of Trees
中野的“后来”模态，受到哥德尔-洛布可证明性逻辑的启发，已被应用于类型系统和程序逻辑中，以捕获保护递归。Birkedal等人通过树的拓扑的内部逻辑来模拟这种模态。我们证明了该逻辑的命题片段的语义可以由线性逆良基直觉Kripke框架给出，因此该逻辑是直觉模态逻辑KM和中间逻辑LC的结合。因此，我们称这种逻辑为$\mathrm{KM}_{\mathrm{lin}}$。通过将蕴涵分解为静态蕴涵和非自反蕴涵的策略，给出了$\mathrm{KM}_{\mathrm{lin}}$的一个可靠的无割完备蕴涵演算。我们的演算提供了确定性和终止向后证明搜索，产生的逻辑和其有效性问题的coNP-完全性的可判定性。我们的演算和决策过程可以被限制为降低线性，从而捕获KM。
2015-04-17 cs.LO
Structural Resolution for Logic Programming
我们介绍了一个三层树演算（3 TC），定义了一个系统的方式，在逻辑编程中的证明搜索的三层树结构。我们使用3 TC来定义一个新的-结构化-版本的解决逻辑编程。
2015-07-21 cs.LO
Automata for two-variable logic over trees with ordered data values
数据树是其中每个节点除了携带来自有限字母表的标签之外，还携带来自无限域的数据值的树。它们已被用作{XML}推理任务和验证的抽象模型。然而，大多数现有的方法考虑的情况下，只有平等测试可以对数据值进行。本文研究了数据值来自线性有序域的数据树，除了相等性检验外，还可以检验一个节点上的数据值是否大于另一个节点上的数据值。我们引入了一个自动机模型，我们称之为有序数据树自动机（ODTA），提供了它的逻辑特征，并证明了它的非空性问题是可判定的3-NEXPTIME。我们还表明，两个变量逻辑上的无秩树，研究Bojanczyk，Muscholl，Schwentik和Segoufin在2009年，正好对应于一个特殊的子类，这个自动机模型。然后，我们定义了一个稍微弱的版本的ODTA，我们称之为弱ODTA，并提供其逻辑特性。非空性问题的复杂性下降到NP。然而，一些现有的形式主义和模型的研究文献中可以捕获已经弱ODTA。我们还表明，ODTA的定义可以很容易地修改，的情况下，数据值来自一个树状偏序域，如字符串。
2013-10-04 cs.LO
A Constructive Equivalence between Computation Tree Logic and Failure Trace Testing
形式化验证的两个主要系统是模型检验和基于代数模型的测试。模型检验基于某种形式的时态逻辑，例如线性时态逻辑（LTL）或计算树逻辑（CTL）。CTL是一种强大而现实的逻辑，它能够表达进程的最有趣的属性，如活性和安全性。基于模型的测试基于进程的某些操作语义（例如跟踪、故障或两者）及其关联的前序。除了互模拟之外，最细粒度的前序（主要是理论上的重要性）是基于故障跟踪的。我们表明，这两个最强大的变种是等价的，也就是说，我们表明，对于任何故障跟踪测试存在一个CTL公式相当于它，反之亦然。我们所有的证明都是构造性的和算法性的。我们的结果允许一个大系统的部分被指定为逻辑，而其他部分被指定为代数，从而结合了最好的两个（逻辑和代数）的世界。
2019-01-30 cs.LO
Monadic Second-Order Logic with Path-Measure Quantifier is Undecidable
证明了用定性路测度量词扩充的无限二叉树的一元二阶逻辑（MSO）理论是不可判定的。这个量词表示树中满足某个公式的无限路径的集合具有勒贝格测度1。为此，我们证明了定性泛奇偶树自动机的空性问题是不可判定的。定性的意思是如果一个树自动机的运行中满足接受条件的路径集合具有勒贝格测度1，则该运行是接受的。
2019-02-15 cs.LO
Global Numerical Constraints on Trees
我们引入了一个逻辑基础的原因树结构上的节点出现的数量的限制。相关的形式主义仅限于表达特定树区域上的出现约束，例如给定节点的子节点。相比之下，在本工作中引入的逻辑可以简洁地表示任何区域，后代或祖先的数值界限。我们证明了即使数值约束是二进制形式的逻辑在单指数时间内也是可判定的。我们还说明了使用的逻辑在描述的数值约束的多方向路径查询XML文档。此外，对正则语言（XML模式）的数值限制也可以通过该逻辑简明地描述。这意味着可判定计数扩展的XML查询和XML模式的表征。此外，由于该逻辑在否定下是封闭的，因此可以用作检验空性、包容性和等价性的最佳推理框架。
2014-06-13 cs.LO
Monadic second order finite satisfiability and unbounded tree-width
Seese（1991）的经典结果证明了一元二阶逻辑的有限可满足性问题只能在有界树宽的结构类上判定。本文证明了以下问题是可判定的：输入：（i）一元二阶逻辑语句$α$，（ii）一个语句$β$，该语句在一阶逻辑的两变量片段中扩展为计数量词. $α$和$β$的词汇表可以相交。输出量：是否存在满足$α\landβ$的有限结构，使得该结构对$α$的词汇表的限制具有有界树宽？(The所需结构的树宽度不受限制）。因此，我们证明了可满足性问题的可判定性的有限结构的有界树宽度的逻辑扩展一元二阶逻辑的线性基数约束的形式$|X_{1}|+\cdots+|X_{r}|<|Y_{1}|+\cdots+|Y_{s}|$，其中$X_{i}$和$Y_{j}$是一元二阶变量。我们证明了WS1S的一个类似的扩展的可判定性。
2016-04-16 cs.LO
A Proof System for a Logic of Presuppositions
本文提出了一个由P. F.斯特劳森它基于M.理查德·迪亚兹1981年在另一篇论文中，我概述了基于真值树的t相关逻辑的推导系统。结论是重言式是真值相关的当且仅当一棵树中的所有变量都是自矛盾的。一棵树可能在所有变量都不自相矛盾的情况下终止。在这种情况下，相关公式仍然是重言式，但不是真值相关重言式。这个概念被扩展到谓词演算，即一种预设逻辑或其变体。
2023-01-19 cs.LO
Multiplicative-Additive Proof Equivalence is Logspace-complete, via Binary Decision Trees
给定一个逻辑中提出的微积分，一个自然的问题是证明的等价性：以确定是否两个给定的证明是等同的任何指称语义，即任何类别的解释逻辑兼容其削减消除程序。这个概念通常可以通过一组规则排列在语法上捕获。非常一般地，证明网可以被定义为提供证明的等价类的规范表示的组合对象。特别地，逻辑的证明网的存在性提供了该逻辑的等价性问题的解决方案。在线性逻辑的某些片段中，可以给出具有良好计算性质的证明网的概念，使其成为研究割消过程的证明的合适表示。最近已经证明，对于线性逻辑的乘法（有单位）片段，不可能有这样一个证明网的概念，因为这个逻辑的等价问题是P空间完全的。研究线性逻辑中的乘加（无单位）片段，发现它与二进制决策树密切相关：建立了基于二进制决策树的证明表示，将证明等价约化为决策树等价，并给出了二进制决策树的逆编码作为证明.作为我们的主要结果，我们得到的证明等价问题的研究片段的复杂性是对数空间完全的。
2017-11-28 cs.LO
A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning
本文提出了一种基于逻辑演算的证明方法，结合归纳定义的谓词表示的有界树宽结构和理论推理，检验分离逻辑公式之间蕴涵的有效性。微积分是可靠的和完备的，在这个意义上，证明树是有效的当且仅当它允许一个（可能是无限的）证明树。我们表明，该过程在以下两种情况下终止：（i）当归纳规则，定义谓词发生在左手边的蕴涵终止，在这种情况下，证明树总是有限的。(ii)当理论是空的，在这种情况下，每个有效的证明树都允许一个有理证明树，其中在证明树中出现的成对不同序列的总数是关于r.t.的双指数。最后的结局。
2022-06-22 cs.LO
A Functional (Monadic) Second-Order Theory of Infinite Trees
本文为无限树上的MSO逻辑提出完全公理化，通过扩展为FSO逻辑并利用奇偶博弈决定性，给出拉宾树定理的证明。
2020-10-22 cs.LO
Continuation Semantics for Fixpoint Modal Logic and Computation Tree Logics
Kyoto University（京都大学）；University of Southampton（南安普顿大学）
本文提出延续语义用于固定点模态逻辑和计算树逻辑，证明其与合取语义等价，并重新定义了 CTL* 的模型结构。
2026-02-27 cs.LO
Definability and Interpolation within Decidable Fixpoint Logics
本文研究可判定不动点逻辑中的可定义性刻画，通过精细分析树模型性质并改进关系逻辑与树逻辑间的转换方法，提供语义及有效刻画。
2019-09-09 cs.LO
The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations
针对一阶逻辑中树宽有界性问题不可判定的情况，本文研究了关系签名上推广的Separation Logic，提出了该逻辑下树宽有界性问题的求解算法。
2024-05-17 cs.FL cs.LO
Controlling the Depth, Size, and Number of Subtrees for Two-variable Logic on Trees
具有两个变量FO2的一阶逻辑的性质的验证已经在许多上下文中进行了研究。在任意结构上，它是可判定的，具有NEXPTIME复杂度，可满足的公式具有指数大小的模型。在单词结构上，FO2被认为具有与一元时态逻辑相同的表达能力，同样的属性也成立。有限标记有序树上的FO2也很有趣：它与XML文档的通用查询语言navigational XML具有相同的表达能力。先前的工作对FO2和FO2给出了FO2的可满足性的2EXPTIME界。在这项工作中，我们第一次深入研究了树上FO2的复杂性，以及模型的大小和深度。我们表明，双指数界是不紧的，也没有NEXPTIME完整性的结果，从字的情况下结转：确切的复杂性取决于所使用的词汇，存在或不存在的模式，以及用于标签的编码。我们的研究结果依赖于分析的子公式类型的模型FO2公式，包括技术控制不同的子树的数量，深度和规模的证人有限满足FO2句子树。
2013-05-30 cs.LO
Logics for Unranked Trees: An Overview
标记未排序树被用作XML文档的模型，在过去的几年里，它们的逻辑语言已经得到了积极的研究。这样的逻辑有不同的目的：有些更适合于提取数据，有些用于表达导航属性，有些则可以轻松地将树的复杂属性与这些属性的树自动机的存在性联系起来。此外，逻辑在它们的模型检查属性、它们的自动机模型以及它们在有序树和无序树上的行为上有显著的不同。在本文中，我们提出了一个调查的逻辑无秩树。
2006-07-26 cs.DB cs.LO
A traditional tree-style tableau for LTL
命题线性时态逻辑（Propositional Linear Time Temporal Logic，LTL）是一种面向计算应用的标准时态逻辑，许多推理技术和工具已经被开发出来。然而，这种逻辑的tableaux看起来不像传统的树形tableau系统，它们的处理通常非常复杂。我们提出了一个新的简单的传统风格的树形画面LTL，并证明它是健全的和完整的。除了易于理解，向学生介绍和手动使用外，它似乎也易于实现，并有望在自动化方面具有竞争力。它特别适合于并行实现。
2016-04-13 cs.LO
On the Expressiveness of a Logic of Separated Relations
我们比较模型理论的表达性的存在片段的分离逻辑在不受限制的关系签名（SLR）-只有分离的连接作为逻辑连接和高阶归纳定义，传统上称为符号堆片段-与（一元）二阶逻辑（（M）SO）的表达性。虽然SLR和MSO在无限树宽的结构上是不可比的，但事实证明，SLR可以嵌入SO中，一般来说，当模型的树宽由作为输入的参数限制时，MSO成为SLR的严格子集。我们还讨论了定义一个片段的SLR，相当于MSO模型的有界树宽的问题。这样的片段，然后将成为最一般的分离逻辑与可判定的蕴涵问题，一个关键成分的实际验证方法的自适应（可重构）组件为基础的和分布式系统。
2022-08-02 cs.LO
Robust Computation Tree Logic
针对分支时间逻辑缺乏鲁棒语义的问题，提出采用多值语义的 rCTL 与 rCTL*，在保持或增强表达能力的同时，使模型检测、可满足性和综合复杂度不增加。
2023-10-24 cs.LO
On the Parameterized Intractability of Monadic Second-Order Logic
Courcelle的一个著名结果是：如果C是一类有界树宽的图，则一元二阶逻辑（MSO_2）的模型检验是C上的固定参数线性时间参数化算法可处理的（fpt），其中参数是树宽加上公式的大小。一个直接的问题是，这是否是最好的，或者结果是否可以扩展到无限树宽的类。在本文中，我们表明，在树的宽度，定理不能进一步推广。更具体地说，我们证明了，如果C是一类图，这是封闭的着色，并满足一定的构造性条件，是这样的树宽度不受\log^{84} n，那么MSO_2-模型检验不是FPT，除非SAT可以解决在次指数时间。如果C的树宽不是多项式有界的，则MSO_2-模型检验不是fpt，除非多项式时间层次中的所有问题都能在次指数时间内求解。
2012-03-23 cs.LO
The Tree Width of Separation Logic with Recursive Definitions
分离逻辑是一种广泛使用的形式主义，用于描述动态分配的链接数据结构，如列表，树等的逻辑的各个片段的可判定性状态构成了一个长期存在的开放问题。目前的结果报告的技术，以确定满足性和有效性的蕴涵分离逻辑（S）的列表（可能与数据）。在本文中，我们建立了一个更一般的可判定性结果。我们证明了任何使用较一般的递归定义谓词的分离逻辑公式都是可判定的可满足性，而且这些公式之间的蕴涵也是可判定的有效性.这些谓词足够通用，可以定义（双）链表、树和比树更通用的结构，比如叶子被链接在一个链表中的树。可判定性证明是通过将一元二阶逻辑在有界树宽度的图上的可判定性归约来实现的。
2013-03-30 cs.FL cs.LO
Automata-Theoretic Characterisations of Branching-Time Temporal Logics
本文通过识别Hesitant Tree Automata的两个变体，为任意分支树上的CTL*和ECTL*等分支时间时序逻辑提供了自动机理论刻画，解决了悬而未决四十年的开放问题。
2024-04-29 cs.LO
PFL: a Probabilistic Logic for Fault Trees
针对故障树结构化查询分析研究不足的问题，本文提出概率故障树逻辑PFL及领域特定语言LangPFL，扩展布尔故障树推理逻辑BFL，支持含概率的故障树属性规范，并基于BDD给出相关理论与模型检测算法，通过COVID-19相关及油气管道故障树验证了有效性。
2025-08-04 cs.LO
Formalization of Fault Trees in Higher-order Logic: A Deep Embedding Approach
故障树（FT）是一种标准的故障建模技术，已被广泛用于预测许多复杂工程系统的可靠性，可用性和安全性。为了便于形式化分析FT的分析，最近提出了一种高阶逻辑形式化的FT。然而，这种形式化在处理大型系统和将FT模型转换成其相应的可靠性框图（RBD）结构方面是相当有限的，即，在可靠性和可用性分析中经常使用的转换。为了克服这些限制，我们提出了一个基于深度嵌入的形式化的FT。特别地，本文提出了AND、OR和NOT FT门的形式化，这些FT门又用于形式化其他常用的FT门，即，与非、或非、异或、抑制、比较器和多数表决等方法，并对其失效概率表达式进行了形式化验证。为了说明的目的，我们提出了一个正式的故障分析的通信网关软件的下一代空中交通管理系统。
2016-08-23 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
Succinctness of Order-Invariant Logics on Depth-Bounded Structures
研究了一阶逻辑和一元二阶逻辑的序不变句在有界树深结构上的表达能力和简洁性。一般来说，顺序不变是不可判定的，因此，人们努力寻找具有与顺序不变句子相同的表达能力的可判定语法的逻辑。我们表明，在有界树深度的结构，顺序不变的FO具有相同的表达能力FO。我们的证明技术允许对这种翻译的简洁性进行细粒度的分析。我们证明了，对于每一个顺序不变的FO句子存在一个FO句子，其大小是小学的原始句子的大小，其数量的交替是线性的树深度。我们得到类似的结果MSO。MSO和FO的表达能力在有界树深结构上是一致的。我们提供了一个翻译MSO FO，我们表明，这种翻译基本上是最佳的公式大小。作为进一步的结果，我们表明，顺序不变的MSO具有相同的表达能力，FO与有界树深度结构上的模计数量词。
2016-03-30 cs.LO
Axiomatizing Epistemic Logic of Friendship via Tree Sequent Calculus
本文积极地解决了Seligman、Girard和Liu等人提出的友谊认知逻辑是否能提供一个希尔伯特系统的问题。为了找到一个Hilbert系统，我们首先介绍了一个健全的，完整的和无割的树（或嵌套）EFL演算，这是一个集成的组合Seligman的基本混合逻辑的树演算和模态逻辑的树演算。然后，我们将树的结构转换成一个普通的公式来指定EFL的Hilbert系统，最后证明我们的Hilbert系统对于预定的二维语义是健全和完备的。
2019-07-10 cs.LO math.LO
Characterizing Weighted MSO for Trees by Branching Transitive Closure Logics
我们引入了分支传递闭包算子的加权一元二阶逻辑公式的分支对应于一个自然的方式在树中固有的分支。对任意交换半环，我们证明了树上的加权一元二阶逻辑等价于由下列算子之一开始的公式的可定义性：（i）分支传递闭包或（ii）存在二阶量词后接泛一阶量词;在这两种情况下，该运算符被应用于（a）通过模计数而丰富的布尔一阶逻辑或（b）布尔一元二阶逻辑上的步进公式。
2015-04-29 cs.FL cs.LO
On the Computability of Measures of Regular Sets of Infinite Trees
本文研究无限树上一元二阶逻辑的概率可满足性问题，提出计算随机树满足给定公式概率的方法，并证明该概率为代数数，从而将此前仅适用于较弱形式体系的结果推广到完整一元二阶逻辑。
2024-11-21 cs.LO
Wreath Products of Forest Algebras, with Applications to Tree Logics
我们使用最近发展起来的森林代数理论，找到代数刻画的语言中定义的各种逻辑的unranked树和森林。这些包括时间逻辑CTL和EF，以及祖先关系上的一阶逻辑。虽然刻画一般是无效的，我们能够用它们来制定必要条件的可定义性，并提供新的证明，一些语言是不可定义的，在这些逻辑。
2012-09-16 cs.FL cs.LO
One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+Past
在本文中，我们提出了一个新的一遍和树形tableau方法的时间命题时态逻辑和有界的变体与过去的运营商的扩展。时间命题时态逻辑（TPTL）是一种具有EXPSPACE完全可满足性问题的实时时态逻辑，已成功地应用于实时系统的验证。与LTL相反，将过去运算符添加到TPTL使得结果逻辑（TPTL+P）的可满足性问题非初等。在本文中，我们设计了一个一遍和树形tableau的TPTL和有界TPTL+P（TPTLb+P），一个语法限制引入编码的时间线为基础的规划问题，恢复EXPSPACE完全的复杂性。TPTL和TPTLb+P的tableau系统以统一的方式呈现，彼此非常相似，提供了一个通用的骨架，然后专门用于每个逻辑。在此过程中，我们将TPTLb+P的语义转换为TPTL+P的一个纯句法片段，给出了一个将前者嵌入后者的翻译。充分证明了系统的可靠性和完备性。特别是，我们给出了一个大大简化的模型理论的完备性证明，它回避了复杂的组合参数所使用的已知证明的一遍和树形tableau系统的LTL和LTL+ P。
2018-09-10 cs.LO
$ω$-Forest Algebras and Temporal Logics
我们使用[4]中介绍的无限树语言的代数框架来导出各种时态逻辑的有效特征，特别是逻辑EF（CTL的一个片段）及其计数变体cEF。
2022-03-25 cs.LO
Querying Fault and Attack Trees: Property Specification on a Water Network
本研究概述三种用于故障树与攻击树属性规约的查询语言，结合配水管网案例验证框架，提出FT/ATs整合建模方法，拓展逻辑组合与PFL语言构造以融合攻击与故障度量的相互作用。
2024-01-29 cs.LO
Reactive Synthesis: Branching Logics and Parameterized Systems
反应合成是一种自动的方法，可以将人类在某种逻辑中表达的意图转化为某种系统。本文分为逻辑和系统两部分。在第一部分中，我们开发了两种新的CTL* 合成方法。第一种方法由两个扩展的SMT为基础的有界综合：一个遵循自底向上的CTL* 模型检验，另一个遵循自动机框架。第二种方法将CTL* 合成减少为LTL合成。这种减少将任何LTL合成器变成CTL* 合成器。这两种方法已经实施，并可在网上查阅。在第二部分中，我们研究了两个系统架构的参数化综合。第一种体系结构是受缓存一致性协议启发的保护系统。在防护系统中，进程转换的启用或禁用取决于某些局部状态中是否存在其他进程。已有的关于保护协议的截断结果仅限于封闭系统，并且对于活性性质的应用有限。我们关闭这些差距，并证明了严格的截止与活性的开放系统，也截止检测死锁。第二种架构是令牌环系统，其中单个令牌循环布置在环中的进程。现有的参数化综合方法的实验表明，它不能扩展到大规格。首先，我们优化的方法，细化截止约简，使用模块化和抽象。评估显示了几个数量级的加速。其次，对工业仲裁协议AMBA进行了参数化综合案例研究。我们描述了新的技巧-一个新的截止扩展和分解合成-，再加上前面描述的优化，使我们能够合成AMBA在一个参数化的设置，第一次。
2018-08-28 cs.LO
Courcelle's Theorem Without Logic
本文受 Lovász 连接矩阵方法启发，提出库尔塞勒定理的广义版本，用纯粹组合假设替代一元二阶逻辑可定义性假设，从而在无需逻辑的条件下保持线性时间判定图性质的结果。
2025-05-05 cs.LO
Possibilistic Computation Tree Logic over Finitely-Valued Kripke Structures: Decidability and Complete Axiomatization
Shaanxi Normal University（陕西师范大学）
本研究针对尚未探讨的PoCTL可满足性问题，通过相关技术证明其可在指数时间内判定，并给出该逻辑的完备公理化，完善了PoCTL的理论基础。
2026-09-22 cs.LO
An Automaton-based Characterisation of First-Order Logic over Infinite Trees
本文研究无穷树上的一阶逻辑，通过引入两类犹豫树自动机精确捕获 polcCTLp 和 cCTL*[f] 的表达能力，提供自动机理论刻画并导出范式，揭示 FO 仅表达安全或共安全属性。
2025-09-17 cs.FL cs.LO
Drawing Prolog Search Trees: A Manual for Teachers and Students of Logic Programming
对于习惯于过程式编码的程序员来说，用Prolog编程很难。在本手册中，介绍了绘制搜索树的方法，目的是更好地理解Prolog的工作原理。在给出Prolog数据库、查询和搜索树的第一个例子之后，系统地介绍了绘制搜索树的艺术，给出了用变量、合取、析取和否定进行查询的准则。进一步的例子提供了完整的搜索树，显示在学习Prolog现在！
2020-01-22 cs.LO cs.PL
Merging Process Algebra and Action-based Computation Tree Logic
进程代数和时态逻辑是反应式和并发系统的规范、验证和系统开发的两种流行范式。这两种方法从不同的角度看待规范和验证，并提供互补的优势。为了在一个统一的框架中混合代数和逻辑风格的规范，Luttgen和Vogler提出了逻辑标记转换系统（LLTS）的概念。本文旨在提出一个面向LLTS的过程演算，除了通常的过程代数运算符，涉及逻辑连接词（合取和析取）和标准的时间运算符（总是和除非）。这种演算保留了这些逻辑运算符的通常属性，允许人们自由地混合操作和逻辑运算符，并支持组合推理。此外，还探讨了该演算与基于Petri网的计算树逻辑（ACTL）之间的联系，包括过程项的特征公式、ACTL公式的特征过程和伽罗瓦连接.
2012-12-31 cs.LO cs.SE
Reasoning about Intuitionistic Computation Tree Logic
Università di Napoli ”Federico II”（那不勒斯费德里科二世大学）；Télécom Paris（巴黎电信学院）
该研究定义了直觉主义版本的计算树逻辑（CTL），阐释其语义特征的形式验证价值，明确语法语义与基本性质，还证明标准CTL的部分不动点公理在该直觉主义版本中不成立。
2023-10-03 cs.AI cs.LO
Guarded Second-Order Logic, Spanning Trees, and Network Flows
根据Courcelle的一个定理，一元二阶逻辑和守护二阶逻辑（其中也可以量化的边缘集）有相同的表达能力，对所有可数$k$-稀疏超图类。在本文的第一部分中，我们将这个结果推广到任意基数的超图。在第二部分中，我们提出了一个概括处理的方法编码的顶点集的单顶点。
2010-02-16 cs.DM cs.LO
Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic
从计算复杂性的角度研究了分支时间逻辑CTL的可满足性问题。严格的上限和下限提供了每个时间操作符片段。在平行，最小模型的大小进行了研究，一个合适的概念极小。第三，研究了平坦的CTL，即，时态运算符嵌套深度非常低的公式。在复杂性和最小模型方面显示出尖锐的二分法：时间深度1具有低表达能力，而时间深度2相当于完整的CTL。
2017-02-24 cs.CC cs.LO
