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.