SCIENCE@home

Complexity Results for Modal Dependence Logic

P. Lohmann,H. Vollmer

Published 2010 in Studia Logica: An International Journal for Symbolic Logic

ABSTRACT

Modal dependence logic was introduced recently by Väänänen. It enhances the basic modal language by an operator = (). For propositional variables p1, . . . , pn, = (p1, . . . , pn-1, pn) intuitively states that the value of pn is determined by those of p1, . . . , pn-1. Sevenster (J. Logic and Computation, 2009) showed that satisfiability for modal dependence logic is complete for nondeterministic exponential time. In this paper we consider fragments of modal dependence logic obtained by restricting the set of allowed propositional connectives. We show that satisfiability for poor man’s dependence logic, the language consisting of formulas built from literals and dependence atoms using \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\wedge, \square, \lozenge}$$\end{document} (i. e., disallowing disjunction), remains NEXPTIME-complete. If we only allow monotone formulas (without negation, but with disjunction), the complexity drops to PSPACE-completeness. We also extend Väänänen’s language by allowing classical disjunction besides dependence disjunction and show that the satisfiability problem remains NEXPTIME-complete. If we then disallow both negation and dependence disjunction, satisfiability is complete for the second level of the polynomial hierarchy. Additionally we consider the restriction of modal dependence logic where the length of each single dependence atom is bounded by a number that is fixed for the whole logic. We show that the satisfiability problem for this bounded arity dependence logic is PSPACE-complete and that the complexity drops to the third level of the polynomial hierarchy if we then disallow disjunction. In this way we completely classify the computational complexity of the satisfiability problem for all restrictions of propositional and dependence operators considered by Väänänen and Sevenster.

PUBLICATION RECORD

CITATION MAP

EXTRACTION MAP

CLAIMS

  • No claims are published for this paper.

CONCEPTS

  • No concepts are published for this paper.

REFERENCES

Showing 1-19 of 19 references · Page 1 of 1

CITED BY

Showing 1-50 of 50 citing papers · Page 1 of 1