Skip to main content
SpringerLink
Log in

Proof Theory of a Multi-Lane Spatial Logic

  • Conference paper
Theoretical Aspects of Computing – ICTAC 2013 (ICTAC 2013)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8049))

Included in the following conference series:

Abstract

We extend the Multi-lane Spatial Logic MLSL, introduced in previous work for proving the safety (collision freedom) of traffic maneuvers on a multi-lane highway, by length measurement and dynamic modalities. We investigate the proof theory of this extension, called EMLSL. To this end, we prove the undecidability of EMLSL but nevertheless present a sound proof system which allows for reasoning about the safety of traffic situations. We illustrate the latter by giving a formal proof for a lemma we could only prove informally before.

This research was partially supported by the German Research Council (DFG) in the Transregional Collaborative Research Center SFB/TR 14 AVACS.

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. Hilscher, M., Linker, S., Olderog, E.-R., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic manoeuvres. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 404–419. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  2. Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. Computer 18, 10–19 (1985)

    Article  Google Scholar 

  3. Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40, 269–276 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  4. Schäfer, A.: A calculus for shapes in time and space. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 463–477. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Basin, D., Matthews, S., Viganó, L.: Natural deduction for non-classical logics. Studia Logica 60, 119–160 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  6. Rasmussen, T.M.: Labelled natural deduction for interval logics. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 308–323. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. Zhou Chaochen, M.R., Hansen, Sestoft, P.: Decidability and undecidability results for duration calculus. In: Enjalbert, P., Finkel, A., Wagner, K.W. (eds.) STACS 1993. LNCS, vol. 665, pp. 58–68. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  8. Woodcock, J., Davies, J.: Using Z – Specification, Refinement, and Proof. Prentice Hall (1996)

    Google Scholar 

  9. Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall, Inc. (1967)

    Google Scholar 

  10. Gabbay, D.M.: Labelled deductive systems. vol. 1. Oxford University Press (1996)

    Google Scholar 

  11. Viganò, L.: Labelled Non-Classical Logics. Kluwer Academic Publishers (2000)

    Google Scholar 

  12. Dutertre, B.: Complete proof systems for first order interval temporal logic. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, LICS 1995, p. 36. IEEE Computer Society, Washington, DC (1995)

    Chapter  Google Scholar 

  13. van Benthem, J., Bezhanishvili, G.: Modal logics of space. In: Aiello, M., Pratt-Hartmann, I., Benthem, J. (eds.) Handbook of Spatial Logics, pp. 217–298. Springer (2007)

    Google Scholar 

  14. Randell, D.A., Cui, Z., Cohn, A.G.: A Spatial Logic based on Regions and Connection. In: Proc. 3rd Int’l Conf. on Knowledge Representation and Reasoning (1992)

    Google Scholar 

  15. Gabbay, D.M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional modal logics: theory and applications. Studies in Logic and the Foundations of Mathematics, vol. 148. Elsevier (2003)

    Google Scholar 

  16. Simpson, A.K.: The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh (1994)

    Google Scholar 

  17. Caleiro, C., Sernadas, A., Sernadas, C.: Fibring logics: Past, present and future. In: We Will Show Them! Essays in Honour of Dov Gabbay, vol. 1, pp. 363–388 (2005)

    Google Scholar 

  18. Rasga, J., Sernadas, A., Sernadas, C., Viganó, L.: Fibring labelled deduction systems. Journal of Logic and Computation 12, 443–473 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  19. Paulson, L.: Isabelle: A Generic Theorem Prover. Springer (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Oldenburg, Germany

    Sven Linker & Martin Hilscher

Authors
  1. Sven Linker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Hilscher
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. International Institute for Software Technology, United Nations University, P.O. Box 3058, Macau, China

    Zhiming Liu

  2. Department of Computer Science, University of York, Deramore Lane, YO10 5GH, York, UK

    Jim Woodcock

  3. Software Engineering Institute, East China Normal University, 3663 Zhongshan Road (North), 200062, Shanghai, China

    Huibiao Zhu

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Linker, S., Hilscher, M. (2013). Proof Theory of a Multi-Lane Spatial Logic. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theoretical Aspects of Computing – ICTAC 2013. ICTAC 2013. Lecture Notes in Computer Science, vol 8049. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39718-9_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-39718-9_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-39717-2

  • Online ISBN: 978-3-642-39718-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation