Termination of Derivations in a Fragment of Transitive Distributed Knowledge Logic

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.

• Type: Journal
• Year: 2008
• Where: INFORMATICALT
• Authors: Regimantas Pliuskevicius, Aida Pliuskeviciene
• Keywords: INFORMATICALT 2008, Logic, Logic S4nd, Transitive Distributed Knowledge