Efficient Realizability Checking by Modularization of LTL Specifications. (3rd September 2021)

• Record Type: Journal Article
• Authors: Ito, Sohei; Osari, Kenji; Shimakawa, Masaya; Hagihara, Shigeki; Yonezaki, Naoki
• Is Part Of: Computer journal. Volume 65:Number 10(2022)
• Page Start: 2801
• Page End: 2814
• Publication Date: 2021-09-03
• Subjects: realizability -- reactive systems -- compositional algorithm -- clustering algorithm; Computers -- Periodicals; 005.1
• DOI: 10.1093/comjnl/bxab116
• Languages: English
• ISSNs: 0010-4620

Abstract

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.