数据字转换器的合成
摘要：反应式综合中的目标是根据系统的反应性和非终止的输入/输出行为的规范自动生成实现。规范通常被建模为关于无限信号序列（ω-words）的逻辑公式或自动机，而实现则表示为传输器。在经典设置中，假设信号集是有限的。本文中，我们考虑使用数据ω-words，即由无限字母表构成的字。在这种情况下，我们研究分别作为自动机和传输器给出的规范和实现，这些规范和实现都有一个有限的寄存器集。根据规范是否是非确定性、全局性或确定性以及实现的寄存器数量是否给定，我们考虑不同的情况。在无界环境中，我们证明了对于非确定性和全局性规范来说是不可判定的，而对于确定性规范来说可以恢复可判定性。在有界环境中，对于非确定性规范仍然是不可判定的，但可以通过禁止对输入数据进行测试来恢复可判定性。我们用于证明后一种结果的通用技术使我们能够重新证明一些已知的结果，即对于全局规范的有界综合是可判定的。
作者：L''eo Exibard, Emmanuel Filiot, Pierre-Alain Reynier
论文ID：1905.03538
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-06-22