Efficient Realizability Checking by Modularization of LTL Specifications. (3rd September 2021) - Ito, Sohei; Osari, Kenji; Shimakawa, Masaya; Hagihara, Shigeki; Yonezaki, Naoki
Abstract: 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.