在线合成
计算机科学中的逻辑
2021-07-05 v1
摘要
合成（synthesis）自动构造满足给定逻辑规范的实现。本文中，我们研究在线合成问题，其中被合成的实现替换一个已在运行的系统。除满足自身规范外，被合成的实现必须保证从先前实现的正确过渡。这一合成问题版本在始终在线（always-on）应用中高度相关，其中更新在系统运行时发生。为规范新旧实现之间的正确交接，我们引入一种称为 LiveLTL 的线性时序逻辑（LTL）扩展。LiveLTL 规范对两个实现分别定义要求，并确保新实现除自身要求外，还满足旧实现遗留的任何未竟义务。对于 LiveLTL 中的规范，我们证明在线合成问题可在与标准反应式合成相同的复杂度界内求解，即 2EXPTIME。我们的实验显示了从 SYNTCOMP 基准与机器人控制创建的 LiveLTL 规范进行在线合成的必要性。
引用
@article{arxiv.2107.01136,
title = {Live Synthesis},
author = {Bernd Finkbeiner and Felix Klein and Niklas Metzger},
journal= {arXiv preprint arXiv:2107.01136},
year = {2021}
}