Efficient Realizability Checking by Modularization of LTL Specifications
Efficient Realizability Checking by Modularization of LTL Specifications
复制标题
通过零担规范模块化进行高效的可实现性检查
DOI：
10.1093/comjnl/bxab116
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Yonezaki Naoki
中科院分区：
文献类型：
--
作者：
Ito Sohei;Osari Kenji;Shimakawa Masaya;Hagihara Shigeki;Yonezaki Naoki
可实现性是反应式系统规范的一个重要要求。反应式系统与环境交互并响应输入事件。可实现性确保反应式系统按照指定的方式运行，而不管其环境如何提供输入。通常，反应式系统规范使用线性时序逻辑（LTL）给出，并且可以对其进行测试以确定规范是否可实现。然而，LTL规格说明的可实现性问题是2 EXPTIME-完全的，这阻碍了其应用到大规模系统。在本文中，我们提出了一种模块化方法来减轻这种计算挑战。
Realizability is an important requirement for reactive system specifications. A reactive system interacts with an environment and responds to input events. Realizability ensures the reactive system behaves as specified, no matter how its environment provides input. Typically, reactive system specifications are given using linear temporal logic (LTL), and they can be tested to ascertain whether the specification is realizable. However, the LTL specification realizability problem is 2EXPTIME-complete, which hinders its application to large-scale systems. In this article, we present a modularization method to mitigate this computational challenge.
影响因子：
1.1
作者：
Ito, Sohei;Ichinose, Takuma;Yonezaki, Naoki
通讯作者：
Yonezaki, Naoki
特刊：第26届国际并发理论会议（CONCUR 2015）论文精选
影响因子：
0.6
作者：
L. Aceto;David de Frutos
通讯作者：
David de Frutos