Intransitive Linear Temporal Logic, Knowledge from Past, Decidability, Admissible Rules
我们的手稿研究线性时间（与UNTIL和NEXT）逻辑的基础上的概念不传递时间。非传递时间特别是，我们展示了如何在这样的框架中表示知识的概念（在这里，我们认为逻辑操作NN和操作UNTIL（实际上，时间整体）是针对过去）。我们研究的基本数学问题是任何逻辑系统的基本问题-可判定性和可判定性w.r.t.可接受的规则首先，我们考虑具有非一致非传递性的逻辑，并描述如何解决这种逻辑的可判定性问题。然后，我们考虑了这种逻辑的一种修改--具有一致不传递性的线性时态逻辑，并解决了推理规则的可容许性问题。在论文的结论部分列举了一系列有待解决的问题。
2015-03-30 cs.LO
Petri Net Reachability Graphs: Decidability Status of First Order Properties
我们调查的可判定性和复杂性状态的模型检查问题的无标签的可达图的Petri网，考虑一阶和模态语言没有标签的过渡或原子命题标记。我们考虑几个参数来区分可判定问题和不可判定问题。我们不仅能够提供精确的边界和系统的分析，而且还展示了我们证明技术的鲁棒性。
2012-10-19 cs.LO
Decidability and Complexity of Decision Problems for Affine Continuous VASS
本文研究仿射连续VASS的可达性、可覆盖性与状态可达性问题，针对不同仿射操作类给出几乎完全的可判定性分类，并补充紧复杂性上下界。
2024-05-17 cs.LO
Decidability of Graph Neural Networks via Logical Characterizations
本文利用Presburger量词等可判定逻辑刻画图神经网络的表达能力，建立了精确对应关系，并据此提出了GNN验证问题的判定过程，同时证明了相关静态分析与验证问题的不可判定性。
2025-01-29 cs.LO
Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints
众所周知，一元浅线性Horn片段是可判定的，并且具有许多应用，例如，在安全协议分析、树自动机或抽象细化中。如何将片段扩展到非Horn情况，保持可判定性，这是一个长期存在的开放问题，例如，能够在协议中表达非确定性。我们证明了非Horn一元浅线性分片的可判定性，并讨论了新的可判定分片的应用。
2017-05-24 cs.LO
Decidability of Intuitionistic Sentential Logic with Identity via Sequent Calculus
我们的论文有两个目的：本文首先在Chlebowski和Leszczynska-Jasion的论文“An Investigation into Intuitionistic Logic with Identity”中提出的演算的基础上，给出了一个直觉主义非Fregean逻辑ISCI的演算（Bulletin of the Section of Logic 48（4），p. 259-283，2019），其次，我们通过所获得的系统讨论ISCI的可判定性问题。上述论文中的原始演算没有为ISCI提供可判定性结果。为了得到这个结果，有两个问题需要解决：直觉逻辑的所谓循环特性和由于身份专用规则的形式而缺乏子公式性质。我们讨论可能的路线，以克服这些问题：我们考虑一个较弱的版本的子公式属性，守卫的复杂性公式，可以包括在它里面，我们还提出了一个证明搜索过程，当它失败时，然后存在一个反模型（在Kripke语义ISCI）。
2022-04-14 cs.LO
On the Decidability of (ground) Reachability Problems for Cryptographic Protocols (extended version)
符号模型中的密码协议的分析与演绎系统有关，演绎系统对攻击者关于该协议的执行的可能动作进行建模。本文提出了一种转换算法，这类演绎系统提供的方程理论具有有限的变化性质。这种变换的终止需要地面可达性问题的可判定性。证明了非基问题的可判定性需要增加一个条件，并给出了一个新的判定准则。
2009-06-05 cs.CR cs.LO
The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL
研究了概率计算树逻辑（PCTL）的可满足性和有限可满足性问题，其中算子不受任何步界的限制。我们建立了几个片段包含定量运算符的可判定性，并指出了在更复杂的片段中出现的困难，其中可判定性仍然是开放的。
2018-06-29 cs.LO
(Un)Decidability Bounds of the Synthesis Problem for Petri Games
该研究针对Petri博弈的综合问题，明确了不同玩家数量和安全性条件下的可判定性边界：双人全局安全条件下问题为NP完全，4人以内有非确定性指数上界，6人及以上局部安全条件下问题不可判定。
2023-10-02 cs.LO
Decidability Problems for Actor Systems
我们介绍了一个名义上的演员为基础的语言，并研究其表达能力。我们已经将域的存在/不存在确定为一个关键的功能：动态地创建与域相结合的名称，从而产生图灵完备性。另一方面，对无国籍行为者的限制导致了诸如终止之类的属性是可判定的系统。当参与者的数量是有界的并且状态是只读的时，这个可判定性结果仍然适用于具有状态的参与者。
2014-12-03 cs.LO cs.PL
On Decidability of Time-bounded Reachability in CTMDPs
考虑连续时间马氏决策过程的时间有界可达性问题。我们证明了这个问题是可判定的Schanuel猜想。我们的决策过程依赖于结构的最优政策和条件的可判定性（根据Schanuel的猜想）的理论的实数扩展指数和三角函数在有界域。我们进一步表明，任何无条件可判定性的结果将意味着无条件可判定的有界连续Skolem问题，或等价地，检查的问题，如果一个指数多项式有一个非切零在有界区间。我们注意到，后者的问题也是可判定的Schanuel的猜想，但寻找无条件的决策程序仍然是长期悬而未决的问题。
2020-06-09 cs.LO cs.SY eess.SY
Decidability of higher-order matching
我们表明，高阶匹配问题是决定使用博弈论的参数。
2009-07-31 cs.GT cs.LO
Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property
Tel Aviv University（特拉维夫大学）
本文通过符号模型性质证明了扩展分层公式的若干片段的可判定性，允许一种类型有自环函数以放宽量词交替约束。
2026-05-13 cs.LO
Decidability of MSO Reparameterization over Countable Chains
Tel Aviv University（特拉维夫大学）
本文研究了如何通过降低表示维度来简化MSO多维点解释，证明在可数标记线性序类上，给定的MSO公式是否允许d维重参数化是可判定的。
2026-05-19 cs.LO
Algorithmic Problems for Computation Trees
本文研究计算树的优化、可解性与可满足性三类算法问题，分析优化问题的可判定性如何依赖于后两者的可判定性，并给出可判定与不可判定的多种实例。
2025-01-03 cs.LO
(Un)Decidability Results for Word Equations with Length and Regular Expression Constraints
我们证明了几个可判定性和不可判定性结果的可满足性和有效性问题的语言，可以表示解决方案的字方程的长度约束。这种语言上的原子公式是字符串项上的等式（单词等式）、长度函数上的线性不等式（长度约束）和正则集中的成员资格。这些问题在逻辑、程序分析和形式化验证中很重要。这些问题的变体已经被数学家研究了几十年。最近，这些公式的实际可满足性程序（又名SMT求解器）在字符串操作程序（如Web应用程序）的安全分析中变得越来越重要。我们证明了三个主要定理。首先，我们给出了一个新的证明不可判定的有效性问题的一组句子写为一个forall-exists量词交替应用于正字方程。这个不可判定性结果的一个推论是，这个集合是不可判定的，即使句子中最多出现两次字符串变量。第二，我们考虑布尔组合的量词自由公式构建的词方程和长度约束。我们表明，如果字方程可以转换为一个解决的形式，在实践中相关的形式，然后满足性问题的布尔组合的字方程和长度约束是可判定的。第三，我们证明了无量词公式在正则解形式、长度约束和正则表达式上的成员谓词上的可满足性问题也是可判定的。
2013-06-25 cs.LO
Decidability problems in automaton semigroups
我们考虑自相似半群的可判定性问题，特别是在$X^*$的自动变换半群。我们描述的算法回答的字问题，并限制其复杂性下的一些额外的假设。我们给出了一个部分算法，决定在一个自动机，给定$x,y$，是否恩格尔身份（$[\cdots[[x,y],y],\dots,y]=1$足够长的换向器序列）所产生的一组是满意的。这个算法成功地证明了Grigorchuk的$2$ -群不是Engel群。接下来，我们考虑识别恩格尔元素，即元素$y$，使得映射$x\mapsto[x,y]$吸引到$\{1\}$的问题。虽然这个问题似乎棘手的一般情况下，我们证明，它是可判定的Grigorchuk的组：恩格尔元素正是那些为了最多$2$。我们在正文中包括了大量的未决问题。我们的计算是使用计算机代数系统“Gap”中的软件包“Fr”实现的。
2017-05-11 cs.LO math.GR
Decidability and Undecidability Results for Propositional Schemata
CNRS（法国国家科学研究中心）
我们定义了一个逻辑的命题公式图式添加到语法的命题逻辑索引命题和迭代连接词范围内的算术变量参数化的区间。可满足性问题是不可判定的，这个新的逻辑，但我们引入了一个非常一般的类的模式，称为有界线性，这个问题变得可判定。这个结果是通过减少到一个特定的类称为定期的模式，我们提供了一个健全的和完整的终止证明过程。这种模式演算允许一个捕获证明模式对应于一个大类的命题逻辑中指定的问题。我们还表明，可满足性问题再次成为不可判定的轻微扩展这一类，从而表明，有界线性模式代表了一个很好的妥协之间的表达性和可判定性。
2014-01-16 cs.AI cs.LO
Third Order Matching is Decidable
针对简单类型 λ-演算中高阶匹配可判定性的开放问题，本文证明了当问题变量阶数至多为三阶时该匹配问题可判定。
2023-06-02 cs.LO
On the Decidability of Reachability in Continuous Time Linear Time-Invariant Systems
研究了连续时间线性定常控制系统状态到状态可达性的判定问题。我们分析这个问题的允许控制集，这是假设下的单位超立方体的线性映射的图像。这自然地对有界（有时称为饱和）控制进行建模。控制集是$\mathbb{R}^n$的仿射子空间的可达性问题的判定性是控制理论中的一个基本结果。我们的第一个结果是二维可判定性（$n=2$），如果矩阵$A$满足某些谱条件，以及一般的条件可判定性。如果变换矩阵$A$是对角的有理元素（或同一代数数的有理倍数），则可达性问题是可判定的。如果变换矩阵$A$只有实特征值，则可达性问题是条件可判定的。时间有界可达性问题在二维上是条件可判定的，也是无条件可判定的。我们的一些可判定性结果是有条件的，因为它们依赖于某些数学理论的可判定性，即指数实数理论（$\mathfrak{R}_{\exp}$）和有界正弦实数理论（$\mathfrak{R}_{\exp,\sin}$）。我们还得到了一个硬度的问题，其中目标是简单的集合（超立方体的尺寸$n-1$或超平面），而不是一个点，控制集是凸有界多面体的温和推广的结果。在这种情况下，我们表明，该问题至少是一样难的\emph{Continuous Positivity problem}或\emph{Nontangential Continuous Positivity problem}。
2021-03-15 cs.LO cs.SY eess.SY
Possibilistic Computation Tree Logic over Finitely-Valued Kripke Structures: Decidability and Complete Axiomatization
Shaanxi Normal University（陕西师范大学）
本研究针对尚未探讨的PoCTL可满足性问题，通过相关技术证明其可在指数时间内判定，并给出该逻辑的完备公理化，完善了PoCTL的理论基础。
2026-09-22 cs.LO
Decidability of definability
对于具有有限关系签名τ的固定可数无限结构Γ，我们研究了如下计算问题：输入是无量词τ-公式_0，_1，.，定义关系R_0，R_1，.，R_n over Γ.问题是关系R_0是否是可由R_1，. R_n，即，可由一阶公式定义，该公式仅使用R_1，...，R_n，等式，合取，存在量化（禁止析取，否定和全称量化）。我们证明了这个问题的可判定性，所有的结构，有一个一阶定义在一个有序的齐次结构Δ有限的关系签名，其年龄是一个拉姆齐类，并确定了许多禁止的子结构。具有这种性质的结构Γ的例子有有理数的序、随机图、齐次泛偏序集、随机竞赛图、所有齐次泛C-关系等等。当我们用存在的正可定义性或存在的可定义性来代替原始的正可定义性时，我们也得到了问题的可判定性。我们的证明利用了普遍的代数和模型理论的概念，拉姆齐理论，以及最近的Ramsey类拓扑动力学的表征。
2012-03-04 cs.LO math.LO
Decidability of predicate logics with team semantics
我们研究了基于团队语义的谓词逻辑的复杂性。证明了二元独立逻辑和二元包含逻辑的可满足性问题都是NEXPTIME-完全的。此外，我们表明，两个变量的依赖逻辑的有效性问题是不可判定的，从而解决了一个开放的问题，从团队语义文献。我们还简要地分析了依赖逻辑的Bernays-Schönfinkel-Ramsey前缀类的复杂性。
2016-06-18 cs.CC cs.LO math.LO
On the decidability and complexity of Metric Temporal Logic over finite words
度量时态逻辑（Metric Temporal Logic，MTL）是一种重要的实时系统规格说明形式。本文证明了有限时间词上MTL的可满足性问题是可判定的，具有非本原递归复杂性。我们还考虑了MTL的模型检查问题：是否所有的话接受一个给定的Alur-Dill时间自动机满足给定的MTL公式。我们证明了这个问题是可判定的有限字。在无限的话，我们表明，模型检验的安全片段的MTL-其中包括不变性和时间有界的响应特性-也是可判定的。这些结果是相当令人惊讶的，因为它们与文献中出现的各种相反的说法相矛盾。
2007-02-28 cs.CC cs.LO
Decidability Problems for Micro-Stipula
本文研究Micro-Stipula演算的可判定性问题，证明子句永不执行问题在一般情况及两个受限片段中不可判定，并发现瞬时片段中初始状态不相交时可达性可判定。
2025-04-23 cs.FL cs.LO
On the Decidability of Reachability in Linear Time-Invariant Systems
CNRS（法国国家科学研究中心）；LaBRI（计算机科学研究与教学联盟实验室）；Alan Turing Institute of Data Science（图灵数据科学研究所）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；IRIF（信息与随机相互作用研究所）；Université Paris Diderot（巴黎第七大学）；Department of Computer Science, University of Oxford（牛津大学计算机科学系）
本文研究了线性时不变控制系统中状态到状态可达性的可判定性问题，探讨了在允许控制集为仿射子空间的情况下可达性问题的可判定性，并在某些谱假设下证明了当控制集为凸多面体时可达性问题的可判定性。
2019-02-18 cs.DM cs.LO cs.SY
Logical Queries over Views: Decidability and Expressiveness
我们研究的问题，决定可满足性的一阶逻辑查询的意见，我们的目的是划定边界之间的可判定和不可判定的片段，这种语言。由于视图在信息集成和数据仓库等应用中的作用，视图目前在数据库研究中占据中心地位。我们的主要结果是确定一个可判定类的一阶查询一元合取的意见，概括了经典类的一阶句子一元关系，称为Lowenheim类的可判定性。然后，我们演示了如何这个类的各种扩展导致不可判定性，也提供了一些表现力的结果。除了它的理论兴趣，我们的新的可判定类是潜在的有趣的应用，如决定复杂的依赖关系的含义，分析一类受限制的主动数据库规则，本体推理。
2008-03-18 cs.DB cs.LO
Axioms and Decidability for Type Isomorphism in the Presence of Sums
我们考虑的问题的特点同构的类型，或等价地，建设性的基数集，同时存在的不相交的工会，笛卡尔产品，和指数。主要依赖于在我们的上下文中没有使用的关于具有指数的多项式的结果，我们得到：通常的有限公理化被称为高中恒等式（HSI）对于类型的重要子类是完备的;当两个类型同构时，它对于该子类是可判定的;对于整个类型集，HSI公理的递归扩展是完备的;并且，对于整个类型集，当基类型被解释为有限集时，关于两个类型是否同构的问题是可判定的。我们还指出了一些相关的开放性问题。
2014-01-20 cs.LO cs.PL math.LO
The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations
针对一阶逻辑中树宽有界性问题不可判定的情况，本文研究了关系签名上推广的Separation Logic，提出了该逻辑下树宽有界性问题的求解算法。
2024-05-17 cs.FL cs.LO
The Tree Width of Separation Logic with Recursive Definitions
分离逻辑是一种广泛使用的形式主义，用于描述动态分配的链接数据结构，如列表，树等的逻辑的各个片段的可判定性状态构成了一个长期存在的开放问题。目前的结果报告的技术，以确定满足性和有效性的蕴涵分离逻辑（S）的列表（可能与数据）。在本文中，我们建立了一个更一般的可判定性结果。我们证明了任何使用较一般的递归定义谓词的分离逻辑公式都是可判定的可满足性，而且这些公式之间的蕴涵也是可判定的有效性.这些谓词足够通用，可以定义（双）链表、树和比树更通用的结构，比如叶子被链接在一个链表中的树。可判定性证明是通过将一元二阶逻辑在有界树宽度的图上的可判定性归约来实现的。
2013-03-30 cs.FL cs.LO
Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability
本文研究可重构广播、带标识符寄存器的多智能体参数化网络，证明一般可覆盖性可判定但非原始递归，其他同步问题不可判定，而单寄存器情形为 NP 完全。
2024-03-04 cs.DC cs.FL cs.LO
First-order Fragments with Successor over Infinite Words
我们考虑片段的一阶逻辑和模型，我们允许有限和无限的话同时。除了相等之外，唯一的二元关系是顺序比较<和后继谓词+1。我们给出了片段Sigma 2 = Sigma 2 [<，+1]和FO 2 = FO 2 [<，+1]的代数和拓扑性质的刻画.为此，我们引入无限词的因子拓扑。事实证明，语言L是FO 2和Sigma 2的交集，当且仅当L是FO 2语言的内部。对称地，一种语言是FO 2和Pi 2的交集，当且仅当它是FO 2语言的拓扑闭包。片段Delta 2，根据定义是Sigma 2和Pi 2的交集，包含FO 2中的Clopen语言。特别地，在无限单词上Delta 2是FO 2的严格子类。我们的刻画产生的可判定性的成员资格问题，所有这些片段在有限和无限的话，作为一个必然的结果，我们也获得了无限的话的可判定性。此外，我们给出了有限字上点深3/2的一个新的可判定代数刻画。点深度3/2在有限词上的可判定性首先由Glaßer和Schmitz在STACS 2000中给出，而FO 2在无限词上的成员问题的可判定性则由Wilke在1998年的论文中给出，而Sigma 2在无限词上的可判定性以前是未知的。
2010-12-30 cs.FL cs.LO
The Membership Problem for Hypergeometric Sequences with Rational Parameters
研究了超几何序列的隶属度问题：给定一个有理数超几何序列$\langle u_n \rangle_{n=0}^\infty$和一个目标$t \in \mathbb{Q}$，判定序列中是否存在$t$.在定义递归$p(n)u_{n}=q(n)u_{n-1}$中，多项式$p(x)$和$q(x)$的根都是有理数的假设下，我们证明了这个问题的可判定性.我们的证明依赖于算术级数中素数密度的界限。我们还观察到成员问题（和变体）的可判定性和超越理论中的Rohrlich-Lang猜想之间的关系。
2022-05-24 cs.LO cs.SC
On the Subspace Orbit Problem and the Simultaneous Skolem Problem
University of Oxford（牛津大学）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；TU Wien（维也纳工业大学）
本文研究了轨道问题的子空间情况，证明当目标子空间维度与轨道维度对数相关时问题可解，且在有理数上具有NP^RP复杂度；同时，目标子空间维度与轨道维度线性相关的版本与斯科尔姆问题等价。
2026-05-14 cs.DM cs.LO
O-Minimal Invariants for Discrete-Time Dynamical Systems
线性回路的终止性分析在计算机科学的许多领域中起着关键作用，包括程序验证和抽象解释。对于线性循环的最简单的变体，终止问题已经涉及到数论中的深开放问题，例如线性递归序列的Skolem和Positivity问题的可判定性，或者离散时间线性动力系统的等价可达性问题。在本文中，我们介绍了类的\emph{o-minimal invariants}，这是广泛的比以前考虑的，并研究了可判定性的存在和算法合成等不变量作为证书的非终止线性循环配备了一大类的停机条件。我们建立了两个主要的可判定性结果，其中一个条件Schanuel的猜想在超越数论。
2020-05-11 cs.CC cs.LO math.AG
The Emptiness Problem for Valence Automata over Graph Monoids
这项工作的研究，在自动机的存储机制，允许可判定性的空虚问题。这个问题是正式使用价自动机，一个抽象的自动机模型，其中的存储机制是由幺半群。对于各种存储机制中的每一种，可以选择一个（通常是无限的）幺半群$M$，使得$M$上的价自动机等价于具有这种存储类型的（单向）自动机。事实上，许多重要的存储机制可以通过有限图定义的幺半群来实现，称为图幺半群。示例包括下推堆栈、部分盲计数器（其表现得像Petri网位置）、盲计数器（其可以获得负值）及其组合。因此，我们研究的图幺半群的空性问题的价自动机是可判定的。图幺半群实现的一个特殊模型是具有下推堆栈的Petri网。对于这些，可判定性是一个长期存在的开放性问题，我们在这里不回答它。然而，如果排除对应于该模型的子图，则可以实现特征化。此外，我们提供了一个描述的存储机制，决策仍然开放。这导致了一个模型，自然推广了下推Petri网和Reinhardt引入的优先级多计数器机。被证明是可判定的情况构成了一个自然的和显然是新的扩展的Petri网与可判定的可达性。最后表明，该模型可以与另一个这样的扩展Atig和Ganty：我们提出了进一步的可判定性结果，包括这两个Petri网扩展。
2017-10-20 cs.FL cs.LO math.GR
Decidability and Complexity for Quiescent Consistency and its Variations
静态一致性是并发对象的正确性的概念，它赋予对象在静态中的行为以意义，即，没有对象的操作被执行的状态。实现对象的正确性是根据相应的抽象规范来定义的。这就产生了两个重要的验证问题：成员资格（检查实现的行为是否被规范允许）和正确性（检查实现的所有行为是否被规范允许）。在本文中，我们证明了静态一致性的成员问题是NP-完全的，正确性问题是可判定的，但CONP-困难和EXPSPACE。对于这两个问题，我们认为有限版本的静态一致性，假设两个静止点之间的事件数量的上限。在这里，我们表明，成员资格的问题是在PTIME，而正确性是在PSPACE。静态一致性不保证顺序一致性，即，它允许在映射到抽象规范时对同一进程的操作调用进行重新排序。因此，我们也考虑静态序列一致性，它加强了静态一致性与一个额外的序列一致性条件。我们表明，无限制版本的成员资格和正确性是NP完全和不可判定的，分别。当通过限制两个静态点之间的事件数量时，成员资格在PTIME中，而正确性在PSPACE中。最后，我们考虑一个版本的静态顺序一致性，将上限的进程的数量为每一个运行的实现，并表明，静态顺序一致性与此限制的成员资格问题是在PTIME。
2015-11-26 cs.DC cs.DS cs.FL
