Signal Processing and Information Technology. Second International Joint Conference, SPIT 2012, Dubai, UAE, September 20-21, 2012, Revised Selected Papers

Research Article

Complexity of Checking Strong Satisfiability of Reactive System Specifications

Download
431 downloads
  • @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
Masaya Shimakawa1, Shigeki Hagihara1, Naoki Yonezaki1
  • 1: Tokyo Institute of Technology

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.