Polynomial hierarchy graph properties in hybrid logic

•Polynomially-bounded growth of sequences of HL formulas expressing PH problems.•The main result still holds if we discharge global modalities provided that graphs are connected and with loops.•An alternative proof of the NP-hardness of the fragment of HL without the pattern binder-box-binder.•Fragments of HL with complete model-checking problems for each degree of the polynomial hierarchy.

In this article, we show that for each property of graphs GG in the polynomial hierarchy (PH) there is a sequence ϕ1,ϕ2,…ϕ1,ϕ2,… of formulas of the full hybrid logic which are satisfied exactly by the frames in GG. Moreover, the size of ϕnϕ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.