In April 2016 Manchester eScholar was replaced by the University of Manchester’s new Research Information Management System, Pure. In the autumn the University’s research outputs will be available to search and browse via a new Research Portal. Until then the University’s full publication record can be accessed via a temporary portal and the old eScholar content is available to search and browse via this archive.

The Complexity of Hybrid Logics over Equivalence Relations

M. Mundhenk, T. Schneider

In: HyLo 2007; 2007. p. 81-90.

Access to files

Full-text and supplementary files are not available from Manchester eScholar. Use our list of Related resources to find this item elsewhere. Alternatively, request a copy from the Library's Document supply service.

Abstract

This paper examines and classifies the computational complexity of modelchecking and satisfiability for hybrid logics over frames withequivalence relations. The considered languages contain all possiblecombinations of the downarrow binder, the existential binder, thesatisfaction operator, and the global modality, ranging from the minimalhybrid language to very expressive languages. For model checking, weseparate polynomial-time solvable from PSPACE-complete cases, and forsatisfiability, we exhibit cases complete for NP, PSpace, NExpTime, andeven N2ExpTime. Our analysis includes the versions of all these languageswithout atomic propositions, and also complete frames.

Bibliographic metadata

Type of resource:
Content type:
Type of conference contribution:
Publication date:
Author(s) list:
Conference title:
HyLo 2007
Proceedings start page:
81
Proceedings end page:
90
Proceedings pagination:
81-90
Contribution total pages:
10
Abstract:
This paper examines and classifies the computational complexity of modelchecking and satisfiability for hybrid logics over frames withequivalence relations. The considered languages contain all possiblecombinations of the downarrow binder, the existential binder, thesatisfaction operator, and the global modality, ranging from the minimalhybrid language to very expressive languages. For model checking, weseparate polynomial-time solvable from PSPACE-complete cases, and forsatisfiability, we exhibit cases complete for NP, PSpace, NExpTime, andeven N2ExpTime. Our analysis includes the versions of all these languageswithout atomic propositions, and also complete frames.

Institutional metadata

University researcher(s):

Record metadata

Manchester eScholar ID:
uk-ac-man-scw:87402
Created by:
Schneider, Thomas
Created:
10th August, 2010, 18:33:36
Last modified:
30th September, 2010, 21:28:52

Can we help?

The library chat service will be available from 11am-3pm Monday to Friday (excluding Bank Holidays). You can also email your enquiry to us.