Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step for every sequence of inputs, such that the LTL formula is satisfied. In this paper, we investigate the notion of dependent variables in the context of reactive synthesis. Inspired by successful pre-processing steps in Boolean functional synthesis, we define dependent variables as output variables that are uniquely assigned, given an assignment, to all other variables and the history so far. We describe an automata-based approach for finding a set of dependent variables. Using this, we show that dependent variables are surprisingly common in reactive synthesis benchmarks. Next, we develop a novel synthesis framework that exploits dependent variables to construct an overall synthesis solution. By implementing this framework using the widely used library Spot, we show that reactive synthesis using dependent variables can solve some problems beyond the reach of several existing techniques. Further, among benchmarks with dependent variables, if the number of non-dependent variables is low (at most 3 in our experiments), our method is able outperform all state-of-the-art tools for synthesis.

翻译：给定一个覆盖输入和输出变量的线性时序逻辑（LTL）公式，反应式合成要求我们设计一个确定性的Mealy机，该机器在每一时间步为每一输入序列提供输出值，使得LTL公式得到满足。本文研究了反应式合成中依赖变量的概念。受布尔函数合成中成功预处理步骤的启发，我们将依赖变量定义为：给定当前所有其他变量的赋值及其历史轨迹，输出变量的取值被唯一确定。我们提出了一种基于自动机的方法来寻找依赖变量集合，并据此发现依赖变量在反应式合成基准测试中出乎意料地普遍存在。接着，我们开发了一种利用依赖变量构建整体合成方案的新型合成框架。通过使用广泛应用的Spot库实现该框架，我们证明基于依赖变量的反应式合成能够解决若干现有技术难以处理的问题。此外，在包含依赖变量的基准测试中，当非依赖变量数量较少（实验中不超过3个）时，我们的方法性能优于所有当前最先进的合成工具。