首页/论文/0801.0537

arXiv 0801.05372008-01-03cs.LOmath.LO

具有极大拓扑复杂性的无穷实迹有理语言

On Infinite Real Trace Rational Languages of Maximum Topological Complexity

Olivier Finkel, Jean-Pierre Ressayre, Pierre Simonnet

发表信息：: Zapiski Nauchnyh Seminarov POMI 316 (2004) 205-223

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

我们考虑无限实迹的集合，在一个依赖字母表（Gamma，D）没有孤立的字母，配备了前缀度量诱导的拓扑。然后，我们证明了所有无限实迹的有理语言都是解析集，并且存在一些无限实迹的有理语言是解析的但不是博雷尔集，甚至是Sigma^1_1-完备的，因此具有最大可能的拓扑复杂性。

英文摘要：

We consider the set of infinite real traces, over a dependence alphabet (Gamma, D) with no isolated letter, equipped with the topology induced by the prefix metric. We then prove that all rational languages of infinite real traces are analytic sets and that there exist some rational languages of infinite real traces which are analytic but non Borel sets, and even Sigma^1_1-complete, hence of maximum possible topological complexity.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

基于终性的无限迹：一种层论方法

Infinite Traces by Finality: a Sheaf-Theoretic Approach

本研究针对Kleisli范畴中终共代数无法通用刻画无限迹语义的问题，提出结合Kleisli范畴、序数层与受保护（余）递归的层论框架，引入受保护行为函子并证明温和条件下其终共代数可直接刻画无限迹。

2025-07-30cs.LO

正则Ω语言中无穷后对应问题的高度不可判定性在有理关系中的三个应用

Three Applications to Rational Relations of the High Undecidability of the Infinite Post Correspondence Problem in a Regular omega-Language

Harel在[Har 86]中指出，“人们可以定义$Σ_1^1$ -著名的Post Correspondence Problem的完全版本”。我们首先给出了这个结果的一个完整的证明，表明在一个正规的$ω$ -语言的无限后对应问题是$Σ_1^1$ -完全的，因此位于算术层次之外，高度不可判定。我们从这个结果推断，它是$Π_1^1$ -完全的，以确定是否两个给定的无穷有理关系是不相交的。然后证明了有限状态Büchi变换器实现的$ω$ -有理函数的两个判定问题之间存在着惊人的差距。事实上Prieur证明在[Pri 01，Pri 02]，这是决定是否一个给定的$ω$ -有理函数是连续的，而我们在这里表明，它是$Σ_1^1$ -完全确定是否一个给定的$ω$ -有理函数至少有一个点的连续性。其次证明了判定给定$ω$ -有理函数的连续集是否是$ω$ -正则的是$Π_1^1$ -完全的。这给出了[CFS 08]中证明为不可判定的两个问题的精确复杂度。

2011-07-29cs.CCcs.LOmath.LO

从无限词上的有理规范合成可计算函数

Synthesizing Computable Functions from Rational Specifications over Infinite Words

本文研究从无限词有理规范合成可计算函数，证明一般情形不可判定，但对确定性有理规范子类可判定且为ExpTime完全，并给出基于奇偶博弈的可靠归约方法。

2024-02-08cs.FLcs.LO

无限迹和活性的Büchi型

Büchi Types for Infinite Traces and Liveness

我们开发了一个新的类型和效果系统的基础上Büchi自动机捕获有限和无限的痕迹产生的程序在一个小的语言，允许非确定性的选择和无限递归。有两个关键的技术贡献：（a）基于Büchi自动机定义的等价关系的抽象，Büchi抽象;（b）一个新的类型和效果系统，以正确地捕获无限的痕迹。我们展示了如何Büchi抽象适合抽象的解释框架，并显示健全性和完整性。

2014-01-20cs.LOcs.PL

论升级的合理性

On the Rationality of Escalation

