在反应式合成中引入监视器而不付出代价
计算机科学中的逻辑
2021-07-05 v1
摘要
时序合成试图构造满足给定声明式（LTL）公式的反应式程序。实践者发现仅使用声明式规约具有挑战性，并发现结合建模与声明式规约的语言更为有用。合成控制器也可能需要与已有或手动构造的程序协同工作。本文探讨一种方法，其在存在作为监视器的已有行为模型下进行声明式规约合成，且益处在于无需推理监视器的状态空间。我们提出一种以自动机监视器作为LTL公式非重复与重复触发器的形式语言。我们使用带记忆的符号自动机作为触发器，所得语言比现有正则表达式触发器严格更具表达力且更简洁。我们给出该语言的组合式合成流程，其中对监视器状态空间的推理最少。为展示方法优势，我们将其应用于需要计数及对任意长事件序列约束的规约，并可由此见参数化之威力，其在本方法中易于处理。我们提供工具为本语言构造控制器（以符号自动机形式）。
引用
@article{arxiv.2107.00929,
title = {Incorporating Monitors in Reactive Synthesis without Paying the Price},
author = {Shaun Azzopardi and Nir Piterman and Gerardo Schneider},
journal= {arXiv preprint arXiv:2107.00929},
year = {2021}
}