Informatica

A transitive distributed knowledge logic is considered. The considered logic S4nD is obtained from multi-modal logic S4n by adding transitive distributed knowledge operator. For a fragment of this logic loop-check-free sequent calculus is proposed. The considered fragment is such that it can be applied for specification and verification of safety properties of knowledge-based distributed systems. By relying on the constructed loop-check-free sequent calculus a PSPACE procedure to determine a termination of backward derivation in considered fragment of the logic S4nD is presented.

In this paper we consider branching time temporal logics of knowledge and belief. These logics involve the discrete time linear temporal logic operators “next” and “until” with the branching temporal logic operator “on all paths”. The latter operator is interpreted with respect to a version of the bundle semantics. In addition the temporal logic of knowledge (belief) contains an indexed set of unary modal operators “agent i knows” (“agent i believes”) and it contains the modality of common knowledge (belief). For these logics we present sequent calculi with a restricted cut rule. Thus, we get proof systems where proof-search becomes decidable. The soundness and completeness for these calculi are proved.

In this paper we consider two logics: temporal logic of common knowledge and temporal logic of common belief. These logics involve the discrete time linear temporal logic operators “next” and “until”. In addition the first logic contains an indexed set of unary modal operators “agent i knows”, the second one contains an indexed set of unary modal operators “agent i believes”. Also the first logic contains the modality of common knowledge and the second one contains the modality of common belief. For these logics we present sequent calculi with an analytic cut rule. The soundness and completeness for these calculi are proved.

A temporal logic of belief and actions (TLBA) is considered. The TLBA allows us to express informational and dynamic properties of computational agents. The considered fragment of TLBA allows one: (1) to present a deduction‐based structured decision procedure; (2) to separate a decision procedure for so‐called induction‐free formulas and (3) to use only logical axioms for such formulas. The main new technical tool of the presented decision procedure is separation rules which incorporate traditional rules for the temporal operator “next”, belief modalities and action constants.