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.

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.