Extended modal dependence logic

Abstract

In this paper we extend modal dependence logic by allowing dependence atoms of the form dep( 1,., n ) where i, 1 ≤ i ≤ n, are modal formulas (in, only propositional variables are allowed in dependence atoms). The reasoning behind this extension is that it introduces a temporal component into modal dependence logic. E.g., it allows us to express that truth of propositions in some world of a Kripke structure depends only on a certain part of its past. We show that strictly extends, i.e., there exist-formulas which are not expressible in. However, from an algorithmic point of view we do not have to pay for this since we prove that the complexity of satisfiability and model checking of and coincide. In addition we show that is equivalent to extended by a certain propositional connective. © 2013 Springer-Verlag Berlin Heidelberg.