Decidability, Introduction Rules and Automata
Gilles Dowek, Ying Jiang
我们提出了一种方法来证明几个著名的推理系统的可证明性的可判定性。该方法推广了割消法和构造识别可证命题的自动机的方法。
We present a method to prove the decidability of provability in several well-known inference systems. This method generalizes both cut-elimination and the construction of an automaton recognizing the provable propositions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata
我们考虑由无限多个均匀设计的线性混合自动机组成的系统，其动态行为由它们与相邻系统的关系决定。我们提出了一类这样的系统和一类安全属性，其验证可以减少到验证（小）家庭的有界大小的相邻系统，并确定在这种情况下，验证问题是可判定的，分别。固定参数易于处理。我们说明了一个例子，从协调车辆指导的方法，并描述了一个实现，使我们能够自动执行这样的验证任务。
The Decidability Frontier for Probabilistic Automata on Infinite Words
我们认为概率自动机的无限的话，接受定义的安全性，可达性，Büchi，coBüchi，和限制平均条件。我们考虑定量和定性决策问题。我们提出了概率有限自动机的扩展和适应性证明，并提出了一个完整的刻画概率自动机的定量和定性决策问题的可判定性和不可判定性的边界上无限的话。
Small model property reflects in games and automata
小模型性质是隐含可判定性的一个重要性质。我们表明，小模型的大小是直接相关的游戏和自动机检查可证明性的一些重要资源。
An Application of the Feferman-Vaught Theorem to Automata and Logics for<br> Words over an Infinite Alphabet
我们表明，一个特殊的情况下，Feferman-Vaught组合定理产生了一个自然的概念，自动机的有限字在一个无限的字母表，具有良好的封闭性和可判定性，以及一些逻辑刻画。我们还考虑了一个轻微的扩展的Feferman-Vaught形式主义，它允许表达更多的组件值之间的关系（如平等），并证明相关的可判定性结果。从这个结果，我们得到了新的类的可判定逻辑的词在一个无限的字母表。
Decidability of Timed Communicating Automata
研究了时间通信网络的可达性问题。每个进程都是一个时间自动机，通过在无界FIFO通道上交换消息与其他进程进行通信。消息携带时钟，该时钟在发送和接收时以适当的定时约束进行检查。每个自动机只能访问它的本地时钟和发送/接收消息的消息时钟集。时间是密集的，所有的时钟都以相同的速度进化。我们的主要贡献是一个完整的特征的可判定和不可判定的通信拓扑结构概括和统一以前的工作。从技术的角度来看，我们使用量词消去和减少计数器自动机与寄存器。
Set Automata and Limits of Decidability of Two-Variable Logic on Data Words
研究扩展数据词双变量逻辑以包含guarded regular二元谓词，定义了idempotent monoids的决定性条件，并引入set automata形式化，证明其与ordered quasi-normal set automata的等价性。
Equivalence of pushdown automata via first-order grammars
给出了一阶文法互模拟等价的可判定性证明。它是Sénizergues（1998，2005）的一个结果的另一种证明，该结果包含了他对确定性下推自动机的著名可判定性问题的肯定解。所提出的证明是概念上更简单，一个特别的新颖性是，它不是作为两个半决策程序，但它提供了一个明确的算法，可能是服从复杂性分析。
Intransitive Linear Temporal Logic, Knowledge from Past, Decidability, Admissible Rules
我们的手稿研究线性时间（与UNTIL和NEXT）逻辑的基础上的概念不传递时间。非传递时间特别是，我们展示了如何在这样的框架中表示知识的概念（在这里，我们认为逻辑操作NN和操作UNTIL（实际上，时间整体）是针对过去）。我们研究的基本数学问题是任何逻辑系统的基本问题-可判定性和可判定性w.r.t.可接受的规则首先，我们考虑具有非一致非传递性的逻辑，并描述如何解决这种逻辑的可判定性问题。然后，我们考虑了这种逻辑的一种修改--具有一致不传递性的线性时态逻辑，并解决了推理规则的可容许性问题。在论文的结论部分列举了一系列有待解决的问题。
Decision Procedures for Sequence Theories (Technical Report)
本文研究序列理论的可判定性，证明基于布尔代数字母表和参数自动机可保持可判定性，并开发了序列求解器 SeCo 以验证其有效性。
Verification for Timed Automata extended with Unbounded Discrete Data Structures
研究了扩展为无界离散数据结构的时间自动机验证问题的可判定性。更详细地说，我们扩展时间自动机与下推堆栈。通过这种方式，我们获得了一个强大的模型，例如可以用来模拟实时程序与过程调用。这是长期以来已知的，该模型的可达性问题是可判定的。本文的目标是确定语言包含问题和相关问题是可判定的时间下推自动机的子类。
On Decidability Properties of One-Dimensional Cellular Automata
在最近的一篇论文中，Sutner证明了一维元胞自动机$\mathcal{A}$的相空间$\mathcal{S}_\mathcal{A}=(Q^\mathbb{Z}, \longrightarrow)$的一阶理论是可判定的，该元胞自动机的配置是$Q^\mathbb{Z}$的元素，对于有限的一组状态$Q$，其中$\longrightarrow$是“下一个配置关系”。他问这个结果是否可以扩展到一个更有表现力的逻辑。本文证明了这一点。我们首先表明，对于每个一维元胞自动机$\mathcal{A}$，相空间$\mathcal{S}_\mathcal{A}$是一个欧米茄自动结构。然后，应用Kuske和Lohrey最近关于omega-自动结构的结果，可以得出结构$\mathcal{S}_\mathcal{A}$的一阶理论，用一些计数和基数量词扩展，是可判定的。我们给出了一维元胞自动机的一些新的可判定性质的例子。在满射元胞自动机的情况下，从Kuske和Lohrey关于有界度结构的结果可以推出一些更有效的算法。另一方面，我们表明，细胞自动机的情况下，自动图给出了新的结果。
On the Control of Asynchronous Automata
Ramadge和Wonham控制器综合问题的分布式版本的可判定性是一个具有挑战性的公开问题，其中对象和控制器都被建模为异步自动机，并且控制器具有因果记忆。存在三类对象，其具有因果记忆的正确控制器的存在已被证明是可判定的：当动作的依赖图是串并行时，当进程连接地通信时，以及当进程的依赖图是树时。设计了一类具有可判定控制器综合问题的可分解对策，给出了已有的三个可判定性结果的统一证明，并给出了可判定对策的新例子.
The Emptiness Problem for Valence Automata over Graph Monoids
这项工作的研究，在自动机的存储机制，允许可判定性的空虚问题。这个问题是正式使用价自动机，一个抽象的自动机模型，其中的存储机制是由幺半群。对于各种存储机制中的每一种，可以选择一个（通常是无限的）幺半群$M$，使得$M$上的价自动机等价于具有这种存储类型的（单向）自动机。事实上，许多重要的存储机制可以通过有限图定义的幺半群来实现，称为图幺半群。示例包括下推堆栈、部分盲计数器（其表现得像Petri网位置）、盲计数器（其可以获得负值）及其组合。因此，我们研究的图幺半群的空性问题的价自动机是可判定的。图幺半群实现的一个特殊模型是具有下推堆栈的Petri网。对于这些，可判定性是一个长期存在的开放性问题，我们在这里不回答它。然而，如果排除对应于该模型的子图，则可以实现特征化。此外，我们提供了一个描述的存储机制，决策仍然开放。这导致了一个模型，自然推广了下推Petri网和Reinhardt引入的优先级多计数器机。被证明是可判定的情况构成了一个自然的和显然是新的扩展的Petri网与可判定的可达性。最后表明，该模型可以与另一个这样的扩展Atig和Ganty：我们提出了进一步的可判定性结果，包括这两个Petri网扩展。
Interrupt Timed Automata with Auxiliary Clocks and Parameters
时间自动机（ITA）是一种表达性的时间模型，根据级别考虑中断。由于这一特点，这种形式主义是不可比拟的时间自动机。然而，已经获得了一些与可达性和模型检验相关的可判定性结果。我们添加辅助时钟ITA，从而扩大其表达能力，同时保持可达性的可判定性。此外，我们定义了一个参数化版本的ITA，多项式的参数出现在警卫和更新。虽然参数推理与时间模型特别相关，但它经常导致不可判定性结果。我们证明了各种可达性问题，包括“强大的”可达性，是可判定的这个模型，我们给一个固定或可变数量的时钟，水平和参数的复杂性上界。
On Linear Time Decidability of Differential Privacy for Programs with Unbounded Inputs
我们介绍了一个自动机模型，用于描述有趣的类的差分隐私机制/算法，包括已知的机制，从文献。这些自动机可以建模算法，其输入可以是实值查询答案的无界序列。我们考虑的问题，检查是否存在一个常数$d$，使这些自动机所描述的算法是$dε$ -差分隐私的隐私预算参数$ε$的所有正值。我们表明，这个问题可以决定在时间上的线性自动机的大小确定的必要和充分条件的基本图形的自动机。本文的结果是已知的算法与一个无界数量的查询答案从实数集取值的第一个可判定性结果。
The logical strength of Büchi's decidability theorem
本文在弱二阶算术理论 RCA_0 中证明了 Büchi 可判定性定理等价于 Σ^0_2 归纳模式、加法着色 Ramsey 定理及 Büchi 补集定理，并蕴含 McNaughton 确定性定理和有界宽度 König 引理。
Reachability-time games on timed automata
在可达性-时间博弈中，玩家Min和Max选择移动，使得在时间自动机中到达最终状态的时间分别最小化或最大化。Asarin和Maler使用值迭代算法证明了强非Zeno时间自动机上可达时间博弈的可判定性。本文补充他们的工作，提供了一个战略改进算法的问题。由于所提出的策略改进算法解决了所有时间自动机上的可达时间博弈，因此也推广了他们的可判定性结果。精确的计算复杂性解决可达时间游戏也建立：问题是EXPTIME完全的时间自动机至少有两个时钟。
Model Checking Flat Freeze LTL on One-Counter Automata
本文解决了单计数器自动机上平坦冻结线性时序逻辑模型检测的可判定性开放问题，通过归约到带参数化相等性测试的可达性问题并转化为Presburger算术证明其可判定。
On the expressive power of invariants in parametric timed automata
结合硬时序约束和并发性的系统的验证是具有挑战性的。当一些定时常数丢失或未知时，这个挑战变得更加困难。参数定时形式主义，如参数定时自动机（PTA），解决了这样的定时常数（被视为参数）的合成，其中一个属性成立。这样的形式主义是高度表达，但也不可判定，并提出了一些可判定的子类。在这里，我们提出了一个语法限制的PTA组成的删除警卫（限制过渡），只保持不变（限制位置）。虽然这种限制保留了PTA的表达能力（因此也保留了它们的不可判定性），但对约束类型的附加限制不仅允许证明可判定性，而且还允许执行满足可达性的参数估值的精确合成。这种形式主义，乍一看似乎微不足道，因为它受益于可达性问题的可判定性，具有比时间自动机（TA）更好的复杂性，但却受到TA相反享受的整个TCTL逻辑的不可判定性的影响。我们相信我们的形式主义允许一个有趣的权衡之间的可判定性和实际的表现力，因此是有前途的。我们在一个小的案例研究中展示了它的适用性。
On the Complexity of Deciding Call-by-Need
在最近的一篇论文中，我们介绍了一个新的框架，用于研究在项重写中对范式和根稳定形式的按需计算的调用。使用基本树自动机技术和地面树传感器，我们获得了简单的可判定性证明类重写系统，比以前的类定义使用复杂的顺序性概念。在本文中，我们表明，我们可以做没有地面树传感器，以达到可判定性的证明，直接树自动机结构中的措辞。这使我们能够获得更好的复杂度界限。
Linear Intransitive Temporal Logic of Knowledge LTK_r, Decision Algorithms, Inference Rules
本文研究了具有自反不传递时间关系的知识与时间线性逻辑LTK_r。逻辑在语义上被定义为在具有不传递和自反时间二元关系的特殊框架下为真的公式集合。LTK_r -框架是由自反不传递关系$R_T$连接的簇的线性链.簇内的元素通过模仿不同代理的知识的几个等价关系连接。我们研究公式和推理规则的可判定性问题。公式的可判定性来自可判定性w.r.t.为了研究推理规则的可容许性，我们引入了一些特殊的构造性Kripke模型，用于描述推理规则的可容许性。利用一种特殊的赋值可定义技术，我们找到了一个确定LTK_r中可容许推理规则的算法。也就是说，我们证明了逻辑LTK_r是可判定的，且关于推理规则的可容许性是可判定的。
Decidability properties for fragments of CHR
我们研究的可判定性终止的两个方言，类似的Datastrophic语言，定义使用的签名，不允许功能符号（arity >0）。这两种语言都允许在规则体中使用=内置，因此都是建立在支持统一的宿主语言上。然而，每一个都施加了一个进一步的限制。第一种语法只允许范围受限的规则，也就是说，如果变量没有出现在规则的头部，它不允许在规则的主体或保护中使用变量。我们表明，存在一个无限的计算是决定这种方言。相反，第二种方言将规则头部的原子数量限制为1。我们证明了在这种情况下，终止计算的存在是可判定的。这些结果表明，这两种方言的表达能力严格低于图灵机。值得注意的是，没有这些限制的语言（没有函数符号）与图灵机一样具有表达力。
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
我们提出了一个统一的翻译LTL公式到确定性拉宾自动机，有限确定性Büchi自动机，和不确定性Büchi自动机。翻译产生自动机的渐近最佳大小（双或单指数，分别）。所有三种翻译都是从一个纯粹逻辑性质的主定理推导出来的。主定理将公式的语言分解为语言的正布尔组合，这些语言可以通过初等方法转化为ω-自动机。特别是，Safra的，排名，和断点结构中使用的其他翻译是不需要的。
Color Graphs: An Efficient Model For Two-Dimensional Cellular Automata Linear Rules
二维的【形】九邻域矩形元胞自动机规则可以使用规则矩阵、状态转移图、布尔函数、代数范式等多种技术建模。本文介绍了一种新的模型，使用彩色图来建模所有的512条线性规则。因此，本文研究的图论性质与其他研究方法相比，简化了对所有线性规则的分析。
On the Path-Width of Integer Linear Programming
研究整数线性规划的可行性问题。我们表明，任何ILP实例的解决方案可以自然地表示由一个FO-可定义的一类图。对于每一个解，可能有许多图来表示它，然而，其中一个图的路径宽度最多为2n，其中n是实例中变量的数量。由于FO在路宽有界的图上是可判定的，我们得到了ILP的另一个可判定性结果.我们使用的技术强调了一个共同的原则，以证明先前已用于自动机与辅助存储器的可判定性。我们还展示了这个新的结果如何链接到自动机理论和程序验证。
The Sticky Path to Expressive Querying: Decidability of Navigational Queries under Existential Rules
本文研究存在规则下导航查询的可判定性，证明任意有限合一集规则集上正则路径查询不可判定，而粘性规则集上可判定，但轻微扩展RPQ形式会导致不可判定。
Query Answering over Contextualized RDF/OWL Knowledge with Forall-Existential Bridge Rules: Attaining Decidability using Acyclicity (full version)
最近爆发的上下文相关的知识语义网（SW），导致了实现的重要性，四元在SW社区。四元组通过添加RDF三元组的“上下文”的新参数来扩展标准RDF三元组，从而通知推理机区分各种上下文中的知识。虽然这种区别将RDF图中的三元组分成不同的上下文，并允许推理在不同的上下文之间解耦，但需要提供桥接规则来跨这些上下文互操作知识。我们将一组四边形与桥牌规则一起称为四边形系统。本文讨论了四元系统上具有可表达的存在桥规则的查询应答问题。事实证明，在四系统上的查询回答一般是不可判定的。我们推导出一类可判定的四系统，即上下文非循环四系统，查询回答可以使用前向链接。已经为派生类建立了数据和查询蕴涵的组合复杂性的严格界限。
Power of Randomization in Automata on Infinite Strings
概率Büchi自动机（PBA）是随机的，有限状态自动机，处理无限长度的输入字符串。基于为接受概率选择的阈值，可以定义不同的语言类别。在本文中，我们提出了一些结果，澄清了这种机器的力量和他们定义的语言的属性。我们关注的广泛主题如下。我们目前的结果的可判定性和精确的复杂性的空虚，普遍性和语言包容性的问题，这样的机器，从而回答中央使用这些模型在形式化验证的问题。其次，我们对PBAs识别的语言进行了拓扑刻画，证明了虽然一般的PBAs可以识别非正则语言，但在拓扑上，这些语言与ω-正则语言一样简单。最后，我们介绍了层次PBAs，这是PBAs的语法限制形式，易于处理，准确地捕捉类的ω-正则语言。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。