IEICE TRANSACTIONS on Information
Complexity of Strong Satisfiability Problems for Reactive System Specifications
Summary :
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 2EXPTIME-complete. 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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E96-D No.10 pp.2187-2193
- Publication Date
- 2013/10/01
- Publicized
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.E96.D.2187
- Type of Manuscript
- PAPER
- Category
- Fundamentals of Information Systems
Authors
Masaya SHIMAKAWA
Tokyo Institute of Technology
Shigeki HAGIHARA
Tokyo Institute of Technology
Naoki YONEZAKI
Tokyo Institute of Technology
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Masaya SHIMAKAWA, Shigeki HAGIHARA, Naoki YONEZAKI, "Complexity of Strong Satisfiability Problems for Reactive System Specifications" in IEICE TRANSACTIONS on Information,
vol. E96-D, no. 10, pp. 2187-2193, October 2013, doi: 10.1587/transinf.E96.D.2187.
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 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 2EXPTIME-complete. 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E96.D.2187/_p
Copy
@ARTICLE{e96-d_10_2187,
author={Masaya SHIMAKAWA, Shigeki HAGIHARA, Naoki YONEZAKI, },
journal={IEICE TRANSACTIONS on Information},
title={Complexity of Strong Satisfiability Problems for Reactive System Specifications},
year={2013},
volume={E96-D},
number={10},
pages={2187-2193},
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 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 2EXPTIME-complete. 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.},
keywords={},
doi={10.1587/transinf.E96.D.2187},
ISSN={1745-1361},
month={October},}
Copy
TY - JOUR
TI - Complexity of Strong Satisfiability Problems for Reactive System Specifications
T2 - IEICE TRANSACTIONS on Information
SP - 2187
EP - 2193
AU - Masaya SHIMAKAWA
AU - Shigeki HAGIHARA
AU - Naoki YONEZAKI
PY - 2013
DO - 10.1587/transinf.E96.D.2187
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E96-D
IS - 10
JA - IEICE TRANSACTIONS on Information
Y1 - October 2013
AB - 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 2EXPTIME-complete. 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.
ER -
English
