Abstract
Open reactive systems provide services to users by interacting the users and environments of the systems. There are several methods that describe formal specifications of reactive systems. Temporal logic is one of the methods. An open reactive system specification is defined to be realizable if and only if there is a program that satisfies the specification even if the environment and the users of the reactive system take any behaviors. There are several kinds of the methods of deciding realizability of open reactive system. These methods are based on automata theory and their complexities are at least double exponential times of the length of a specification. This paper shows the relation between a syntax and realizability properties of reactive system specifications. This relation can reduce the complexity of deciding the properties of reactive system specifications.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Bouyer, P., Bozzelli, L., Chevalier, F.: Controller synthesis for MTL specifications. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 450–464. Springer, Heidelberg (2006). doi:10.1007/11817949_30
Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989). doi:10.1007/BFb0035748
Harel, D., Pnueli, A.: On the development of reactive systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series, vol. 13, pp. 477–498. Springer, Heidelberg (1985)
Kupferman, O., Madhusudan, P., Thiagarajan, P.S., Vardi, M.Y.: Open systems in reactive environments: control and synthesis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 92–107. Springer, Heidelberg (2000). doi:10.1007/3-540-44618-4_9
Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, pp. 188–197 (2005)
Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989). doi:10.1007/BFb0035790
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of 16th Annual ACM Symposium on the Principle of Programming Languages, pp. 179–190 (1989)
Mori, R., Yonezaki, N.: Several realizability concepts in reactive objects. In: Information Modeling and Knowledge Bases. IOS, Amsterdam (1993)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Yoshiura, N. (2017). The Relation Between Syntax Restriction of Temporal Logic and Properties of Reactive System Specification. In: Nguyen, N., Tojo, S., Nguyen, L., Trawiński, B. (eds) Intelligent Information and Database Systems. ACIIDS 2017. Lecture Notes in Computer Science(), vol 10192. Springer, Cham. https://doi.org/10.1007/978-3-319-54430-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-54430-4_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-54429-8
Online ISBN: 978-3-319-54430-4
eBook Packages: Computer ScienceComputer Science (R0)