Skip to main content
SpringerLink
Log in

Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic

  • Conference paper
Computational Logic in Multi-Agent Systems (CLIMA 2008)

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

Included in the following conference series:

Abstract

Linear-time temporal logic (LTL) is known as one of the most useful logics for verifying concurrent systems, and infinitary logic (IL) is known as an important logic for formalizing common knowledge reasoning. The research fields of both LTL and IL have independently been developed each other, and the relationship between them has not yet been discussed before. In this paper, the relationship between LTL and IL is clarified by showing an embedding of LTL into IL. This embedding shows that globally and eventually operators in LTL can respectively be represented by infinitary conjunction and infinitary disjunction in IL. The embedding is investigated by two ways: one is a syntactical way, which is based on Gentzen-type sequent calculi, and the other is a semantical way, which is based on Kripke semantics. The cut-elimination theorems for (some sequent calculi for) LTL, an infinitary linear-time temporal logic ILT ω (i.e., an integration of LTL and IL), a multi-agent infinitary epistemic linear-time temporal logic IELT ω and a multi-agent epistemic bounded linear-time temporal logic ELT l are obtained as applications of the resulting embedding theorem and its extensions and modifications. In particular, the cut-elimination theorem for IELT ω gives a new proof-theoretical basis for extremely expressive time-dependent multi-agent logical systems with common knowledge reasoning.

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. Baratella, S., Masini, A.: An approach to infinitary temporal proof theory. Archive for Mathematical Logic 43(8), 965–990 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  2. van Benthem, J.: Modality, bisimulation and interpolation in infinitary logic. Annals of Pure and Applied Logic 96(1-3), 29–41 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  3. Dixon, C., Gago, M.-C.F., Fisher, M., van der Hoek, W.: Using temporal logics of knowledge in the formal verification of security protocols. In: Proceedings of the 11th International Symposium on Temporal Representation and Reasoning (TIME 2004), pp. 148–151. IEEE Computer Society Press, Los Alamitos (2004)

    Google Scholar 

  4. Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)

    Google Scholar 

  5. Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Formal Models and Semantics (B), pp. 995–1072. Elsevier and MIT Press (1990)

    Google Scholar 

  6. Feferman, S.: Lectures on proof theory. In: Proceedings of the summer school in logic. Lecture Notes in Mathematics, vol. 70, pp. 1–107. Springer, Heidelberg (1968)

    Google Scholar 

  7. Halpern, J.H., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and beliefs. Artificial Intelligence 54, 319–379 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  8. van der Hoek, W., Wooldridge, M.: Cooperation, knowledge and time: Alternating-time temporal epistemic logic and its applications. Studia Logica 75, 125–157 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  9. Kamide, N.: An equivalence between sequent calculi for linear-time temporal logic. Bulletin of the Section of the Logic 35(4), 187–194 (2006)

    MathSciNet  MATH  Google Scholar 

  10. Kamide, N.: Bounded linear-time temporal logic: From Gentzen to Robinson 37 pages (manuscript 2008)

    Google Scholar 

  11. Kaneko, M.: Common knowledge logic and game logic. Journal of Symbolic Logic 64(2), 685–700 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  12. Kaneko, M., Nagashima, T.: Game logic and its applications II. Studia Logica 58(2), 273–303 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  13. Kawai, H.: Sequential calculus for a first order infinitary temporal logic. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 33, 423–432 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  14. Keisler, H.J., Knight, J.F.: Barwise: infinitary logic and addmissible sets. Bulletin of Symbolic Logic 10(1), 4–36 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  15. Kröger, F.: LAR: a logic of algorithmic reasoning. Acta Informatica 8, 243–266 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  16. Lewis, D.K.: Covention: A philosophical study. Harvard University Press (1969)

    Google Scholar 

  17. Lichtenstein, O., Pnueli, A.: Propositional temporal logics: decidability and completeness. Logic Journal of the IGPL 8(1), 55–85 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  18. Lismont, L., Mongin, P.: On the logic of common belief and common knowledge. Theory and Decision 37, 75–106 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  19. Lorenzen, P.: Algebraische und logitishe Untersuchungen über freie Verbände. Journal of Symbolic Logic 16, 81–106 (1951)

    Article  MathSciNet  MATH  Google Scholar 

  20. Maruyama, A., Tojo, S., Ono, H.: Temporal epistemic logics for multi-agent models and their efficient proof-search procedures. Computer Software 20(1), 51–65 (2003) (in Japanese)

    Google Scholar 

  21. Novikov, P.S.: Inconsistencies of certain logical calculi. In: Infinistic Methods, pp. 71–74. Pergamon, Oxford (1961)

    Google Scholar 

  22. Paech, B.: Gentzen-systems for propositional temporal logics. In: Börger, E., Kleine Büning, H., Richter, M.M. (eds.) CSL 1988. LNCS, vol. 385, pp. 240–253. Springer, Heidelberg (1989)

    Google Scholar 

  23. Pliuškevičius, R.: Investigation of finitary calculus for a discrete linear time logic by means of infinitary calculus. In: Barzdins, J., Bjorner, D. (eds.) Baltic Computer Science. LNCS, vol. 502, pp. 504–528. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  24. Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57 (1977)

    Google Scholar 

  25. Szabo, M.E.: A sequent calculus for Kröger logic. In: Salwicki, A. (ed.) Logic of Programs 1980. LNCS, vol. 148, pp. 295–303. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  26. Szałas, A.: Concerning the semantic consequence relation in first-order temporal logic. Theoretical Computer Science 47(3), 329–334 (1986)

    MathSciNet  MATH  Google Scholar 

  27. Takeuti, G.: Proof theory. North-Holland Pub. Co., Amsterdam (1975)

    MATH  Google Scholar 

  28. Tanaka, Y.: Cut-elimination theorems for some infinitary modal logics. Mathematical Logic Quarterly 47(3), 327–339 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  29. Tanaka, Y.: Representations of algebras and Kripke completeness of infinitary and predicate logics, Doctor thesis, Japan Advanced Institute of Science and Technology (1999)

    Google Scholar 

  30. Wooldridge, M., Dixon, C., Fisher, M.: A tableau-based proof method for temporal logics of knowledge and belief. Journal of Applied Non-Classical Logics 8, 225–258 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  31. Y. Vardi, M.: Branching vs. linear time: final showdown. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 1–22. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Waseda Institute for Advanced Study, 1-6-1 Nishi Waseda, Shinjuku-ku, Tokyo, 169-8050, Japan

    Norihiro Kamide

Authors
  1. Norihiro Kamide
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Imperial College London, Ashton Street, L69 3BX, Liverpool, UK

    Michael Fisher

  2. Department of Computing, Imperial College London, 180 Queen’s Gate, SW7 2AZ, London, UK

    Fariba Sadri

  3. Department of Computer Science, Artificial Intelligence Institute, Computational Logic Group, Dresden University of Technology, Nöthnitzer Str. 46, 01187, Dresden, Germany

    Michael Thielscher

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kamide, N. (2009). Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic. In: Fisher, M., Sadri, F., Thielscher, M. (eds) Computational Logic in Multi-Agent Systems. CLIMA 2008. Lecture Notes in Computer Science(), vol 5405. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02734-5_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02734-5_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02733-8

  • Online ISBN: 978-3-642-02734-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation