Research Article
Complexity of Checking Strong Satisfiability of Reactive System Specifications
@INPROCEEDINGS{10.1007/978-3-319-11629-7_6, author={Masaya Shimakawa and Shigeki Hagihara and Naoki Yonezaki}, title={Complexity of Checking Strong Satisfiability of Reactive System Specifications}, proceedings={Signal Processing and Information Technology. Second International Joint Conference, SPIT 2012, Dubai, UAE, September 20-21, 2012, Revised Selected Papers}, proceedings_a={SPIT}, year={2014}, month={11}, keywords={Reactive System Verification of Specification Complexity Linear Temporal Logic}, doi={10.1007/978-3-319-11629-7_6} }- Masaya Shimakawa
Shigeki Hagihara
Naoki Yonezaki
Year: 2014
Complexity of Checking Strong Satisfiability of Reactive System Specifications
SPIT
Springer
DOI: 10.1007/978-3-319-11629-7_6
Abstract
Many fatal accidents involving safety-critical reactive systems have occurred in unexpected situations, which were not considered during the design and test phases of the systems. To prevent these 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. It is known that the complexity of the realizability problem is 2EXPTIME-complete. On the other hand, 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.
