CBCTL: A Reasoning System of TemporalEpistemic Logic with Communication Channel

This paper introduces a temporal epistemic logic CBCTL that updates agent-s belief states through communications in them, based on computational tree logic (CTL). In practical environments, communication channels between agents may not be secure, and in bad cases agents might suffer blackouts. In this study, we provide inform* protocol based on ACL of FIPA, and declare the presence of secure channels between two agents, dependent on time. Thus, the belief state of each agent is updated along with the progress of time. We show a prover, that is a reasoning system for a given formula in a given a situation of an agent ; if it is directly provable or if it could be validated through the chains of communications, the system returns the proof.




References:
[1] A. E. Emerson and J. Srinivasan. Branching time temporal logic. In J.
W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Linear Time,
Branching Time and Partial Order in Logics and Models for Concurrency,
pp. 123-172. Springer-Verlag, Berlin, 1989.
[2] A. S. Rao & M. P. Gergeff. Decision procedure for BDI logics. Journal
of Logic and Computation, Vol. 9, No. 3, pp. 293-342, 1998.
[3] D. M. Gabbay, M. A. Reynolds, M. Finger. Temporal Logic. Mathematical
Foundations and Computational Aspects, Volume 2, Clarendon Press,
Oxford, 2000.
[4] FIPA Foundation for Intelligent Physical Agents. Fipa 97 part
2 version 2.0: Agent communication language specification, 1997.
http://www.drogo.cselt.it/fipa.org.
[5] J. Barwise and J. Seligman. Information Flow. The Logic of Distributed
Systems, Cambridge University Press, New York, 1997.
[6] M. Benerecetti, F. Giunchiglia and L. Serafini. Model Checking Multiagent
Systems. Journal of Logic and Computation, Special Issue
"Computational and Logical Aspects of Multi-Agent Systems", 8(3), pp.
401-423, 1998.
[7] M. Colombetti. A commitment-based approach to agent speech acts and
conversations. In Proceedings of the Workshop on Agent Languages and
Conversational Policies, pp. 21-29, 2000.
[8] M. Colombetti. Commitment-based semantics for agent communication
languages. In Proceedings of the First Workshop on the History and
Philosophy of Logic, Mathematics and Computation (HPLMC00), Sansebastian,
2000.
[9] M. Wooldridge and A. Rao. Foundations of Rational Agency. Applied
Logic Series, Volume 14, Kluwer Academic Publishers, 1999.
[10] M. Wooldridge. Reasoning about Rational Agents. MIT Press, Cambridge,
2000.
[11] P. R. Cohen and H. J. Levesque. Rational interaction as the basis
for communication. In P. R. Cohen, J. Morgan & M. E. Pollach,
editors, Intentions in Communication, Chapter 8, pp. 221-255. MIT Press,
Cambridge, 1990.