Complexity of Strong Satisfiability Problems for Reactive System Specifications
Complexity of Strong Satisfiability Problems for Reactive System Specifications
复制标题
DOI：
10.1587/transinf.e96.d.2187
复制
发表时间：
2013-10
期刊：
影响因子：
--
通讯作者：
Masaya Shimakawa;Shigeki Hagihara;N. Yonezaki
中科院分区：
文献类型：
--
作者：
Masaya Shimakawa;Shigeki Hagihara;N. Yonezaki
在系统开发的设计和测试阶段中未考虑，许多涉及安全 - 关键反应系统的致命事故发生在意外情况下。为了防止此类事故，应设计反应性系统，以适当响应环境中的任何请求。在规范阶段验证此属性可降低安全关键反应性系统的开发成本。规范的此属性通常称为可实现性。可靠性问题的复杂性是2 Expimectey。我们介绍了强大的满足感概念，这是实现可靠性的必要条件。许多实用的不可检验的规格也非常不满意。在本文中，我们表明，强大的可满足性问题的复杂性是Expass-Complete。这意味着与可实现性相比，强大的可满足性为分析提供了较低的复杂性。此外，我们表明，即使只允许最高时间为2的公式，也可以实现强大的满足性问题。关键词：反应性系统，强大的满足性，可实现性，复杂性，LTL规范
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 2EXPTIMEcomplete. 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. key words: reactive system, strong satisfiability, realizability, complexity, LTL specification