Skip to main content
SpringerLink
Log in

The Relation Between Syntax Restriction of Temporal Logic and Properties of Reactive System Specification

  • Conference paper
  • First Online:
Intelligent Information and Database Systems (ACIIDS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10192))

Included in the following conference series:

  • 2132 Accesses

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 to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. 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

    Chapter  Google Scholar 

  2. 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

    Chapter  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. 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

    Chapter  Google Scholar 

  5. 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)

    Google Scholar 

  6. 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

    Chapter  Google Scholar 

  7. 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)

    Google Scholar 

  8. Mori, R., Yonezaki, N.: Several realizability concepts in reactive objects. In: Information Modeling and Knowledge Bases. IOS, Amsterdam (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Information and Computer Sciences, Saitama University, 255, Shimo-ookubo, Sakura-ku, Saitama, Japan

    Noriaki Yoshiura

Authors
  1. Noriaki Yoshiura
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Noriaki Yoshiura .

Editor information

Editors and Affiliations

  1. Wrocław University of Science and Technology, Wroclaw, Poland

    Ngoc Thanh Nguyen

  2. Japan Advanced Institute of Science and Technology, Nomi, Japan

    Satoshi Tojo

  3. Japan Advanced Institute of Science and Technology, Nomi, Japan

    Le Minh Nguyen

  4. Wrocław University of Science and Technology, Wroclaw, Poland

    Bogdan Trawiński

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation