Belief updating by communication channel

In this paper, we introduce the notion of communication channel into a multiagent system. We formalize the system in term of logic with Belief modality, where each possible world includes CTL. We represent the channel by a reserved set of propositional variables. With this, we revise the definition of inform of FIPA; if the channel exists the receiver agent surely learns the information whereas if not the action fails. According to this distinction, the current state in each world would diverge into two different states. We have implemented a prover, that works also as a model builder. Given a formula in a state in a possible world, the system proves whether it holds or not, while if an inform action is initiated the system adds new states with branching paths.