基于有限时域规约的反应式合成混合组合推理
计算机科学中的逻辑
2020-02-19 v3 人工智能
形式语言与自动机理论
摘要
LTLf 合成是从 LTLf 表达的有限时域行为高层描述自动构造反应式系统。迄今为止，LTLf 公式到确定性有限状态自动机（DFA）的转换已被认为是合成可扩展性的主要瓶颈。近期研究也表明 DFA 状态空间的大小在合成中同样起着关键作用。因此，有效解决合成瓶颈需要转换在时间和内存上高效，并防止状态空间爆炸。然而，当前基于显式状态表示或符号状态表示的转换方法在规模上无法充分满足这些需求：显式状态方法生成最小 DFA 但因昂贵的 DFA 最小化而缓慢；符号状态表示虽简洁，但因缺乏 DFA 最小化而生成极大的状态空间，连其符号表示也无法补偿该膨胀。本文提出一种用于转换的混合表示方法。该方法同时利用状态空间的显式与符号表示，有效发挥二者互补优势。由此，我们提供了一种满足全部三项需求的 LTLf 到 DFA 转换技术，从而解决瓶颈。在转换与合成基准上的综合实证评估支持了混合方法的优越性。
引用
@article{arxiv.1911.08145,
title = {Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications},
author = {Suguman Bansal and Yong Li and Lucas M. Tabajara and Moshe Y. Vardi},
journal= {arXiv preprint arXiv:1911.08145},
year = {2020}
}
备注
Accepted by AAAI 2020. Tool Lisa for (a). LTLf to DFA conversion, and (b). LTLf synthesis can be found here: https://github.com/vardigroup/lisa