Complexity results for modal dependence logic. (English) Zbl 1432.03043
Summary: Modal dependence logic was introduced recently by J. Väänänen [in: New perspectives on games and interaction. Selected papers based on the presentations at the colloquium, Amsterdam, Netherlands, February 5–7, 2007. Amsterdam: Amsterdam University Press. 237–254 (2008; Zbl 1377.03011)]. It enhances the basic modal language by an operator \(=()\). For propositional variables \(p_1,\dots,p_n,=(p_1,\dots,p_{n-1},p_n)\) intuitively states that the value of \(p_n\) is determined by those of \(p_1,\dots,p_{n-1}\). M. Sevenster [J. Log. Comput. 19, No. 6, 1157–1173 (2009; Zbl 1193.03042)] 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 \(\wedge,\square,\lozenge\) (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 [loc. cit.] and Sevenster [loc. cit.].
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 \(\wedge,\square,\lozenge\) (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 [loc. cit.] and Sevenster [loc. cit.].
MSC:
| 03B60 | Other nonclassical logic |
| 03B45 | Modal logic (including the logic of norms) |
| 68Q25 | Analysis of algorithms and problem complexity |
Keywords:
dependence logic; modal logic; satisfiability problem; computational complexity; poor man’s logicReferences:
| [1] | Abramsky Samson, Väänänen Jouko: From IF to BI. Synthese 167(2), 207-230 (2009) · Zbl 1175.03016 · doi:10.1007/s11229-008-9415-6 |
| [2] | Bauland, Michael, Elmar Böhler, Nadia Creignou, Steffen Reith, Henning Schnoor, and Heribert Vollmer, The complexity of problems for quantified constraints, Theory of Computing Systems 47:454-490, 2010. 10.1007/s00224-009-9194-6. · Zbl 1204.68182 |
| [3] | Cook, Stephen A., The complexity of theorem-proving procedures, in STOC ’71: Proceedings of the third annual ACM symposium on Theory of computing, ACM, New York, NY, USA, 1971, pp. 151-158. · Zbl 0253.68020 |
| [4] | Donini, Francesco M., Maurizio Lenzerini, Daniele Nardi, Bernhard Hollunder, Werner Nutt, and Alberto Marchetti-Spaccamela, The complexity of existential quantification in concept languages, Artif. Intell. 53(2-3):309-327, 1992. · Zbl 1193.68241 |
| [5] | Hemaspaandra, Edith, The complexity of poor man’s logic, Journal of Logic and Computation 11(4):609-622, 2001. Corrected version: [6]. · Zbl 1006.03017 |
| [6] | Hemaspaandra, Edith, The complexity of poor man’s logic, CoRR, cs.LO/9911014v2, 2005. |
| [7] | Hemaspaandra Edith, Schnoor Henning., Schnoor Ilka.: Generalized modal satisfiability. J. Comput. Syst. Sci. 76(7), 561-578 (2010) · Zbl 1197.68048 · doi:10.1016/j.jcss.2009.10.011 |
| [8] | Henkin, L., Some remarks on infinitely long formulas, in Infinitistic Methods, Proceedings Symposium Foundations of Mathematics, Pergamon, Warsaw, 1961, pp. 167-183. · Zbl 0121.25308 |
| [9] | Hintikka, J., and G. Sandu, Informational independence as a semantical phenomenon, in J. E. Fenstad, I. T. Frolov, and R. Hilpinen, (eds.), Logic, Methodology and Philosophy of Science VIII, vol. 126, Elsevier, Amsterdam, 1989, pp. 571-589. · Zbl 0683.03004 |
| [10] | Ladner, Richard E., The computational complexity of provability in systems of modal propositional logic, Siam Journal on Computing 6(3):467-480, 1977. · Zbl 0373.02025 |
| [11] | Lewis Harry: Satisfiability problems for propositional calculi. Mathematical Systems Theory 13, 45-53 (1979) · Zbl 0428.03035 · doi:10.1007/BF01744287 |
| [12] | Lohmann, Peter, and Heribert Vollmer, Complexity results for modal dependence logic, in Proceedings 19th Conference on Computer Science Logic, vol. 6247 of Lecture Notes in Computer Science, Springer Berlin / Heidelberg, 2010, pp. 411-425. · Zbl 1270.03048 |
| [13] | Meier, Arne, Martin Mundhenk, Michael Thomas, and Heribert Vollmer, The complexity of satisfiability for fragments of CTL and CTL*, Electronic Notes in Theoretical Computer Science 223:201-213, 2008. Proceedings of the Second Workshop on Reachability Problems in Computational Models (RP 2008). · Zbl 1337.68134 |
| [14] | Peterson G., Reif J., Azhar S.: Lower bounds for multiplayer noncooperative games of incomplete information. Computers & Mathematics with Applications 41(7-8), 957-992 (2001) · Zbl 0991.91007 · doi:10.1016/S0898-1221(00)00333-3 |
| [15] | Reith, Steffen, and Klaus W. Wagner, The complexity of problems defined by boolean circuits, in Proceedings International Conference Mathematical Foundation of Informatics, (MFI99), World Science Publishing, 2000, pp. 25-28. |
| [16] | Sevenster Merlijn.: Model-theoretic and computational properties of modal dependence logic. Journal of Logic and Computation 19(6), 1157-1173 (2009) · Zbl 1193.03042 · doi:10.1093/logcom/exn102 |
| [17] | Väänänen, Jouko, Dependence logic: A new approach to independence friendly logic, no. 70 in London Mathematical Society student texts, Cambridge University Press, 2007. · Zbl 1117.03037 |
| [18] | Väänänen, Jouko, Modal dependence logic, in Krzysztof R. Apt, and Robert van Rooij, (eds.), New Perspectives on Games and Interaction, vol. 4 of Texts in Logic and Games, Amsterdam University Press, 2008, pp. 237-254. · Zbl 1377.03011 |
| [19] | Wrathall Celia: Complete sets and the polynomial-time hierarchy. Theoretical Computer Science 3(1), 23-33 (1977) · Zbl 0366.02031 · doi:10.1016/0304-3975(76)90062-1 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
