The Complexity of Monotone Hybrid Logics over Linear Frames and the Natural Numbers

TL;DR

This paper investigates the complexity of satisfiability problems in monotone hybrid logics over linear orders and natural numbers, revealing complexity classifications and model-theoretic properties for various fragments.

Contribution

It provides a detailed complexity analysis of monotone hybrid logics over different frames, including new results on NP-completeness and tractability classifications.

Findings

Satisfiability is non-elementary over linear orders.

Satisfiability is PSPACE-complete over N.

Certain fragments are NP-complete or in LOGSPACE.

Abstract

Hybrid logic with binders is an expressive specification language. Its satisfiability problem is undecidable in general. If frames are restricted to N or general linear orders, then satisfiability is known to be decidable, but of non-elementary complexity. In this paper, we consider monotone hybrid logics (i.e., the Boolean connectives are conjunction and disjunction only) over N and general linear orders. We show that the satisfiability problem remains non-elementary over linear orders, but its complexity drops to PSPACE-completeness over N. We categorize the strict fragments arising from different combinations of modal and hybrid operators into NP-complete and tractable (i.e. complete for NC1or LOGSPACE). Interestingly, NP-completeness depends only on the fragment and not on the frame. For the cases above NP, satisfiability over linear orders is harder than over N, while below NP it is at most as hard. In addition we examine model-theoretic properties of the fragments in question.