Undecidability of a Very Simple Modal Logic with Binding
我们展示了什么可以说是最简单的非子布尔模态逻辑的约束力的隐式概念的可满足性问题的不可判定性。这一工作丰富了从混合逻辑到记忆逻辑的关于模态逻辑不可判定性的一系列已有结果。
2015-08-14 cs.LO
On the Undecidability of Fuzzy Description Logics with GCIs with Lukasiewicz t-norm
IIIA - CSIC（西班牙国家研究委员会人工智能研究所）；ISTI - CNR（意大利国家研究委员会信息科学与技术研究所）
最近有一些意想不到的结果，模糊描述逻辑（FDLs）与一般概念包含（GCI）。他们表明，与经典的情况下，DL ALC与GCI不具有有限的模型属性下Lukasiewicz逻辑或产品逻辑，具体地说，知识库可满足性是一个不可判定的问题产品逻辑。我们在这里完成的分析表明，知识库可满足性也是一个不可判定的问题Lukasiewicz逻辑。
2011-07-27 cs.AI cs.LO
On the Decidability and Complexity of Some Fragments of Metric Temporal Logic
度量时态逻辑$\mtlfull$是研究最多的实时逻辑之一。它表现出相当大的多样性的表达性和可判定性的基础上允许的一套模式和时间间隔的限制$I$的性质。\oomit{The classical results of Alur and Henzinger showed that $\mtlfull$ is undecidable where as $\mitl$ which uses only non-singular intervals $NS$ is decidable. In a surprizing result, Ouaknine and Worrell showed that the satisfiability of $\mtl$ is decidable over finite pointwise models, albeit with NPR decision complexity, whereas it remains undecidable for infinite pointwise models or for continuous time.}在本文中，我们通过证明$\mtlsns$（其中$NS$表示非奇异区间）的可满足性在有限逐点严格单调时间上也是可判定的，从而加强了可判定性结果。我们利用时间投影技术给出了从Ouaknine和Worrell的逻辑$\mtls…
2013-11-27 cs.LO
(Un)Decidability Results for Word Equations with Length and Regular Expression Constraints
我们证明了几个可判定性和不可判定性结果的可满足性和有效性问题的语言，可以表示解决方案的字方程的长度约束。这种语言上的原子公式是字符串项上的等式（单词等式）、长度函数上的线性不等式（长度约束）和正则集中的成员资格。这些问题在逻辑、程序分析和形式化验证中很重要。这些问题的变体已经被数学家研究了几十年。最近，这些公式的实际可满足性程序（又名SMT求解器）在字符串操作程序（如Web应用程序）的安全分析中变得越来越重要。我们证明了三个主要定理。首先，我们给出了一个新的证明不可判定的有效性问题的一组句子写为一个forall-exists量词交替应用于正字方程。这个不可判定性结果的一个推论是，这个集合是不可判定的，即使句子中最多出现两次字符串变量。第二，我们考虑布尔组合的量词自由公式构建的词方程和长度约束。我们表明，如果字方程可以转换为一个解决的形式，在实践中相关的形式，然后满足性问题的布尔组合的字方程和长度约束是可判定的。第三，我们证明了无量词公式在正则解形式、长度约束和正则表达式上的成员谓词上的可满足性问题也是可判定的。
2013-06-25 cs.LO
Decision Problems for Petri Nets with Names
我们证明了nu-PN，纯名称创建和名称管理的P/T网的扩展的可判定性和不可判定性的结果。通过将具有抑制弧的网的可达性归结为可达性，给出了可达性不可判定性的一个简单证明，从而证明了nu-PN网的表达能力严格优于P/T网。我们证明了nu-PN是结构良好的转移系统。特别地，我们得到了可覆盖性和可终止性的可判定性，从而没有达到图灵机的表达能力。此外，它们是严格良结构的，因此有界性问题也是可判定的。我们考虑两个属性，宽度有界性和深度有界性，分解有界性。宽度有界性已经被证明是可判定的。我们在这里证明深度有界的不可判定性。最后，我们得到阿克曼硬度的结果，我们所有的可判定的决策问题。
2010-11-17 cs.LO
Satisfiability of CTL* with constraints
我们证明了在Z上具有等式，顺序和模约束的CTL* 的可满足性是可判定的。以前，仅知道CTL* 的某些片段的可判定性，例如，存在主义和积极的碎片和EF。
2013-06-04 cs.LO
The Complexity of Satisfiability for Fragments of Hybrid Logic -- Part I
混合逻辑的可满足性问题是不可判定的。这引发了一个关于可判定和可处理片段的研究计划。在本文中，我们调查的影响，限制命题部分的语言的可判定性和可满足性问题的复杂性在任意的，传递的，总的框架，框架的基础上的等价关系。我们还考虑了不同的模态和混合算子。我们跟踪边界的可判定性，并给出了精确的复杂性，大多数片段，特别是包括否定的所有片段。对于单调片段，我们能够区分容易的情况下，从困难的情况下，这取决于允许的一组操作。
2009-06-08 cs.CC cs.LO
Delta-Decidability over the Reals
给定实数上任意可计算函数的集合F，我们证明了存在一个算法，给定任意只包含有界量词的L_F-语句φ和任意正有理数δ，该算法判定“φ为真”或“φ的δ-加强为假”.在适当的假设下，对于C-可计算签名F，L_F中有界k-语句的δ-判定问题存在于（k_k^P）^C中.结果与著名的不可判定性结果形成鲜明对比，并作为一个理论基础，为使用数值方法在决策过程中的非线性一阶理论在实数。
2012-04-30 cs.LO
Decidability and Universality in Symbolic Dynamical Systems
自图灵的工作以来，各种类型的动力系统的计算普适性的许多不同定义已经蓬勃发展。我们提出了一个普遍性的一般定义，适用于任意离散时间符号动力系统。系统的普适性定义为模型检验问题的不可判定性。对于图灵机、计数器机和标记系统，我们的定义与经典的定义一致。然而，它产生了一个新的定义细胞自动机和subshifts。我们的定义是强大的初始条件，这是一个理想的物理可实现的功能。我们推导出不可判定性和普适性的必要条件。例如，一个通用系统必须有一个敏感点和一个适当的子系统。我们猜想泛系统有无穷多个子系统。我们还讨论了论文，根据该计算应该发生在“混沌的边缘”，我们展示了一个普遍的混沌系统。
2005-07-08 cs.CC cs.LO
Rich Sequences and Decidability of Arithmetic Theories
Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；Oxford University（牛津大学）；Keble College, Oxford（牛津基布尔学院）
本文提出新框架，将整数序列的随机性结果转化为算术结构一阶理论不可判定性的证明，应用于线性递推序列和欧拉函数等，得出多个理论不可判定。
2026-09-18 cs.FL 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
On the freeze quantifier in Constraint LTL: decidability and complexity
约束LTL是LTL在Presburger约束上的推广，通常被用作一种形式语言来描述具有约束的操作模型的行为。冻结量词可以是语言的一部分，如在一些实时逻辑中，但这种变量绑定机制在许多逻辑语言中（一阶时态逻辑，混合逻辑，序列图逻辑，导航逻辑，具有抽象的逻辑等）是相当普遍和普遍的。我们表明，约束LTL在简单的域（N，=）增加了冻结量词是不可判定的，这是一个令人惊讶的结果，鉴于穷人的语言约束（只有平等测试）。许多版本的无冻结约束LTL在具有定性谓词的域上是可判定的，我们的不可判定性结果实际上建立了Sigma_1^1-完备性。在积极的一面，我们提供的复杂性结果时，域是有限的（EXPSPACE-完备性）或当公式是平坦的，在某种意义上介绍的文件。我们的不可判定性的结果是尖锐的（即限制变量的数量），我们所有的复杂性特征确保完整性方面的一些复杂性类（主要是PSPACE和EXPSPACE）。
2006-09-29 cs.CC cs.LO
Quasi-decidability of a Fragment of the First-order Theory of Real Numbers
在本文中，我们考虑的一个片段的一阶理论的实数，其中包括系统的方程的连续功能在有界域，并为所有的功能是可计算的意义上，它是可能的计算任意关闭分段区间近似。即使这个片段是不可判定的，我们证明了有一个（可能是非终止的）算法来检查可满足性，使得（1）每当它终止时，它计算出一个正确的答案，（2）当输入是鲁棒的时，它总是终止。一个公式是鲁棒的，如果它的可满足性在小扰动下不改变。作为我们的算法的基本工具，我们使用的概念，从（微分）拓扑领域的程度。
2016-08-12 cs.CC cs.LO
Complexity of Hybrid Logics over Transitive Frames
本文研究了传递框架、传递树和线性框架上的混合逻辑的复杂性。我们证明了在传递框架上的可满足性是NEXPTIME-完全的。这与这种语言在任意框架上的可满足性的不可判定性形成对比（Areces，Blackburn，Marx 1999）。它还表明，添加@运营商或过去的模态导致不可判定传递框架。这再次与传递树和线性框架的情况形成对比，在这些情况下，我们证明这些语言是非元素可判定的。此外，我们建立了2 EXPTIME和EXPTIME上界可满足的传递框架和传递树，分别为混合直到/因为语言。一个EXPTIME下限保持模态直到语言在两个框架类。
2008-06-25 cs.LO
Undecidability of a Theory of Strings, Linear Arithmetic over Length, and String-Number Conversion
近年来，在形式化验证、软件工程和安全社区中，对字符串方程、长度函数和字符串数转换谓词的理论有相当大的兴趣。这些理论的SMT求解器，如Z3 str 2，CVC 4和S3，在暴露字符串密集型程序中的安全漏洞方面具有巨大的实用价值。此外，在弦理论的背景下，还有许多开放的可判定性和复杂性理论问题，这些问题引起了数学家的极大兴趣。基于上述应用和未解决的问题，我们研究了弦方程的一阶、多排序、无量词理论$T_{s,n}$，弦长度上的线性算术，以及弦数转换谓词，并证明了三个定理.首先，我们证明了理论$T_{s,n}$的可满足性问题是不可判定的，通过一个带有幂谓词的自然数上的线性算术理论的约化，我们称之为幂算术。其次，我们表明，字符串-数字转换谓词是可表达的权力谓词，字符串方程和长度函数。这个第二个定理，结合我们提出的不可判定性定理的约简，表明幂谓词可以用词方程和长度函数表示，当且仅当串-数值转换谓词也可以在同一片段中表示。这样的结果是非常有用的工具，在比较不同的理论的表达能力，并建立可判定性和复杂性的结果。第三，我们为$T_{s,n}$的函数和谓词提供了一个一致的公理化$Γ$。此外，我们还证明了通过$Γ$的逻辑闭包得到的理论$T_Γ$不是一个完备的理论.
2016-10-26 cs.LO
Undecidability and non-axiomatizability of modal many-valued logics
在这项工作中，我们研究了一类全球模态逻辑所产生的Kripke框架评估某些剩余格，在文献中称为模态多值逻辑的可判定性。我们展示了一个大的家庭，这些模态逻辑是不可判定的，与经典的模态逻辑和命题逻辑定义在同一类代数。这个家族包括了在标准Lukasiewicz代数和乘积代数上计算的Kripke框架所产生的全局模态逻辑。我们改进了前面的结果，证明了全局模态Lukasiewicz和乘积逻辑甚至不能递归可公理化。我们的结论是否定地解决了开放的问题，即每个全局模态逻辑是否与它的局部模态逻辑在无限制必然规则下是封闭的。
2022-04-15 cs.LO math.LO
Decidability bounds for Presburger arithmetic extended by sine
我们考虑Presburger算法的正弦函数扩展，称之为正弦Presburger算法（$\sin$ -PA），并系统地研究了决策问题的$\sin$ -PA的句子集。特别地，在Schanuel猜想的假设下，给出了一个存在$\sin$ -PA语句的判定算法.这个过程减少决策的理论有序添加剂群的实数扩展正弦，这是决定下Schanuel猜想。另一方面，我们证明了四个交替的量词块足以满足$\sin$ -PA句子的不可判定性。要做到这一点，我们明确解释弱一元二阶理论的网格，这是不可判定的，在$\sin$ -PA。
2022-05-02 cs.LO math.LO
Dividing Line between Decidable PDA's and Undecidable Ones
Senizergues已经证明了语言等价对于不相交的ε-确定性PDA是可判定的。Stirling证明了强双相似性对于PDA是可判定的。在消极的一面Srba证明，弱双相似性是不可判定的赋范PDA。后来，Jancar和Srba建立了不相交epsilon-pushing PDA和不相交epsilon-popping PDA的弱双相似性的不可判定性。本文推广了这些可判定性和不可判定性结果。扩展是通过查看PDA的几个变体的分支双相似性的等价性检查问题来完成的。
2014-04-28 cs.LO
Logical Queries over Views: Decidability and Expressiveness
我们研究的问题，决定可满足性的一阶逻辑查询的意见，我们的目的是划定边界之间的可判定和不可判定的片段，这种语言。由于视图在信息集成和数据仓库等应用中的作用，视图目前在数据库研究中占据中心地位。我们的主要结果是确定一个可判定类的一阶查询一元合取的意见，概括了经典类的一阶句子一元关系，称为Lowenheim类的可判定性。然后，我们演示了如何这个类的各种扩展导致不可判定性，也提供了一些表现力的结果。除了它的理论兴趣，我们的新的可判定类是潜在的有趣的应用，如决定复杂的依赖关系的含义，分析一类受限制的主动数据库规则，本体推理。
2008-03-18 cs.DB cs.LO
Exploring Non-Regular Extensions of Propositional Dynamic Logic with Description-Logics Features
TU Dresden（德累斯顿工业大学）；University of Wrocław（弗罗茨瓦夫大学）
本文研究非正则路径表达式对 ALC 扩展描述逻辑可判定性的影响，证明 ALCvpl 在加入 Self 或 nominals 后概念可满足性不可判定，并确立含非正则原子的查询蕴涵不可判定。
2024-05-13 cs.AI cs.LO
Decidability of the interval temporal logic ABBar over the natural numbers
在本文中，我们把注意力集中在艾伦的关系“满足”，“开始”，“开始于”（简称ABBar），解释了自然数的时间间隔逻辑。我们首先介绍的逻辑，我们表明，它是有足够的表现力来建模独特的区间属性，如完成条件，捕捉基于点的时态逻辑的基本形式，如直到运营商，并编码相关的度量约束。然后，我们证明了ABBar在自然数上的可满足性问题是可判定的，提供了一个小模型定理的基础上原来的压缩方法。最后证明了问题的EXPSPACE-完全性
2010-02-03 cs.LO
The Complexity of Data-Free Nfer
本文研究无数据 nfer 的求值与可满足性复杂性，证明仅含包含规则时二者均可在多项式时间求解，无循环规范可满足性为可判定且具 NExpTime 下界，完整语言则不可判定。
2026-10-27 cs.LO
Undecidability of a weak version of MSO+U
本文证明在 $\omega$-词上扩展二阶谓词 $U_1$ 的 MSO 不可判定，并推论允许量化最终周期集合时 MSO 也不可判定。
2020-02-10 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
Analysis of logics with arithmetic
该研究针对带计数与算术的逻辑的有限可满足性问题，给出局部Presburger量词逻辑可满足性复杂度紧界与双变量计数逻辑基数半线性表示，还简化了部分已有关键结果的证明。
2025-10-29 cs.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
Logic of the Hide and Seek Game: Characterization, Axiomatization, Decidability
本文研究捉迷藏博弈逻辑 LHS，证明单关系 LHS 不可判定，给出 van Benthem 风格刻画定理，并通过拆分 LHS- 语言建立完备 Hilbert 证明系统且证明其可判定，结果可推广至任意 n > 2 个智能体。
2023-05-25 cs.LO math.LO
Formal Languages via Theories over Strings
我们调查的形式语言的性质表示的公式在量词的自由理论的字方程，算术长度的限制，语言成员谓词的类定期，明显下推，和确定性上下文无关的语言。总的来说，我们考虑了20个不同的理论和可判定性问题，例如形式语言的空性和普遍性。首先，我们讨论了它们的相对表达能力，并观察到一个粗略的划分为两个层次的基础上是否存在字方程。其次，我们考虑了几个重要的决策问题，如空性和普遍性的可判定性状态。注意空性问题等价于相应理论上的可满足性问题。第三，我们考虑的问题，是否在一个理论的语言是在另一个表达，并显示几个负面的结果，这个问题是不可判定的。这些结果是特别相关的背景下，范式在实践和理论方面的字符串解决。
2022-05-01 cs.FL cs.LO
Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
提出$ω$MSO$\Join$BAPA逻辑，通过Parikh-Muller树自动机证明其在树可解释结构上的可满足性可判定，并推广至带高级计数的双变量逻辑与$μ$-演算。
2023-11-23 cs.FL cs.LO
Non-Rigid Designators in Modal and Temporal Free Description Logics (Extended Version)
本研究提出带非严格限定摹状词与名称的模态描述逻辑，关联一阶模态逻辑单变量片段可满足性，证明$\n mathbf{S5}^{n}$等逻辑概念可满足性为NEXPTIME完全，还分析了时态逻辑可判定性。
2024-09-10 cs.LO
SHACL Satisfiability and Containment (Extended Paper)
University of Southampton（南安普顿大学）；Università degli Studi di Napoli Federico II（那不勒斯费德里科二世大学）
XML约束语言（SHACL）是最近W3C推荐的用于验证RDF数据的语言。具体来说，SHACL文档是在RDF图上强制特定形状的约束的集合。以前的工作提供了理论和实际的验证问题的结果，但没有考虑标准的决策问题的可满足性和包容性，这是至关重要的验证的可行性的约束和重要的设计和优化的目的。在本文中，我们进行了深入的研究，非递归SHACL的不同功能，提供了一个新的一阶语言，称为SCL的翻译，准确地捕捉语义的SHACL w.r.t.可满足性和包容性。我们研究了SHACL功能在这个逻辑中的相互作用，并提供了详细的地图的可判定性和复杂性的结果，上述决策问题的不同SHACL子语言。值得注意的是，我们证明了这两个问题是不可判定的完整的语言，但我们提出了可判定的组合有趣的功能。
2020-11-05 cs.AI cs.DB cs.LO
Computabilities of Validity and Satisfiability in Probability Logics over Finite and Countable Models
Harvard University（哈佛大学）
Kuyper和Terwijn的$ε$ -逻辑（本文中称为$ε$ E-逻辑）是一阶逻辑的变体，具有相同的语法，其中模型配备有概率测度，并且其中$\forall x$量词被解释为“存在测度$\ge 1 - ε$的集合$A$，使得对于每个$x \in A$，.在此之前，Kuyper和Terwijn证明了这个逻辑的一般可满足性和有效性问题是：i）对于有理$ε\in (0, 1)$，分别是$Σ^1_1$ -完全和$Π^1_1$ -困难的; ii）对于$ε= 0$，分别是可判定的和$Σ^0_1$ -完全的。形容词“普遍”在这里的意思是“在所有语言中一致”。“我们在有限模型的情况下扩展了这些结果。特别是，我们证明了在$ε$ E-逻辑有限模型的可满足性和有效性的问题，i）合理的$ε\in (0, 1)$，分别为$Σ^0_1$ -和$Π^0_1$ -完全，和ii）$ε= 0$，分别可判定和$Π^0_1$ -完全。虽然也取得了部分结果对可数的情况下，$ε$ E-逻辑的可计算性在可数模型仍然在很大程度上没有解决。此外，大多数的结果，本文和Kuyper和Terwijn，不适用于个别语言的有限数量的一元谓词。降低这一要求仍然是研究的重点。在积极的一面，我们得出了相应的问题的可判定性一元关系语言-平等和功能免费的语言与许多一元和零其他谓词。这一结果适用于所有三种无限制、可数和有限模型的情况。在这些可判定性和不…
2014-12-12 cs.LG cs.LO math.LO
Context unification is in PSPACE
语境是带有一个“洞”的术语，即我们可以替换论点的地方。在上下文统一，我们给出了一个方程的条款与变量表示上下文，并询问这个方程的可满足性。上下文统一是二阶统一的一个自然子变量，是不可判定的，同时也是词方程的一个推广，是可判定的。这是这两者之间的独特问题，其可判定性是不确定的（近二十年来）。在本文中，我们证明了上下文统一是在PSPACE。在一阶签名是有限的（通常）假设下，结果成立。这一结果是通过扩展的再压缩技术，最近开发的作者和使用，特别是获得一个新的PSPACE算法满足字方程，上下文统一。重新压缩基于执行简单的压缩规则（替换相邻函数符号对），这些规则（概念上）应用于上下文方程的解，并且以某种方式修改方程，使得实际上可以直接对方程执行这样的压缩步骤，而不知道实际的解。
2013-11-08 cs.FL cs.LO
Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)
Free University of Bozen-Bolzano（博尔扎诺自由大学）
本文研究有限迹上的线性时态逻辑（LTLf），其中命题字母被替换为任意理论上的一阶公式，其思想是可满足性模理论。由此产生的逻辑，称为LTLf模理论（LTLfMT），是半可判定的。尽管如此，它的高表现力在许多用例中非常有用，例如数据感知流程的模型检查和数据感知规划。尽管这些问题通常是不可判定的，但能够解决可满足的实例是一个值得研究的折衷方案。在激励和描述这样的用例之后，我们提供了一个基于单通道树形tableau系统的SMT编码的LTLfMT的健全和完整的半决策过程。该算法在BLACK可满足性检查工具中实现，并在新的基准测试上进行了实验评估，结果表明了该方法的可行性。
2022-05-24 cs.AI cs.LO
String Solving with Word Equations and Transducers: Towards a Logic for Analysing Mutation XSS (Full Version)
我们研究了以连接和有限状态转换器作为原子操作的弦逻辑的可满足性的判定性的基本问题。虽然限制到一种类型的操作产生的可判定性，很少有人知道他们的组合理论，这是特别相关的动态网页在一个更现实的浏览器模型的安全漏洞分析时的可判定性。一方面，单词方程（带有连接的字符串逻辑）不能精确地捕获清理功能（例如htmlescape）和隐式浏览器转换（例如innerHTML突变）。另一方面，转换器遭受能够对消毒功能和浏览器转换建模，但不能对字符串连接建模的相反问题。简单地将词方程和转换器组合在一起很容易导致不可判定的逻辑。我们的主要贡献是表明，“直线片段”的逻辑是可判定的（复杂性范围从PSPACE到EXPSPACE）。该片段可以表达的程序逻辑的直线字符串操作程序的连接和转换作为原子操作，这出现在执行有界模型检验或动态符号执行。我们证明了逻辑可以自然地表达分析Web应用程序中的突变XSS所需的约束。最后，在存在长度、字母计数、正则、indexOf和不等性约束的情况下，逻辑仍然是可判定的。
2015-11-05 cs.LO
Timed context-free temporal logics (extended version)
本文的重点是时间逻辑的实时下推反应系统的行为的描述。本文旨在通过确保组合设置中的可判定性和易处理性，来桥接专门用于分别表达密集实时实时属性和上下文无关属性的易处理逻辑。为此，我们引入两个实时线性时序逻辑指定定量定时上下文无关的要求在逐点语义设置：事件时钟嵌套时序逻辑（ECNTL）和嵌套度量时序逻辑（NMTL）。ECNTL逻辑是CARET逻辑（标准LTL的上下文无关扩展）和事件时钟时序逻辑（与事件时钟自动机类相关的易处理实时逻辑框架）的扩展。我们证明了ECNTL的可满足性和可视下推时间自动机VPTA对ECNTL的可视模型检验是可判定的和EXPTIME完全的。另一个提出的逻辑NMTL是标准度量时态逻辑（MTL）的上下文无关的扩展。众所周知，未来MTL的可满足性在无限时间词上是不可判定的，但在有限时间词上是可判定的。另一方面，我们表明，通过增加未来的MTL与未来的上下文无关的时间运营商，可满足性问题原来是不可判定的有限时间的话。在积极的一面，我们设计了一个有意义的和可判定的片段的逻辑NMTL，这是表示等价于ECNTL和可满足性和明显的模型检查的VPTA是EXPTIME完成的。
2018-08-14 cs.LO
Timed Context-Free Temporal Logics
本文的重点是时间逻辑的实时下推反应系统的行为的描述。本文旨在通过确保组合设置中的可判定性和易处理性，来桥接专门用于分别表达密集实时实时属性和上下文无关属性的易处理逻辑。为此，我们引入两个实时线性时序逻辑指定定量定时上下文无关的要求在逐点语义设置：事件时钟嵌套时序逻辑（EC_NTL）和嵌套度量时序逻辑（NMTL）。逻辑EC_NTL是逻辑CaRet（标准LTL的上下文无关扩展）和事件时钟时序逻辑（与事件时钟自动机类相关的易处理实时逻辑框架）的扩展。本文证明了EC_NTL的可满足性和可视下推时间自动机（VPTA）对EC_NTL的可视模型检验是可判定的和EXPTIME-完全的。另一个提出的逻辑NMTL是标准度量时态逻辑（MTL）的上下文无关的扩展。众所周知，未来MTL的可满足性在无限时间词上是不可判定的，但在有限时间词上是可判定的。另一方面，我们表明，通过增加未来的MTL与未来的上下文无关的时间运营商，可满足性问题原来是不可判定的有限时间的话。在积极的一面，我们设计了一个有意义的和可判定的片段的逻辑NMTL，这是表示等价于EC_NTL和可满足性和明显的模型检查的VPTA是EXPTIME完成的。
2018-09-10 cs.LO
A Decidable Theory of Skiplists of Unbounded Size and Arbitrary Height
本文给出了任意高度跳跃者的理论，并证明了无量词公式的可满足性问题的可判定性。跳跃列表是一种命令式软件数据结构，它通过在内存中维护几个级别的有序单链表来实现集合，其中每个级别是其较低级别的子列表。Skiplist在实践中被广泛使用，因为它们提供了与平衡二叉树相当的性能，并且可以更有效地实现。为了实现此性能，大多数实现都会动态增加高度（级别数）。由于动态大小（节点数量）和不同层之间的共享，很难对Skiplist进行推理。此外，关于动态高度的推理增加了处理任意多个水平的挑战。本文的第一个贡献是理论TSL，允许表示堆内存布局的跳跃列表的任意高度。第二个贡献是无量词TSL公式的可满足性问题的判定过程。最后的贡献是说明了形式化验证的实际skiplist实现使用此决策过程。
2013-01-18 cs.LO
