Reducing Bounded Realizability Analysis to Reachability Checking

Realizability verification of reactive system specifications can detect dangerous situations that can arise, which were not expected while drawing the specifications. However, such verification typically involves complex, intricate analyses. The complexity of the realizability problem is 2EXPTIME-complete. To avoid this difficulty, Schewe et al. introduced the notion of bounded realizability. While realizability is the property that a model of a reactive system exists that satisfies a given specification, bounded realizability requires the existence of a model of size k that satisfies the given specification. They presented a method based on satisfiability modulo theories (SMT) for bounded realizability checking. Here, we present a more efficient method for checking bounded realizability. Our method reduces bounded realizability checking to satisfiability (SAT)-based reachability checking and is faster because in many cases, the result is obtained by reachability checking of small steps. We show the complexity of a bounded realizability problem for linear temporal logic (LTL) specifications is NEXPTIME-complete, in which the upper bound is derived from our SAT-encoding technique. We also report experimental results that show the effectiveness of our method.