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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)
Alur, R., La Torre, S.: Deterministic generators and games for ltl fragments. ACM Trans. Comput. Logic 5(1), 1–25 (2004)
Boas, P.V.E.: The convenience of tilings. In: Complexity, Logic, and Recursion Theory, pp. 331–363. Marcel Dekker Inc. (1997)
Hagihara, S., Kitamura, Y., Shimakawa, M., Yonezaki, N.: Extracting environmental constraints to make reactive system specifications realizable. In: Proc. of the 16th Asia-Pacific Software Engineering Conference, pp. 61–68. IEEE (2009)
Hagihara, S., Yonezaki, N.: Completeness of verification methods for approaching to realizable reactive specifications. In: Proc. of 1st Asian Working Conference on Verified Software. UNU-IIST Technical Report, vol. 348, pp. 242–257 (2006)
Jackson, D.: Automating first-order relational logic. In: Proceedings of the 8th ACM SIGSOFT International Symposium on Foundations of Software Engineering: Twenty-First Century Applications, SIGSOFT 2000/FSE-8, pp. 130–139. ACM (2000)
Manna, Z., Pnueli, A.: Axiomatic approach to total correctness of programs. Acta Informatica 3(3), 243–263 (1974)
Mori, R., Yonezaki, N.: Several realizability concepts in reactive objects. In: Information Modeling and Knowledge Bases (1993)
Mori, R., Yonezaki, N.: Derivation of the input conditional formula from a reactive system specification in temporal logic. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 567–582. Springer, Heidelberg (1994)
Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2006)
Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science 13, 45–60 (1981)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–190 (1989)
Rosner, R.: Modular Synthesis of Reactive Systmes. Ph.D. thesis, Weizmann Institute of Science (1992)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Theor. Comput. Sci. 49(2-3), 217–237 (1987)
Tauriainen, H.: On translating linear temporal logic into alternating and nondeterministic automata. Research Report A83, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland (2003)
Yoshiura, N.: Decision procedures for several properties of reactive system specifications. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 154–173. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 ICST Institute for Computer Science, Social Informatics and Telecommunications Engineering
About this paper
Cite this paper
Shimakawa, M., Hagihara, S., Yonezaki, N. (2014). Complexity of Checking Strong Satisfiability of Reactive System Specifications. In: Das, V.V., Elkafrawy, P. (eds) Signal Processing and Information Technology. SPIT 2012. Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, vol 117. Springer, Cham. https://doi.org/10.1007/978-3-319-11629-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-11629-7_6
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11628-0
Online ISBN: 978-3-319-11629-7
eBook Packages: Computer ScienceComputer Science (R0)