Abstract: 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.
Abstract: Existing work in temporal logic on representing the
execution of infinitely many transactions, uses linear-time temporal
logic (LTL) and only models two-step transactions. In this paper,
we use the comparatively efficient branching-time computational tree
logic CTL and extend the transaction model to a class of multistep
transactions, by introducing distinguished propositional variables
to represent the read and write steps of n multi-step transactions
accessing m data items infinitely many times. We prove that the
well known correspondence between acyclicity of conflict graphs
and serializability for finite schedules, extends to infinite schedules.
Furthermore, in the case of transactions accessing the same set of
data items in (possibly) different orders, serializability corresponds
to the absence of cycles of length two. This result is used to give an
efficient encoding of the serializability condition into CTL.