A Fibred Belief Logic for Multi-agent Systems
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.
KeywordsModal Logic Temporal Logic Atomic Formula Local Clock Belief Operator
Unable to display preview. Download preview PDF.
- 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
- 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.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
- 7.Hughes, G.E., Cresswell, M.J.: A New Introduction to Modal Logic, Routledge (1996)Google Scholar
- 10.McMillan, K.L.: Symbolic model checking - an approach to the state explosion problem. PhD thesis, SCS, Carnegie Mellon University (1992)Google Scholar
- 11.Mendelson, E.: Introduction to Mathematical Logic, 4th edn. International Thomson Publishing (1997)Google Scholar
- 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