首页/论文/2307.04499

arXiv 2307.044992023-07-10cs.LO

数据字的一阶综合问题再探

First order synthesis for data words revisited

Julien Grange, Mathieu Lehaut

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

AI总结：

本文重新研究数据字上一阶逻辑片段的综合问题，明确划定了可判定与不可判定的精确边界。

摘要：

我们继续研究数据字上一阶逻辑片段的可综合问题，并精确刻画可判定性与不可判定性之间的边界。

英文摘要：

We carry on the study of the synthesis problem on data words for fragments of first order logic, and delineate precisely the border between decidability and undecidability.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

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

继续探索

相关论文

数据字上前缀一阶逻辑的合成

Synthesis for prefix first-order logic on data words

本文研究了无限参与者分布式系统的反应式合成问题，通过数据字建模执行，并采用实现有限顺序的前缀一阶逻辑片段作为规范，最终证明了该合成问题的可判定性。

2024-04-22cs.LO

重访物理感知综合：用基本逻辑门布局指导工艺映射

Physically Aware Synthesis Revisited: Guiding Technology Mapping with Primitive Logic Gate Placement

针对VLSI设计前后端迭代成本高的问题，提出PigMAP框架，通过线长驱动的工艺映射生成物理友好网表，含性能和功耗两种模式，在EPFL基准上实现延迟与功耗的优化。

2024-08-15cs.LO

具有综合功能的词转换逻辑

Logics for Word Transductions with Synthesis

我们引入了一个逻辑，称为LT，来表达属性的转换，即从输入到输出（有限）字的二元关系。在LT中，输入/输出依赖性通过一个origin函数来建模，该函数与输出单词的任何位置相关联，即它所源自的输入位置。LT非常适合表达关系（不一定是函数），并且可以表达所有规则的函数转换，即例如由确定性双向转换器定义的转换。尽管它的高表达能力，LT有可判定的可满足性和等价性问题，与紧的非初等和初等的复杂性，取决于特定的LT-公式表示。我们的主要贡献是一个合成结果：从LT中定义的任何转换R，可以合成一个规则的功能转换f，使得对于R域中的所有输入词u，f被定义并且（u，f（u））属于R。因此，我们得到任何功能转导是正规的当且仅当它是LT-可定义的。我们还研究了LT的几个扩展的算法和表达特性，并明确了转换和数据字之间的对应关系。作为一个副结果，我们得到了一个新的数据字的可判定逻辑。

2018-05-30cs.FLcs.LO

Church 综合问题的 Curry-Howard 方法

A Curry-Howard Approach to Church's Synthesis

本文通过 Curry-Howard 对应关系，引入直觉主义变体 SMSO 并借助自动机可实现性模型，为 Church 综合问题提供了可靠且完备的算法求解方法。

2019-12-06cs.LO

有限字上部分定义域的加权规格综合

Synthesis from Weighted Specifications with Partial Domains over Finite Words

本文从定量指标出发研究了终止反应系统的综合问题。这种系统被建模为有限换能器，其执行被表示为$(I\times O)^*$中的有限字，其中$I,O$分别是输入和输出符号的有限集合。加权规格$S$分配一个有理值（或$-\infty$）到$(I\times O)^*$中的单词，并且我们考虑三种用于合成的目标，即阈值目标，其中系统的执行被要求高于某个给定阈值，最佳值和近似目标，其中要求系统通过提供产生最佳值和$\varepsilon$的输出符号来尽可能地执行。最佳值分别为w.r.t. $S$。我们建立了一个景观的可判定性的结果，这三个目标和加权规范与部分域的有限的话，由确定性加权自动机配备和，贴现和平均措施。由此产生的目标是不定期的一般情况下，我们开发了一个无限的游戏框架来解决相应的合成问题，即（加权）关键前缀游戏类。

2021-03-09cs.FLcs.GTcs.LO

数据字上一阶逻辑片段的参数化综合

Parameterized Synthesis for Fragments of First-Order Logic over Data Words

研究了具有参数化进程数的系统的综合问题。在Church的经典案例中，系统根据到目前为止运行的程序选择动作，目的是满足给定的规范。困难在于，与此同时，环境执行系统无法控制的操作。与固定的有限字母表的情况相反，这里我们考虑参数化字母表的情况。字母表反映了静态但未知的进程的数量。综合问题然后问是否有一个有限数量的过程，系统可以满足规范。这种变体对于非常有限的逻辑已经是不可判定的。因此，我们考虑一个一阶逻辑没有顺序的词的位置。我们表明，即使在这种限制的情况下，合成是不可判定的，如果系统和环境都可以访问所有的进程。另一方面，我们证明了问题是可判定的，如果环境只能访问有限数量的进程。在这种情况下，甚至有一个截止值，这意味着它足以检查有限数量的过程架构来解决综合问题。

2019-10-31cs.FLcs.LO

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

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

Synthesizing Computable Functions from Rational Specifications over Infinite Words

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

2024-02-08cs.FLcs.LO

活性验证与综合：递归程序的新算法

Liveness Verification and Synthesis: New Algorithms for Recursive Programs

我们考虑递归程序的活性验证和活性合成问题。活性验证问题（LVP）是判定给定的omega-正则语言是否包含给定的omega-上下文无关语言。活性合成问题（LSP）是计算一个策略，使得当沿着该策略进行给定的omega-上下文无关游戏时，保证导出给定omega-正则语言中的单词。这两个问题分别是EXPTIME完全问题和EXPTIME完全问题。我们的贡献是新的算法具有最佳的时间复杂度。对于LVP，我们概括了最近的拉索发现算法（也称为拉姆齐算法）从有限递归程序。对于LSP，我们概括了最近的摘要为基础的算法从有限到无限的话。Lasso查找和摘要已被证明在有限状态和有限字设置的许多实现中是有效的。

2017-01-11cs.FLcs.LO

实时的合成很难！

Real-Time Synthesis is Hard!

研究度量区间时态逻辑（MITL）中给定规范的反应式综合问题（RS）。已知RS在非常一般的情况下是不可判定的，但仅在无限词上;并且只有非常严格的BRRS子情况是可判定的（参见D 'Souza et al.和Bouyer et al.）。本文对MITL综合的可判定性边界进行了精确化。我们表明RS是不可判定的有限的话太，并提出了一个景观的限制（无论是在逻辑上和可能的控制器），仍然是不可判定的。从积极的方面来看，我们重新审视了BRRS，并引入了一个高效的动态算法来解决它。

2016-06-22cs.FLcs.LO

无限字的可计算正则函数的综合

Synthesis of Computable Regular Functions of Infinite Words

本文针对正则函数的可计算性综合问题，证明正则函数的可计算性等价于连续性，建立连续性通用刻画，证明有理与正则函数的可计算性可判定，其中有理函数可在NLogSpace内判定，还刻画了一致连续性并关联一致可计算性。

2024-09-18cs.FLcs.LO

定期模型检验再访（技术报告）

Regular Model Checking Revisited (Technical Report)

在这方面的贡献，我们重温定期模型检验，一个强大的框架，已成功地应用于验证的无限状态系统，特别是参数化系统（并发系统与任意数量的进程）。我们提供了一个重新制定的定期模型检验与长度保持传感器在存在的二阶理论在自动结构。我们认为，这是一个自然的配方，使我们能够利用强大的综合技术，已被广泛研究的软件验证社区。更确切地说，在这个公式中，一阶部分表示所需正确性属性的验证条件（我们有完整的求解器），而存在量化的二阶变量表示要合成的关系。我们表明，许多有趣的正确性可以用这种方式制定，例如安全，活性，双相似性，和游戏。更重要的是，我们表明，这种新的配方允许新的有趣的基准（和旧的定期模型检验基准，以前被认为是困难的），特别是在参数化系统验证领域，要解决。

2021-11-21cs.FLcs.LO

认知协议综合的自动机技术

Automata Techniques for Epistemic Protocol Synthesis

在这项工作中，我们的目标是应用自动机技术的动态认知逻辑，如认知规划研究的问题。要做到这一点，我们首先注意到，重复执行广告无穷大的命题事件模型从一个初始的认知模型产生的关系结构，可以用自动机表示。这种对应关系，再加上最近的结果，统一的战略，使我们能够给一个替代的可判定性证明的认知规划问题的命题事件，作为副产品准确的上界，其时间复杂度，并有可能合成一个有限词自动机，描述了所有的解决方案计划。事实上，使用自动机技术使我们能够解决一个更普遍的问题，我们引入并称之为认知协议合成。

2014-04-03cs.LO

由概率分量合成的复杂性

The Complexity of Synthesis from Probabilistic Components

综合问题要求从系统的规范自动构造系统。在传统的设置中，系统是“从头开始构建的”，而不是由可重用的组件组成。然而，这在实践中是罕见的，几乎每一个重要的软件系统都严重依赖于可重用组件库的使用。最近，Lustig和Vardi从可重用组件库中引入了控制流和控制流合成。他们证明了控制流综合是不可判定的，而控制流综合是可判定的。Nain、Lustig和Vardi考虑了从概率组件库中进行控制流合成的问题，并证明了该问题对于定性分析是可判定的（要求满足概率1的规范）。我们的主要贡献控制流合成的概率组件是建立更好的复杂性边界的定性分析问题，并表明，更一般的定量问题是不可判定的。对于定性分析，我们表明，问题（一）是EXPTIME-完全的规范时，作为一个确定性的奇偶校验字自动机，提高了以前已知的2 EXPTIME上限;（二）属于UP $\cap$ coUP和奇偶博弈硬，当规范是直接作为一个奇偶校验条件的组件，提高了以前已知的EXPTIME上限。

2015-02-17cs.LO

基于递归组件库的综合

Synthesis from Recursive-Components Libraries

综合是根据系统的规范自动构造系统。在经典的综合算法中，它总是假设系统是“从头开始构建”，而不是由可重用的组件组成。当然，这在现实生活中很少发生。在现实生活中，几乎每一个重要的商业软件系统都严重依赖于使用可重用组件库。此外，其他上下文，如Web服务编排，可以建模为从组件库合成系统。2009年，我们引入了基于可重用组件库的LTL合成。在这里，我们扩展的工作和学习的综合从组件库与“调用和返回”的控制流结构。这种控制流结构在软件系统中非常常见。我们定义的嵌套词时序逻辑（NWTL）的递归组件库，其中NWTL是一个规范的形式主义，比LTL更丰富，这是适合于“调用和返回”的计算合成的问题。我们解决了这个问题，提供了一个综合算法，并显示该问题是2EXPTIME完全的，作为标准的综合。

2011-06-07cs.LOcs.SE

一种多范式语言用于反应合成

A multi-paradigm language for reactive synthesis

California Institute of Technology（加州理工学院）；Jet Propulsion Lab, Caltech（加州理工学院喷气推进实验室）

本文提出一种整合命令式与声明式元素的反应合成问题描述语言，通过游戏求解器输入结构化编程语言，支持序列约束表达，结合LTL片段和过去LTL实现高效合成。

2016-02-03cs.LOcs.PLcs.SY