- 著者
-
Takashi TOMITA
Shigeki HAGIHARA
Masaya SHIMAKAWA
Naoki YONEZAKI
- 出版者
- The Institute of Electronics, Information and Communication Engineers
- 雑誌
- IEICE TRANSACTIONS on Information and Systems (ISSN:09168532)
- 巻号頁・発行日
- vol.E105-D, no.10, pp.1665-1677, 2022-10-01
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.