×

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:

jSpin; SPIN; NuSMV
PDFBibTeX XMLCite
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, (Automated Reasoning with Analytic Tableaux and Related Methods, Proceedings of the International Conference, TABLEAUX 2000. Automated Reasoning with Analytic Tableaux and Related Methods, Proceedings of the International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000. Automated Reasoning with Analytic Tableaux and Related Methods, Proceedings of the International Conference, TABLEAUX 2000. Automated Reasoning with Analytic Tableaux and Related Methods, Proceedings of the International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Lecture Notes in Computer Science, vol. 1847 (2000), Springer-Verlag), 82-97 · Zbl 0963.03005
[4] Augsten, N.; Barbosa, D.; Böhlen, M. H.; Palpanas, Themis, Tasm: Top-k approximate subtree matching, (Proceedings of the 26th International Conference on Data Engineering, ICDE 2010. Proceedings of the 26th International Conference on Data Engineering, ICDE 2010, March 1-6, 2010, Long Beach, CA, USA (2010), IEEE), 353-364
[5] Banerjee, M.; Dubois, D., A simple modal logic for reasoning about revealed beliefs, (Symbolic and Quantitative Approaches to Reasoning with Uncertainty, Proceedings of the 10th European Conference, ECSQARU 2009. Symbolic and Quantitative Approaches to Reasoning with Uncertainty, Proceedings of the 10th European Conference, ECSQARU 2009, Verona, Italy, July 1-3, 2009. Symbolic and Quantitative Approaches to Reasoning with Uncertainty, Proceedings of the 10th European Conference, ECSQARU 2009. Symbolic and Quantitative Approaches to Reasoning with Uncertainty, Proceedings of the 10th European Conference, ECSQARU 2009, Verona, Italy, July 1-3, 2009, Lecture Notes in Computer Science, vol. 5590 (2009), Springer-Verlag), 805-816 · Zbl 1245.03019
[6] Ben-Ari, Mordechai, Principles of the Spin Model Checker (2008), Springer-Verlag: 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.; 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, (Financial Cryptography. Financial Cryptography, Lecture Notes in Computer Science, vol. 1465 (1998), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 254-274
[9] Blaze, M.; Feigenbaum, J.; Keromytis, A. D., The role of trust management in distributed systems security, (Vitek, J.; Jensen, Christian D., Secure Internet Programming (1999), Springer-Verlag: Springer-Verlag London, UK), 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, (Proceedings of the 11th International Symposium on Temporal Representation and Reasoning (2004), IEEE Computer Society), 148-151
[13] Elofson, G., Developing trust with intelligent agents: an exploratory study, (Trust and Deception in Virtual Societies (2001), Kluwer Academic: Kluwer Academic Dordrecht, The Netherlands), 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 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.: 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.; 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, (Theorem Proving with Analytic Tableaux and Related Methods, Proceedings of the 4th International Workshop, TABLEAUXʼ95. Theorem Proving with Analytic Tableaux and Related Methods, Proceedings of the 4th International Workshop, TABLEAUXʼ95, Schloß Rheinfels, St. Goar, Germany, May 7-10, 1995. Theorem Proving with Analytic Tableaux and Related Methods, Proceedings of the 4th International Workshop, TABLEAUXʼ95. Theorem Proving with Analytic Tableaux and Related Methods, Proceedings of the 4th International Workshop, TABLEAUXʼ95, Schloß Rheinfels, St. Goar, Germany, May 7-10, 1995, Lecture Notes in Computer Science, vol. 918 (1995), Springer-Verlag), 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, (Proceedings of the 9th European Workshop on Modelling Autonomous Agents in a Multi-Agent World: MultiAgent System Engineering, MAAMAWʼ99 (1999), Springer-Verlag: Springer-Verlag London, UK), 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, (Proceedings of the 14th Australian Joint Conference on Artificial Intelligence: Advances in Artificial Intelligence, AIʼ01 (2001), Springer-Verlag: Springer-Verlag London, UK), 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, (Proceedings of AI2002: Advances in Artificial Intelligence. Proceedings of AI2002: Advances in Artificial Intelligence, Lecture Notes in Computer Science, vol. 2557 (2002), Springer-Verlag), 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, (Proceedings of the 9th Asian Computing Science Conference. Proceedings of the 9th Asian Computing Science Conference, Lecture Notes in Computer Science, vol. 3321 (2004), Springer-Verlag), 142-156 · Zbl 1115.68514
[31] Liu, C.; Ozols, M. A.; Orgun, M. A., A fibred belief logic for multi-agent systems, (Zhang, Shichao; Jarvis, Ray, Proceedings of the 18th Australian Joint Conference on Artificial Intelligence. Proceedings of the 18th Australian Joint Conference on Artificial Intelligence, Sydney, Australia, December 5-9, 2005. Proceedings of the 18th Australian Joint Conference on Artificial Intelligence. Proceedings of the 18th Australian Joint Conference on Artificial Intelligence, Sydney, Australia, December 5-9, 2005, Lecture Notes in Computer Science, vol. 3809 (2005), Springer-Verlag), 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, (Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems, AAMASʼ06 (2006), ACM: ACM New York, NY, USA), 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, (Proceedings of the 2008 IEEE/WIC/ACM International Conference on Web Intelligence and International Conference on Intelligent Agent Technology - Workshops. Proceedings of the 2008 IEEE/WIC/ACM International Conference on Web Intelligence and International Conference on Intelligent Agent Technology - Workshops, 9-12 December, 2008, Sydney, NSW, Australia (2008), IEEE), 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, (Palsberg, Jens, Static Analysis, Proceedings of the 7th International Symposium, SAS 2000. Static Analysis, Proceedings of the 7th International Symposium, SAS 2000, Santa Barbara, CA, USA, June 29-July 1, 2000. Static Analysis, Proceedings of the 7th International Symposium, SAS 2000. Static Analysis, Proceedings of the 7th International Symposium, SAS 2000, Santa Barbara, CA, USA, June 29-July 1, 2000, Lecture Notes in Computer Science, vol. 1824 (2000), Springer-Verlag), 302-321 · Zbl 0966.68579
[38] May, W., A tableau calculus for a temporal logic with temporal connectives, (Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Computer Science, vol. 1617 (1999), Springer-Verlag), 232-246 · Zbl 0931.03034
[39] Orgun, M. A.; Liu, C., Reasoning about dynamics of trust and agent beliefs, (Proceedings of the 2006 IEEE International Conference on Information Reuse and Integration (2006), IEEE Systems, Man, and Cybernetics Society), 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, (Proceedings of the 2000 IEEE Symposium on Security and Privacy (2000), IEEE Computer Society: IEEE Computer Society Washington, DC, USA), 56-73
[43] Schulte, O., Minimal belief change and Pareto-optimality, (Proceedings of the 12th Australian Joint Conference on Artificial Intelligence: Advanced Topics in Artificial Intelligence, AIʼ99 (1999), Springer-Verlag: Springer-Verlag London, UK), 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, (Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems, AAMASʼ06 (2006), ACM: ACM New York, NY, USA), 220-222
[46] P.F. Syverson, P.C.V. Oorschot, A unified cryptographic protocol logic, in: NRL Publication, 5540-227, Naval Research Lab, 1996.; 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, (Proceedings of the 1st ACM Conference on Computer and Communications Security, CCSʼ93 (1993), ACM: ACM New York, NY, USA), 232-243
[49] Wen, J.; Zhang, M.; Li, X., The study on the application of BAN logic in formal analysis of authentication protocols, (Proceedings of the 7th International Conference on Electronic Commerce (2005), ACM Press), 744-747
[50] Winslett, M., An introduction to trust negotiation, (Proceedings of the 1st International Conference on Trust Management, iTrustʼ03 (2003), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 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.; 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.; 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.