A Fibred Belief Logic for Multi-agent Systems

  • Chuchang Liu
  • Maris A. Ozols
  • Mehmet A. Orgun
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3809)


To introduce a temporal dimension to a belief logic, we consider a powerful technique called fibring for combining belief logics and temporal logics. In a fibred belief logic, both temporal operators and belief operators are treated equally. This paper in particular discusses a combination of a belief logic called Typed-Modal Logic with a linear-time temporal logic. We show that, in the resulting logic, we can specify and reason about not only agent beliefs but also the timing properties of a system. With this logical system one is able to build theories of trust for the description of, and reasoning about, multi-agent systems.


Modal Logic Temporal Logic Atomic Formula Local Clock Belief Operator 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Broadfoot, P., Lowe, G.: Analysing a stream authentication protocol using model checking. In: Proc. of the 7th European Symposium on Research in Computer Security, ESORICS (2002)Google Scholar
  2. 2.
    Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Transactions on Computer Systems 8(1), 18–36 (1990)CrossRefGoogle Scholar
  3. 3.
    Clarke, E., Jha, S., Marrero, W.: A machine checkable logic of knowledge for specifying security properties of electronic commerce protocols. In: Proc. of the Workshop on Formal Methods and Security Protocols (1998)Google Scholar
  4. 4.
    Durgin, N., Mitchell, J., Pavlovic, D.: A compositional logic for proving security properties of protocols. Journal of Computer Security 11, 677–721 (2003)Google Scholar
  5. 5.
    Gabbay, D.M.: Fibring Logics. Oxford University Press, Oxford (1999)zbMATHGoogle Scholar
  6. 6.
    Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence 54, 319–379 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Hughes, G.E., Cresswell, M.J.: A New Introduction to Modal Logic, Routledge (1996)Google Scholar
  8. 8.
    Liu, C., Orgun, M.A.: Dealing with multiple granularity of time in temporal logic programming. Journal of Symbolic Computation 22, 699–720 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Liu, C., Ozols, M.A., Orgun, M.A.: A temporalised belief logic for specifying the dynamics of trust for multi-agent systems. In: Maher, M.J. (ed.) ASIAN 2004. LNCS, vol. 3321, pp. 142–156. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  10. 10.
    McMillan, K.L.: Symbolic model checking - an approach to the state explosion problem. PhD thesis, SCS, Carnegie Mellon University (1992)Google Scholar
  11. 11.
    Mendelson, E.: Introduction to Mathematical Logic, 4th edn. International Thomson Publishing (1997)Google Scholar
  12. 12.
    Perrig, A., Canetti, R., Tygar, J.D., Song, D.: Efficient authentication and signing of multicast streams over lossy channels. In: IEEE Symposium on Security and Privacy, pp. 56–73 (May 2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Chuchang Liu
    • 1
  • Maris A. Ozols
    • 1
  • Mehmet A. Orgun
    • 2
  1. 1.Information Networks DivisionDefence Science and Technology OrganisationEdinburghAustralia
  2. 2.Department of ComputingMacquarie UniversitySydneyAustralia

Personalised recommendations