arXiv 1606.071242016-06-22cs.LOcs.FL

实时的合成很难！

Real-Time Synthesis is Hard!

Thomas Brihaye, Morgane Estiévenart, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege, Nathalie Sznajder

摘要：

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

英文摘要：

We study the reactive synthesis problem (RS) for specifications given in Metric Interval Temporal Logic (MITL). RS is known to be undecidable in a very general setting, but on infinite words only; and only the very restrictive BRRS subcase is known to be decidable (see D'Souza et al. and Bouyer et al.). In this paper, we precise the decidability border of MITL synthesis. We show RS is undecidable on finite words too, and present a landscape of restrictions (both on the logic and on the possible controllers) that are still undecidable. On the positive side, we revisit BRRS and introduce an efficient on-the-fly algorithm to solve it.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

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

继续探索

相关论文

硬布尔约束下期望成本最小化及其在定量综合中的应用

Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis

在布尔合成中，我们给出了一个LTL规范，目标是构建一个转换器，在对抗环境中实现它。通常，一个规范既包含对抗性环境下应该满足的布尔需求，也包含多值组件，这些组件指的是满足的质量，并且我们希望在概率环境下最小化其预期成本。在这项工作中，我们研究，第一次，平均支付游戏中，系统的目标是在概率环境中的预期成本最小化，同时肯定满足$ω$ -经常性条件对抗的环境。我们考虑的情况下，$ω$ -正则条件是作为一个奇偶目标或由LTL公式。我们表明，在一般情况下，最优策略不需要存在，而且，极限值不能近似的有限记忆策略。因此，我们专注于计算的极限值，并给出严密的复杂性界合成$ε$ -最优策略的有限内存和无限内存的战略。我们表明，我们的游戏自然出现在各种情况下的合成与布尔和多值目标。除了直接应用之外，在与某些行为的成本和回报的合成中，它允许我们计算$ω$的最小感测成本-常规规格-一种质量度量，其中我们寻找最小化从输入读取的预期信号数量的传感器。

2016-04-24cs.FLcs.LO

布尔函数综合的难点

What's hard about Boolean Functional Synthesis

给定布尔输入和输出之间的关系规范，布尔函数合成的目标是将每个输出合成为输入的函数，以满足规范。在本文中，我们首先表明，除非复杂性理论中的一些硬结构被证伪，否则布尔函数合成必须生成指数大小的Skolem函数，从而在最坏的情况下需要指数时间。既然这种固有的困难，我们应该做些什么来解决这个问题呢？我们提出了一个两阶段的布尔函数合成算法，其中第一阶段是有效的时间和合成函数的大小，并解决了绝大多数的基准。为了解释这种令人惊讶的良好性能，我们提供了一个充分条件，在该条件下，第一阶段必须产生精确的正确答案。当这个条件失败时，第二阶段建立在第一阶段的结果上，可能需要指数时间，并在最坏的情况下生成指数大小的函数。详细的实验评估表明，我们的算法比大多数基准测试的最先进的技术表现更好。

2018-05-18cs.LO

鲁棒控制器的设计与无功综合

Specification and Reactive Synthesis of Robust Controllers

本文研究了从区间时序逻辑QDDC中给出的正则性质的逻辑规范综合鲁棒控制器的问题。我们的规范包括硬鲁棒性和软鲁棒性。在这里，硬鲁棒性保证承诺在用户指定的放松（弱化）假设下的不变性。一个系统的框架，逻辑上指定的假设弱化的公式，称为鲁棒性标准，提出。软鲁棒性涉及控制器保持尽可能多的输入的承诺的能力，而不管任何假设。我们提出了一个统一的方法来合成一个强大的控制器，保证指定的硬鲁棒性，它优化指定的软鲁棒性。该方法使用DCSynth工具实现，该工具提供软需求优化的控制器合成。通过一个同步总线仲裁器的案例研究，我们的实验表明，硬鲁棒性标准以及软鲁棒性的综合控制器的能力，以满足承诺的影响“尽可能多”。分析了最坏情况和预期情况下的行为。

2019-05-27cs.LO

基于线性时序逻辑的协调程序综合

Synthesis of coordination programs from linear temporal logic

本文提出了一种方法，用于合成一个反应式程序，协调一组其他反应式程序的动作，使组合系统满足其所需的长期行为的时间规范。传统上，电抗合成已被应用于有状态硬件电路的构造。这项工作的动机是应用到其他领域，如物联网（物联网）和机器人，在那里有必要协调多个传感器，设备和机器人的行动。数学模型将这些实体表示为Hoare CSP模型中的单个过程。给定一个交互实体网络（称为\emph{environment}）和一个长期行为的时间规范，该合成方法构建一个\emph{coordinator}过程（如果存在），该过程指导环境实体的动作，使得组合系统无死锁并满足给定规范。主要的技术挑战在于，由于环境中的非确定性以及对协调器隐藏的环境动作，协调器可能仅具有环境状态的\emph{partial knowledge}。这是第一个方法来处理这两个来源的部分知识，这样做的任意线性时序逻辑规范。结果表明，协调综合问题是\PSPACE -硬的环境的大小。一个原型实现是能够合成紧凑的解决方案，一些协调问题。

2019-11-10cs.FLcs.LOcs.PL

参数化时态逻辑的分布式综合

Distributed Synthesis for Parameterized Temporal Logics

我们认为，在参数化的时间逻辑，如PROMPT-LTL，它扩展LTL的时间运营商配备了参数，约束其范围的规范的分布式实现的合成。对于单过程综合，这是公认的，这样的参数扩展不会增加最坏情况下的复杂性。对于同步分布式系统，我们表明，尽管是更强大的，PROMPT-LTL的可实现性问题并不比它的LTL对应。对于异步系统，我们必须表达调度假设，因此考虑一个假设保证合成问题。由于异步分布式综合对于LTL已经是不可判定的，我们给出了基于有界综合的PROMPT-LTL假设保证综合问题的半判定过程。最后，我们证明了我们的结果扩展到更强的逻辑PLTL和PLDL。

2018-02-26cs.GTcs.LO

基于轨迹抽象精化的实时的程序验证与参数综合

Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction

本文研究了实时的【形】系统的安全性验证与综合问题。我们介绍实时的【形】程序，这些程序由可以执行离散和实值变量赋值的指令组成。它们足够通用，可以捕获有趣的时间系统类，如时间自动机，秒表自动机，时间（d）Petri网和混合自动机。我们提出了一种使用轨迹抽象细化的半算法来解决实时的【形】程序的可达性验证问题和参数综合问题。所有提出的算法已经实施，我们已经进行了一系列的实验，比较我们的新方法的性能，以国家的最先进的工具，在经典的可达性，鲁棒性分析和参数合成定时系统。我们表明，我们的新方法提供了解决方案，这些问题是无法解决的，目前最先进的工具。

2020-07-21cs.FLcs.LOcs.SY

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

Syntroids：使用时序逻辑规范为FPGA合成游戏

Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications

我们提出了Syntroids，一个案例研究的时间逻辑规范的硬件自动合成。Syntroids是一款在FPGA上实现的太空射击街机游戏，其中控制流架构已完全在时间流逻辑（TSL）中指定，并使用反应式合成实现。TSL是最近引入的一种分离控制和数据的时态逻辑。这导致了可扩展的合成，因为合成过程的成本与处理数据的复杂性无关。在这个案例研究中，我们报告我们的经验与基于TSL的开发的Syntroids游戏和实现质量与合成相比，手动编程。我们还讨论了解决和开放的挑战，目前可用的合成工具。

2021-01-18cs.ARcs.LO