Termination of Derivations in a Fragment of Transitive Distributed Knowledge Logic

Article type: Research Article

Authors: Pliuškevičius, Regimantas | Pliuškevičienė, Aida

Affiliations: Institute of Mathematics and Informatics, Akademijos 4, LT-08663 Vilnius, Lithuania, e-mail: {regis, aida}@ktl.mii.lt

Abstract: 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.

Keywords: logic of knowledge, distributed knowledge, safety and liveness properties of distributed systems, deduction-based decision procedure, sequent calculus, loop-check, backtracking, PSPACE-complexity

Journal: Informatica, vol. 19, no. 4, pp. 597-616, 2008