一种用于反应式安全规范可实现性与综合的表方法

我们引入一种表决策方法，用于判定以 LTL 安全片段（包含有界未来时序算子）表达的规范的可实现性。时序与模态逻辑的表决策过程在可满足性、将时序公式翻译为等价 Büchi 自动机以及模型检测（给定规范与系统）方面已被充分研究。然而，据我们所知，尚无针对反应式综合问题的表方法研究。反应式综合始于将命题变量划分为环境控制变量与系统控制变量的规范，其目标是自动生成一个对所有环境均保证该规范成立的系统。可实现性即判定是否存在这样一个系统的决策问题。本文提出一种判定安全规范可实现性的方法，并由此可提取（即综合）出正确系统（在规范可实现的情况下）。我们的方法可轻易扩展以处理更丰富的域（整数等）和时序算子中的界，而这是基于自动机的综合方法所无法做到的。