基于符号自动机的 DECLARE 反应式合成
形式语言与自动机理论
2022-12-22 v1 计算机科学中的逻辑
摘要
给定在有限迹上解释的线性时序逻辑（LTLf）规范，反应式合成问题要求找到一个可有限表示、可终止的控制器，该控制器对环境不可控动作作出反应以强制实施期望的系统规范。本文首次研究了 DECLARE（LTLf 的一个片段，在理论与实践中广泛用于指定声明式、基于约束的业务流程）的反应式合成问题。我们提供了三重贡献。首先，我们给出该问题的一个朴素双指数时间合成算法。其次，我们展示如何将任意 DECLARE 规范紧凑编码为 LTLf 中等价的纯过去规范，并借此定义一种优化的单指数时间 DECLARE 合成算法。第三，我们通过引入纯过去时序公式到符号确定性有限自动机的新颖翻译，推导出该算法的符号版本。
引用
@article{arxiv.2212.10875,
title = {Reactive Synthesis for DECLARE via symbolic automata},
author = {Luca Geatti and Marco Montali and Andrey Rivkin},
journal= {arXiv preprint arXiv:2212.10875},
year = {2022}
}