从理论模可实现性到理论模综合（第一部分）：动态方法
计算机科学中的逻辑
2023-10-13 v1
摘要
反应式综合是利用 LTL 中的时序逻辑规约生成正确控制器的过程，但其应用一直局限于布尔规约。近来，一种布尔抽象技术可将含有理论中文字的 LTL_T 规约翻译为等可实现的 LTL 规约。然而，目前尚无综合过程。在理论模综合中，待综合的系统接收一阶理论 T 中环境变量的赋值，并输出来自 T 的系统变量赋值。本文探讨如何结合从布尔化 LTL 规约得到的静态布尔控制器，以及对可产生 T 中可满足存在公式模型的求解器进行动态查询，来综合出完整的控制器。这是首个实现理论模反应式综合的方法。
引用
@article{arxiv.2310.07904,
title = {From Realizability Modulo Theories to Synthesis Modulo Theories Part 1: Dynamic approach},
author = {Andoni Rodríguez and Cesar Sanchez},
journal= {arXiv preprint arXiv:2310.07904},
year = {2023}
}