Complexity of model checking for modal dependence logic. (English) Zbl 1298.68170
Bieliková, Mária (ed.) et al., SOFSEM 2012: Theory and practice of computer science. 38th conference on current trends in theory and practice of computer science, Špindlerův Mlýn, Czech Republic, January 21–27, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27659-0/pbk). Lecture Notes in Computer Science 7147, 226-237 (2012).
Summary: Modal dependence logic (MDL) was introduced recently by Väänänen. It enhances the basic modal language by an operator \(= (\cdot )\). For propositional variables \(p _{1},\dots ,p _{n }\) the atomic formula \(= (p _{1},\dots ,p _{n - 1},p _{n })\) intuitively states that the value of \(p _{n }\) is determined solely by those of \(p _{1},\dots ,p _{n - 1}\).
We show that model checking for MDL formulae over Kripke structures is NP-complete and further consider fragments of MDL obtained by restricting the set of allowed propositional and modal connectives. It turns out that several fragments, e.g., the one without modalities or the one without propositional connectives, remain NP-complete.
We also consider the restriction of MDL where the length of each single dependence atom is bounded by a number that is fixed for the whole logic. We show that the model checking problem for this bounded MDL is still NP-complete. Furthermore we almost completely classifiy the computational complexity of the model checking problem for all restrictions of propositional and modal operators for both unbounded as well as bounded MDL.
For the entire collection see [Zbl 1236.68005].
We show that model checking for MDL formulae over Kripke structures is NP-complete and further consider fragments of MDL obtained by restricting the set of allowed propositional and modal connectives. It turns out that several fragments, e.g., the one without modalities or the one without propositional connectives, remain NP-complete.
We also consider the restriction of MDL where the length of each single dependence atom is bounded by a number that is fixed for the whole logic. We show that the model checking problem for this bounded MDL is still NP-complete. Furthermore we almost completely classifiy the computational complexity of the model checking problem for all restrictions of propositional and modal operators for both unbounded as well as bounded MDL.
For the entire collection see [Zbl 1236.68005].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B45 | Modal logic (including the logic of norms) |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
References:
| [1] | Beyersdorff, O., Meier, A., Mundhenk, M., Schneider, T., Thomas, M., Vollmer, H.: Model checking CTL is almost always inherently sequential. Logical Methods in Computer Science (2011), http://arxiv.org/abs/1103.4990v1 · Zbl 1220.68068 |
| [2] | Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986) · Zbl 0591.68027 · doi:10.1145/5397.5399 |
| [3] | Ebbing, J., Lohmann, P.: Complexity of model checking for modal dependence logic. CoRR abs/1104.1034v1 (2011), http://arxiv.org/abs/1104.1034v1 · Zbl 1385.68015 |
| [4] | Hemaspaandra, E.: The complexity of poor man’s logic. CoRR cs.LO/9911014v2 (2005), http://arxiv.org/abs/cs/9911014v2 · Zbl 1006.03017 |
| [5] | Hemaspaandra, E., Schnoor, H., Schnoor, I.: Generalized modal satisfiability. J. Comput. Syst. Sci. 76(7), 561–578 (2010) · Zbl 1197.68048 · doi:10.1016/j.jcss.2009.10.011 |
| [6] | Lewis, H.: Satisfiability problems for propositional calculi. Mathematical Systems Theory 13, 45–53 (1979) · Zbl 0428.03035 · doi:10.1007/BF01744287 |
| [7] | Lohmann, P., Vollmer, H.: Complexity Results for Modal Dependence Logic. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 411–425. Springer, Heidelberg (2010), http://dx.doi.org/10.1007/978-3-642-15205-4_32 · Zbl 1270.03048 · doi:10.1007/978-3-642-15205-4_32 |
| [8] | Sevenster, M.: Model-theoretic and computational properties of modal dependence logic. Journal of Logic and Computation 19(6), 1157–1173 (2009), http://logcom.oxfordjournals.org/cgi/content/abstract/exn102v1 · Zbl 1193.03042 · doi:10.1093/logcom/exn102 |
| [9] | Väänänen, J.: Dependence logic: A new approach to independence friendly logic. London Mathematical Society Student Texts, vol. 70. Cambridge University Press (2007) · Zbl 1117.03037 · doi:10.1017/CBO9780511611193 |
| [10] | Väänänen, J.: Modal dependence logic. In: Apt, K.R., van Rooij, R. (eds.) New Perspectives on Games and Interaction, Texts in Logic and Games, vol. 4, pp. 237–254. Amsterdam University Press (2008) · Zbl 1377.03011 |
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.
