Logic of semipublic communications,
Jan A. Plaza,
Abstracts of papers,
European Summer Meeting of the Association for Symbolic Logic,
Veszprem, 1992.
Journal of Symbolic Logic, Vol. 58, No. 3, September 1993.
September 1993,
pp. 1120-1121.
Original text follows.
Logic of semipublic communications
Jan A. Plaza
In distributed systems one often deals with statements such as
"processor 5 knows
the value of variable x", so
one needs a formal logical system for reasoning about knowledge.
Currently existing systems evolved from modal logics, such as
(multimodal) S5 or S4 with the Kripke semantics. These logics are
commonly accepted as logics of knowledge -- they are capable of
describing static states of knowledge. However they do not reflect how
the knowledge changes after
communications among agents (processors).
In this research we analyze situations in which it is generally
known that, say, "at the next moment processor i
will pass to processor j
the
information whether x is 0 or
1".
Processor j will
be the only
recipient of the information, but it is publicly known that this
communication will take place. We
call such a communication a
semipublic
communication.
We show that Kripke semantics is adequate to semipublic communications:
if the initial states of agents' knowledge are represented by a Kripke
model, then the states of knowledge resulting from a semipublic
communication can also be represented by a Kripke model. (we conjecture
that the
class of semipublic communications is the broadest class with this
property.)
We also give an effective construction which yields the model resulting
from the initial Kripke model after a given semipublic communication.
This construction
is a basis for a semantic interpretation of a new logical
connective
*i,j with the following
informal meaning. α *i,j
β means
that β
will be true after a
semipublic communication in which agent i will tell to the
agent j
whether α
was recently
true. This, and other related connectives, are used in formulas of the propositional logic of semipublic communications.
Parameters of time are not explicitly present in the formulas of this
logic.
The logic of semipublic communications is defined by its semantics. We
find an axiomatization of this logic and prove the soundness and
completeness theorem. Moreover, we prove that the logic is decidable.
This logic can be used
to investigate general properties of communications; for instance,
using this logic we
characterize situations in which a sequence of semipublic
communications can be replaced by
parallel semipublic communications.
The logic can be also applied while designing a distributed protocol.
Typically, one produces a succession of versions, the first version of
the protocol being clearly correct, but only the last version being
time-efficient. Then, the question arises whether the last version is
equivalent to the
first one. If the protocols are based on semi-public communications,
they can be
represented by formulae of the logic, and our decidability algorithm
can be used
to test their equivalence. If the protocols are divided into smaller
modules, it is
enough to test equivalence of the corresponding modules, and this can
be
computationally feasible.
Go back to: Dynamic epistemic logics