Safety LTL 综合的符号化方法
计算机科学中的逻辑
2020-08-18 v2
摘要
时序综合是使用系统行为的声明式规范，自动设计一个与环境交互的系统。用于提供此类规范的一种流行语言是线性时序逻辑，或 LTL。然而，一般情况下的 LTL 综合在实践中一直是一个难以解决的难题。正因如此，许多工作专注于为 LTL 的特定片段开发综合程序，这些片段的综合问题更容易。在本工作中，我们关注 Safety LTL，这里将其定义为否定范式 (NNF) 中无 Until 的 LTL 片段，并证明其表达了安全 LTL 公式的一个片段。该片段的内在动机是观察到，在许多情况下仅说明某件“好事”最终会发生是不够的，我们需要说明它将在何时发生。我们在此证明，Safety LTL 综合在算法上比 LTL 综合显著更简单。我们以两种方式利用了这种简单性：首先描述了一种基于归约到 Horn-SAT 的显式方法，该方法在博弈图大小上可在线性时间内求解；然后通过一种高效的符号构造，允许一种基于 BDD 的符号化方法，其性能显著优于现有的 LTL 综合工具。
引用
@article{arxiv.1709.07495,
title = {A Symbolic Approach to Safety LTL Synthesis},
author = {Shufang Zhu and Lucas M. Tabajara and Jianwen Li and Geguang Pu and Moshe Y. Vardi},
journal= {arXiv preprint arXiv:1709.07495},
year = {2020}
}