Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


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

  • Speaker:   Dr  Thomas Schneider  (University of Bremen)
  • Host:   Uli Sattler
  • 6th March 2013 at 14:00 in Lecture Theatre 1.4
Hybrid logic (HL) with binders is an expressive specification language that extends modal logic (ML). Its satisfiability problem is undecidable in general. To represent the temporal behavior of systems and agents, structures over which ML and HL are interpreted can be restricted to the natural numbers or general linear orders. Over both these frame classes, satisfiability of HL with binders is known to be decidable, but of non-elementary complexity.

In this talk, we consider monotone HLs (i.e., the Boolean connectives are conjunction and disjunction only) over the natural numbers and general linear orders. We show that the satisfiability problem remains non- elementary over linear orders, but its complexity drops to PSPACE- completeness over natural numbers. We categorize the strict fragments arising from different combinations of modal and hybrid operators into NP-complete and tractable, and show that the latter cases are complete for NC1 or 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 natural numbers, while below NP it is at most as hard. In addition to the study of computational complexity, we examine model-theoretic properties of the fragments in question.

This is joint work with Stefan Goeller (Bremen), Arne Meier (Hannover), Martin Mundhenk (Jena), Michael Thomas (TWT GmbH) and Felix Weiss (Jena).
▲ Up to the top