Towards Efficient Implementation of Realizability Checking for Reactive System Specifications

Realizability checking is used to detect flaws in reactive system specifications that are difficult for humans to find. However, these checks are computationally costly. To address this problem, researchers have studied efficient methods for implementing such checking procedures. In this paper, we propose a new implementation method of realizability checking. While symbolic approaches have been adopted in many previous methods, we take a partially symbolic approach, in which binary decision diagrams (BDDs) are used partially. We developed a prototype realizability checker based on our method, and experimentally compared it to tools based on other implementation methods. Our prototype was efficient in comparison to the other tools.