×

zbMATH — the first resource for mathematics

An analytic tableau calculus for a temporalised belief logic. (English) Zbl 1248.68471
Summary: A tableau is a refutation-based decision procedure for a related logic, and is among the most popular proof procedures for modal logics. In this paper, we present a labelled tableau calculus for a temporalised belief logic called \(TML^{+}\), which is obtained by adding a linear-time temporal logic onto a belief logic by the temporalisation method of Finger and Gabbay. We first establish the soundness and the completeness of the labelled tableau calculus based on the soundness and completeness results of its constituent logics. We then sketch a resolution-type proof procedure that complements the tableau calculus and also propose a model checking algorithm for \(TML^{+}\) based on the recent results for model checking procedures for temporalised logics. \(TML^{+}\) is suitable for formalising trust and agent beliefs and reasoning about their evolution for agent-based systems. Based on the logic \(TML^{+}\), the proposed labelled tableau calculus could be used for analysis, design and verification of agent-based systems operating in dynamic environments.

MSC:
68T27 Logic in artificial intelligence
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T42 Agent technology and artificial intelligence
Software:
SPIN; jSpin; NuSMV
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Adi, K.; Debbabi, M.; Mejri, M., A new logic for electronic commerce protocols, Theoretical computer science, 291, 3, 223-283, (2003) · Zbl 1008.68047
[2] Artosi, A.; Benassi, P.; Governatori, G.; Rotolo, A., Shakespearian modal logic: A labelled treatment of modal identity, Advances in modal logic, 1, 1-21, (1998) · Zbl 0909.03022
[3] Artosi, A.; Governatori, G.; Rotolo, A., A labelled tableau calculus for nonmonotonic (cumulative) consequence relations, (), 82-97 · Zbl 0963.03005
[4] Augsten, N.; Barbosa, D.; Böhlen, M.H.; Palpanas, Themis, Tasm: top-k approximate subtree matching, (), 353-364
[5] Banerjee, M.; Dubois, D., A simple modal logic for reasoning about revealed beliefs, (), 805-816 · Zbl 1245.03019
[6] Ben-Ari, Mordechai, Principles of the spin model checker, (2008), Springer-Verlag London · Zbl 1142.68044
[7] M. Blaze, J. Feigenbaum, J. Lacy, Decentralized trust management, in: Proceedings of the 1996 IEEE Computer Society Symposium on Research in Security and Privacy, 1996, pp. 164-173.
[8] Blaze, M.; Feigenbaum, J.; Strauss, M., Compliance checking in the policymaker trust management system, (), 254-274
[9] Blaze, M.; Feigenbaum, J.; Keromytis, A.D., The role of trust management in distributed systems security, (), 185-210
[10] Burrows, M.; Abadi, M.; Needham, R.M., A logic of authentication, ACM transactions on computer systems, 8, 1, 18-36, (1990)
[11] Cimatti, A.; Clarke, E.M.; Giunchiglia, F.; Roveri, M., Nusmv: a new symbolic model checker, International journal on software tools for technology transfer (STTT), 2, 410-425, (2000) · Zbl 1059.68582
[12] Dixon, C.; Gago, M.C.F.; Fisher, M.; Hoek, W.V.D., Using temporal logics of knowledge in the formal verification of security protocols, (), 148-151
[13] Elofson, G., Developing trust with intelligent agents: an exploratory study, (), 125-138
[14] Finger, M.; Gabbay, D.M., Adding a temporal dimension to a logic system, Journal of logic, language and information, 1, 203-233, (1992) · Zbl 0798.03031
[15] Fitting, M.; Mendelsohn, R.L., First-order modal logic, (1999), Kluwer Academic
[16] Franceschet, M.; Montanari, A.; de Rijke, M., Model checking for combined logics with an application to mobile systems, Automated software engineering, 11, 3, 289-321, (2004)
[17] Gabbay, D.M., Fibring logics, (1999), Oxford University Press Oxford · Zbl 0909.03001
[18] Gabbay, D.M.; Shehtman, V.B., Products of modal logics, part 3: products of modal and temporal logics, Studia logica, 72, 2, 157-183, (2002) · Zbl 1014.03023
[19] Gabbay, D.M.; Hodkinson, I.; Reynolds, M., Temporal logic (vol. 1): mathematical foundations and computational aspects, (1994), Oxford University Press, Inc. New York, NY, USA · Zbl 0921.03023
[20] L. Gong, R. Needham, R. Yahalom, Reasoning about belief in cryptographic protocols, in: Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, 1990, pp. 234-248.
[21] Governatori, G., Labelled tableaux for multi-modal logics, (), 79-94
[22] Grandison, T.; Sloman, M., A survey of trust in Internet applications, IEEE communications surveys and tutorials, 3, 4, (2000)
[23] Halpern, J.Y.; Samet, D.; Segev, E., Defining knowledge in terms of belief: the modal logic perspective, The review of symbolic logic, 2, 3, 469-487, (2009) · Zbl 1186.03030
[24] Jonker, C.M.; Treur, J., Formal analysis of models for the dynamics of trust based on experiences, (), 221-231
[25] Kracht, M.; Wolter, F., Properties of independently axiomatizable bimodal logics, The journal of symbolic logic, 56, 4, 1469-1485, (1991) · Zbl 0743.03013
[26] Kripke, S.A., Semantical considerations on modal logic, Acta philosophica fennica, 16, 83-94, (1963) · Zbl 0131.00602
[27] Liu, C., Logical foundations for reasoning about trust in secure digital communication, (), 333-344 · Zbl 1052.68725
[28] Liu, C.; Orgun, M.A., Verification of reactive systems using temporal logic with clocks, Theoretical computer science, 220, 2, 377-408, (1999) · Zbl 0954.68104
[29] Liu, C.; Ozols, M.A., Trust in secure communication systems - the concept, representations, and reasoning techniques, (), 60-70 · Zbl 1032.68797
[30] Liu, C.; Ozols, M.A.; Orgun, M.A., A temporalised belief logic for specifying the dynamics of trust for multi-agent systems, (), 142-156 · Zbl 1115.68514
[31] Liu, C.; Ozols, M.A.; Orgun, M.A., A fibred belief logic for multi-agent systems, (), 29-38 · Zbl 1151.68654
[32] Lomuscio, A.; Woźna, B., A complete and decidable security-specialised logic and its application to the tesla protocol, (), 145-152
[33] Ma, Ji; Orgun, M.A., Trust management and trust theory revision, IEEE transactions on systems, man and cybernetics, part A, 36, 3, 451-460, (2006)
[34] Ma, J.; Orgun, M.A., Analytic tableaux for verifying agent beliefs, (), 643-646
[35] Ma, J.; Orgun, M.A., Formalising theories of trust for authentication protocols, Information systems frontiers, 10, 1, 19-32, (2008)
[36] Ma, J.; Orgun, M.A.; Sattar, A., Analysis of authentication protocols for multi-agent systems using labelled tableaux, IEEE transactions on systems, man, and cybernetics, part B, 39, 4, 889-900, (2009)
[37] Mauborgne, L., Tree schemata and fair termination, (), 302-321 · Zbl 0966.68579
[38] May, W., A tableau calculus for a temporal logic with temporal connectives, (), 232-246 · Zbl 0931.03034
[39] Orgun, M.A.; Liu, C., Reasoning about dynamics of trust and agent beliefs, (), 105-110
[40] Orgun, M.A.; Liu, C.; Nayak, A.C., Knowledge representation, reasoning and integration using temporal logic with clocks, Mathematics in computer science, 2, 1, 143-163, (2008) · Zbl 1158.68502
[41] Orgun, M.A.; Governatori, G.; Liu, C., Modal tableaux for verifying stream authentication protocols, Autonomous agents and multi-agent systems, 19, 1, 53-75, (2009)
[42] Perrig, A.; Tygar, J.D.; Song, D.; Canetti, R., Efficient authentication and signing of multicast streams over lossy channels, (), 56-73
[43] Schulte, O., Minimal belief change and Pareto-optimality, (), 144-155 · Zbl 0956.03510
[44] Sernadas, A.; Sernadas, C., Combining logic systems: why, how what for?, CIM bulletin, 15, 9-14, (2003)
[45] Su, K.; Luo, X.; Sattar, A.; Orgun, M.A., The interpreted system model of knowledge, belief, desire and intention, (), 220-222
[46] P.F. Syverson, P.C.V. Oorschot, A unified cryptographic protocol logic, in: NRL Publication, 5540-227, Naval Research Lab, 1996.
[47] Teepe, W., On ban logic and hash functions or: how an unjustified inference rule causes problems, Autonomous agents and multi-agent systems, 19, 1, 76-88, (2009)
[48] van Oorschot, Paul, Extending cryptographic logics of belief to key agreement protocols, (), 232-243
[49] Wen, J.; Zhang, M.; Li, X., The study on the application of BAN logic in formal analysis of authentication protocols, (), 744-747
[50] Winslett, M., An introduction to trust negotiation, (), 275-283 · Zbl 1051.68851
[51] R. Yahalom, B. Klein, T. Beth, Trust relationships in secure systems - a distributed authentication perspective, in: Proceedings of the 1993 IEEE Symposium on Research in Security and Privacy, 1993, pp. 150-164.
[52] T. Yu, M. Winslett, A unified scheme for resource protection in automated trust negotiation, in: IEEE Symposium on Security and Privacy, 2003, pp. 110-122.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.