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

Our paper(1) considers a hybrid LTLACK between the multiagent logic with the local common knowledge operation and an extended version of the linear temporal logic LTL. 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 LTLACK and related decidability problem. The key result is an algorithm which recognizes theorems of LTLACK (so we show that LTLACK 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.