Skip to main content
SpringerLink
Log in

Integrating Temporal Logics

  • Conference paper
Integrated Formal Methods (IFM 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2999))

Included in the following conference series:

Abstract

In this paper, we study the predicative semantics of different temporal logics and the relationships between them. We use a notation called generic composition to simplify the manipulation of predicates. The modalities of possibility and necessity become generic composition and its inverse of converse respectively. The relationships between different temporal logics are also characterised as such modalities. Formal reasoning is carried out at the level of predicative semantics and supported by the higher-level laws of generic composition and its inverse. Various temporal domains are unified under a notion called resource cumulation. Temporal logics based on these temporal domains can be readily defined, and their axioms identified. The formalism provides a framework in which human experience about system development can be formalised as refinement laws. The approach is demonstrated in the transformation from Duration Calculus to Temporal Logic of Actions. A number of common design patterns are studied. The refinement laws identified are then applied to the case study of water pump controlling.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)

    MATH  Google Scholar 

  2. Chen, Y.: Generic composition. Formal Aspects of Computing 14(2), 108–122 (2002)

    Article  MATH  Google Scholar 

  3. Chen, Y.: Cumulative computing. In: 19th Conference on the Mathematical Foundations of Programming Semantics. ENTCS. Elsevier, Amsterdam (2003)

    Google Scholar 

  4. Emerson, E.A., Clarke, E.M.: Charaterizing correctness properties of parallel programs as fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 169–181. Springer, Heidelberg (1980)

    Google Scholar 

  5. Hehner, E.C.R.: Predicative programming I, II. Communications of ACM 27(2), 134–151 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  6. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  7. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  8. Lamport, L.: Hybrid systems in TLA+. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 77–102. Springer, Heidelberg (1993)

    Google Scholar 

  9. Lamport, L.: A temporal logic of actions. ACM Transctions on Programming Languages and Systems 16(3), 872–923 (1994)

    Article  Google Scholar 

  10. Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science 13, 45–60 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  11. Pnueli, A., Harel, E.: Applications of temporal logic to the specification of realtime systems. In: Joseph, M. (ed.) FTRTFT 1988. LNCS, vol. 331, pp. 84–98. Springer, Heidelberg (1988)

    Google Scholar 

  12. Ravn, A.P., Rischel, H., Hansen, K.M.: Specifying and verifying requirements of real-time systems. IEEE Transactions on Software Engineering 19(1), 41–55 (1993)

    Article  Google Scholar 

  13. Schenke, M., Olderog, E.: Transformational design of real-time systems part i: From requirements to program specifications. Acta Informatica 36(1), 1–65 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  14. Shalqvist, H.: Completeness and correspondence in the first and second order semantics for modal logic. In: Proceedings of the third Scandinavian logic symposium, North Holland, pp. 110–143 (1975)

    Google Scholar 

  15. von Karger, B.: A calculational approach to reactive systems. Science of Computer Programming 37, 139–161 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  16. Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  17. Zhou, C.C., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 36–59. Springer, Heidelberg (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Leicester, Leicester, LE1 7RH, UK

    Yifeng Chen & Zhiming Liu

Authors
  1. Yifeng Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhiming Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, University of Kent, CT2 7NF, Canterbury, Kent, UK

    Eerke A. Boiten

  2. Department of Computing, University of Sheffield, S1 4DP, Sheffield, UK

    John Derrick

  3. School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Australia

    Graeme Smith

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chen, Y., Liu, Z. (2004). Integrating Temporal Logics. In: Boiten, E.A., Derrick, J., Smith, G. (eds) Integrated Formal Methods. IFM 2004. Lecture Notes in Computer Science, vol 2999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24756-2_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24756-2_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-21377-2

  • Online ISBN: 978-3-540-24756-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation