Skip to main content
SpringerLink
Log in

Completeness of Neighbourhood Logic

  • Conference paper
  • First Online:
Book cover STACS 99 (STACS 1999)

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

Included in the following conference series:

Abstract

This paper presents a completeness result for a first-order interval temporal logic, called Neighbourhood Logic (NL) which has two neighbourhood modalities. NL can support the specification of liveness and fairness properties of computing systems as well as formalisation of many concepts of real analysis. These two modalities are also adequate in the sense that they can derive other important unary and binary modalities of interval temporal logic. We prove the completeness result for NL by giving a Kripke model semantics and then mapping the Kripke models to the interval models for NL.

The work was done when the author visited UNU/IIST as a fellow during May–Aug.’97

The work was done when the author visited UNU/IIST as a fellow Jun.’96–Jan.’97

On leave of absence from Software Institute, Chinese Academy of Sciences

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur R., Courcoubetis C., Henzinger T., Ho P-H.: Hybrid Automata: An algorithmic approach to the specification and verification of Hybrid systems, in Hybrid Systems, R.L. Grossman, A. Nerode, A. P. Ravn and H. Rischel (Eds.), LNCS 736, pp. 209–229, Springer-Verlag, 1993.

    Google Scholar 

  2. Barua Rana, Zhou Chaochen: Neighbourhood Logics: NL and NL2, UNU/IIST Report no. 120, 1997.

    Google Scholar 

  3. Berry Gérard, Gonthier Georges: The Esterel Synchronous Programming Language: Design, Semantics and Implementation, in Science of Computer Programming, vol. 19, pp. 87–152, Elsevier, 1992.

    Article  MATH  Google Scholar 

  4. Dutertre B.: Complete Proof Systems for First Order Interval Logic, Tenth Annual IEEE Symp. on Logic in Computer Science, pp. 36–43, IEEE Press, 1995.

    Google Scholar 

  5. Halpern J., Shoham Y.: A Propositional Modal Logic of Time Intervals, Journal of the ACM 38(4) pp. 935–962, 1991. Also appeared in Proceedings of the First IEEE Symposium on Logic in Computer Science, pp. 279–292, Computer Society Press, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  6. Hansen Michael, Zhou Chaochen: Duration Calculus: Logical Foundations, To appear in Formal Aspects of Computing.

    Google Scholar 

  7. Humberstone: Interval semantics for Tense Logic, Jour of Phil. Logic, 8, 1979.

    Google Scholar 

  8. Hughes G. E., Creswell M.J.: An introduction to Modal Logic, Routledge, 1990.

    Google Scholar 

  9. Lamport L.: Hybrid systems in TLA +, in in Hybrid Systems, R.L. Grossman, A. Nerode, A. P. Ravn and H. Rischel (Eds.), LNCS 736, pp. 77–102, Springer-Verlag, 1993.

    Google Scholar 

  10. Manna Z., Pnueli A.: Verifying hybrid systems, in Hybrid Systems, R. L. Grossman, A. Nerode, A. P. Ravn and H. Rischel (Eds.), LNCS 736, pp. 4–35, Springer-Verlag 1993.

    Google Scholar 

  11. Moszkowski B.: A Temporal Logic for Multilevel Reasoning about Hardware, IEEE Computer 18(2) pp. 10–19, 1985.

    Google Scholar 

  12. Pujari Arun K: Neighbourhood Logic & Interval Algebra. UNU/IIST Report no. 116, 1997.

    Google Scholar 

  13. Qiu Zongyan, Zhou Chaochen: A Combination of Interval Logic and Linear Temporal Logic. UNU/IIST Report no. 123, 1997 (accepted by PROCOMET’98).

    Google Scholar 

  14. Roy Suman, Zhou Chaochen: Notes in Neighbourhood Logic, UNU/IIST Report no. 97, 1997.

    Google Scholar 

  15. Shoenfield J., Mathematical Logic, Addison-Wesley, Reading, Mass., 1967.

    MATH  Google Scholar 

  16. Venema Y.: Expressiveness and Completeness of an Interval Tense Logic, Notre Dame Journal of Formal Logic, Vol. 31, No. 4, pp. 529–547, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  17. Venema Y.: A Modal Logic for Chopping Intervals, Journal of Logic and Computation, Vol. 1, pp. 453–476, Oxford University Press, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  18. Zhou Chaochen, Hansen Michael R.: An Adequate First Order Interval Logic. UNU/IIST Report No. 91, Revised report, December 1996.

    Google Scholar 

  19. Zhou Chaochen, Hoare C. A. R., Ravn A. P.: A Calculus of Durations, Information Processing Letters, Vol. 40, No. 5, pp. 269–276, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  20. Zhou Chaochen, Ravn A. P., Hansen Michael R.: An extended duration calculus for hybrid systems, in Hybrid Systems, R. L. Grossman, A. Nerode, A. P. Ravn and H. Rischel (Eds.), LNCS 736, pp. 36–59, Springer-Verlag, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Stat-Math. unit, I.S.I., 203 B.T. Road, Calcutta, 700 035, India

    Rana Barua

  2. Computer Science and Automation, I.I.Sc., Bangalore, 560 012, India

    Suman Roy

  3. International Institute for Software Technology, UNU/IIST, P.O. Box 3057, Macau

    Zhou Chaochen

Authors
  1. Rana Barua
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Suman Roy
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zhou Chaochen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. FB IV - Informatik, Universität Trier, D-54286, Trier, Germany

    Christoph Meinel

  2. LIFL, Université de Lille I, Bătiment 3, F-59655, Villeneuve d’Ascq Cedex, France

    Sophie Tison

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barua, R., Roy, S., Chaochen, Z. (1999). Completeness of Neighbourhood Logic. In: Meinel, C., Tison, S. (eds) STACS 99. STACS 1999. Lecture Notes in Computer Science, vol 1563. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49116-3_49

Download citation

  • DOI: https://doi.org/10.1007/3-540-49116-3_49

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65691-3

  • Online ISBN: 978-3-540-49116-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation