Decidability of a syntactic fragment of the hybrid computation tree logic with the operator

Abstract

Hybrid logics with the ↓ operator are generally undecidable. In this paper, we present a fragment of the hybrid CTL with the ↓ operator (HCTL(@, ↓ )), called the reducible fragment, that has the same complexity for the satisfiability problem as standard CTL (EXPTIME-Complete). In order to prove this, we show that the satisfiability problem for a formula in this fragment can be polynomially reduced to the satisfiability problem for a formula in the hybrid CTL without the ↓ operator (HCTL(@)).