Polynomial hierarchy graph properties in hybrid logic.

In this article, we show that for each property of graphs G in the polynomial hierarchy (PH) there is a sequence ϕ1,ϕ2,… of formulas of the full hybrid logic which are satisfied exactly by the frames in G. Moreover, the size of ϕn is bounded by a polynomial in n. These results lead to the definition of syntactically defined fragments of hybrid logic whose model checking problem is complete for each degree in the polynomial hierarchy.