Decidability of hybrid logic with local common knowledge based on linear temporal logic LTL

Babenyshev, Sergey and Rybakov, Vladimir V. (2008) Decidability of hybrid logic with local common knowledge based on linear temporal logic LTL. In: 4th Conference on Computability in Europe, CiE 2008, 15th June 2008 - 20th June 2008, Athens, Greece.

File not available for download.

Abstract

Our paper considers a hybrid between the multi-agent logic with the local common knowledge operation and an extended version of the linear temporal logic . The logic is based on the semantics of Kripe/Hintikka models with potentially infinite runs and the time points represented by clusters of states with agents’ accessibility relations. We study the satisfiability problem for and related decidability problem. The key result is an algorithm which recognizes theorems of (so we show that is decidable), which, as a consequence, also solves the satisfiability problem. Technique is based on verification of validity for special normal reduced forms of rules in models of double exponential in the size of rules.