Termination of Derivations in a Fragment of Transitive Distributed Knowledge Logic

A transitive distributed knowledge logic is considered. The considered logic S4_nD is obtained from multi-modal logic S4_n 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 S4_nD is presented.