升级是无限博弈的一个典型特征。因此，为研究无限数学结构而设计的工具，也就是那些从共归纳中推导出来的工具是必不可少的。在这里，我们使用共归纳，或反向共归纳（以显示其与有限博弈的相同概念的连接），以仔细和正式研究的无限博弈，特别是那些被称为美元拍卖，这被认为是升级的范式。不像什么是公认的，我们表明，假设其他代理人将永远停止，投标是理性的，因为它会导致一个子博弈完美均衡。我们证明了这不是唯一的理性策略（唯一的子博弈完美均衡）。事实上，如果一个行动者停下来，并且每走一步都会停下来，我们就可以说他也是理性的，只要他承认他的对手永远不会停下来，因为这对应于一个子博弈完美均衡。令人惊讶的是，在无限美元拍卖博弈中，双方在每一步都停止的行为不是纳什均衡，因此不是子博弈完美均衡，因此不是理性的。

2010-04-29cs.GTcs.LO

泡沫是理性的

Bubbles are rational

正如我们使用无限序贯博弈理论中的均衡概念所展示的那样，泡沫和升级对于相信无限世界的经济和环境代理人来说是合理的。这违背了一个自我调节、明智和和平的经济平衡的愿景。换句话说，在这种情况下，均衡不是稳定的同义词。我们试图从这一陈述中得出方法论的结论和一种新的经济学方法。对于经济主体的心智（认知心理学的一个概念），我们建议在无限博弈中加入共归纳来进行适当的推理。这样，我们就完善了理性的概念。

2013-05-01cs.GTcs.LOq-fin.GN

更多相关论文收起更多论文

无限状态系统迹包含的抽象加细

Abstraction Refinement for Trace Inclusion of Infinite State Systems

\emph{data automaton}是一个有限自动机，配备了在无限数据域范围内的变量（计数器或寄存器）。数据自动机的轨迹是在自动机的执行期间由计数器取得的字母符号和值的交替序列。本文所解决的问题是包含在这样的自动机识别的痕迹（数据语言）之间的集合。由于该问题在一般情况下是不可判定的，我们给出了一个基于抽象加细的半算法，该算法被证明是可靠的和完备的，但不能保证其终止性。我们已经实现了我们的技术在一个~原型工具，并在几个非平凡的例子显示出可喜的成果。

2015-10-21cs.FLcs.LO

上下文相关语言、有理图和决定论

Context-Sensitive Languages, Rational Graphs and Determinism

我们调查家庭的无限自动机上下文敏感的语言。一个无限自动机是一个有两组初始和最终顶点的无限标记图。它的语言是所有标记从初始顶点到最终顶点的路径的词的集合。在2001年，Morvan和Stirling证明了有理图接受初始和最终顶点的有理集之间的上下文敏感语言。这一结果后来被扩展到子家庭的合理图定义的更严格的类别的传感器。语言<br><br>我们的贡献是提供上述结果的句法和自包含的证明，当早期的结构依赖于一个非平凡的范式的上下文相关的语法定义的Penttonen在20世纪70年代。这些新的证明技术使我们能够通过考虑由传感器类型、图的度或初始顶点集的大小的限制定义的几个子族来总结和细化这些结果。

2006-07-19cs.LO

Parikh's theorem for infinite alphabets

We investigate commutative images of languages recognised by register automata and grammars. Semi-linear and rational sets can be naturally extended to this setting by allowing for orbit-finite unions instead of only finite ones. We prove that commutative images of languages of one-register automata are not always semi-linear, but they are always rational. We also lift the latter result to grammars: commutative images of one-register context-free languages are rational, and in consequence commutatively equivalent to register automata. We conjecture analogous results for automata and grammars w…

2021-04-24cs.FLcs.LO

Type-based Enforcement of Infinitary Trace Properties for Java

A common approach to improve software quality is to use programming guidelines to avoid common kinds of errors. In this paper, we consider the problem of enforcing guidelines for Featherweight Java (FJ). We formalize guidelines as sets of finite or infinite execution traces and develop a region-based type and effect system for FJ that can enforce such guidelines. We build on the work by Erbatur, Hofmann and Zălinescu, who presented a type system for verifying the finite event traces of terminating FJ programs. We refine this type system, separating region typing from FJ typing, and use ideas o…

2021-07-23cs.LOcs.PL

采用有限迹技术的无限迹目标：将LTL转换为LTLf+

Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+

本研究提出首个从LTL到LTLf+的线性转换方法，将LTL归一化为Manna-Pnueli层次的反应片段，保留LTLf+的优势且无渐近代价，可将LTLf+技术应用于更多AI问题。

2026-08-04cs.AIcs.FLcs.LO