Many fatal accidents involving safety-critical reactive systems have occurred in unexpected situations that were not considered during the design and test phases of development. To prevent such accidents, reactive systems should be designed to respond appropriately to any request from an environment at any time. Verifying this property during the specification phase reduces development reworking. This property of a specification is commonly known as realizability. Realizability checking for reactive system specifications involves complex and intricate analysis. The complexity of realizability problems is 2EXPTIME-complete. To detect typical simple deficiencies in specifications efficiently, we introduce the notion of bounded strong satisfiability (a necessary condition for realizability), and present a method for checking this property. Bounded strong satisfiability is the property that, for all input patterns represented by loop structures of a given size k, there is a response that satisfies a given specification. We report a checking method based on a satisfiability solver, and show that the complexity of the bounded strong satisfiability problem is co-NEXPTIME-complete. Moreover, we report experimental results showing that our method is more efficient than existing approaches.

This paper focuses on verification for reactive system specifications. A reactive system is an open system that continuously interacts with an uncontrollable external environment, and it must often be highly safe and reliable. However, realizability checking for a given specification is very costly, so we need effective methods to detect and analyze defects in unrealizable specifications to refine them efficiently. We introduce a systematic characterization on necessary conditions of realizability. This characterization is based on quantifications for inputs and outputs in early and late behaviors and reveals four essential aspects of realizability: exhaustivity, strategizability, preservability and stability. Additionally, the characterization derives new necessary conditions, which enable us to classify unrealizable specifications systematically and hierarchically.

Many fatal accidents involving safety-critical reactive systems have occurred in unexpected situations, which were not considered during the design and test phases of system development. To prevent such accidents, reactive systems should be designed to respond appropriately to any request from an environment at any time. Verifying this property during the specification phase reduces the development costs of safety-critical reactive systems. This property of a specification is commonly known as realizability. The complexity of the realizability problem is 2EXPTIME-complete. We have introduced the concept of strong satisfiability, which is a necessary condition for realizability. Many practical unrealizable specifications are also strongly unsatisfiable. In this paper, we show that the complexity of the strong satisfiability problem is EXPSPACE-complete. This means that strong satisfiability offers the advantage of lower complexity for analysis, compared to realizability. Moreover, we show that the strong satisfiability problem remains EXPSPACE-complete even when only formulae with a temporal depth of at most 2 are allowed.