ABSTRACT
This paper focuses on verification for specifications of reactive systems. A reactive system is an open system that interacts with an uncontrollable external environment continuously, and it is often required to be highly safe and reliable. However, the realizability checking for a given specification is very costly, so that we need effective methods to detect and analyze defects of unrealizable specifications for refining them efficiently.
We introduce a systematic characterization on necessary conditions of the realizability. This characterization is based on quantifications for inputs and outputs in early/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 defects of unrealizable specifications systematically and hierarchically.
