Abstract
The Bernays-Schönfinkel class with Datalog is a 2-variable fragment of the Bernays-Schönfinkel class extended with least fixed points expressible by certain monadic Datalog programs. It was used in a bounded model checking procedure for programs manipulating dynamically allocated pointer structures, where the bounded model checking problem was reduced to the satisfiability of formulas in this logic. The best known upper bound on the complexity of the satisfiability problem for this logic was 2NEXPTIME.
In this paper we extend the Bernays-Schönfinkel class with Datalog to a more expressive logic — a fragment of two-variable logic with counting quantifiers extended with the same kind of fixed points. We prove that both satisfiability and entailment for the new logic are decidable in NEXPTIME and we give a matching lower bound for the original logic, which establishes NEXPTIME-completeness of the satisfiability and entailment problems for both of them. Our algorithm is based on a translation to 2-variable logic with counting quantifiers.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis of single-parent heaps. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 91–105. Springer, Heidelberg (2007)
Bansal, K., Brochenin, R., Lozes, E.: Beyond shapes: Lists with ordered data. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 425–439. Springer, Heidelberg (2009)
Bouajjani, A., Drăgoi, C., Enea, C., Sighireanu, M.: A logic-based framework for reasoning about composite data structures. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009 - Concurrency Theory. LNCS, vol. 5710, pp. 178–195. Springer, Heidelberg (2009)
Charatonik, W., Georgieva, L., Maier, P.: Bounded model checking of pointer programs. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 397–412. Springer, Heidelberg (2005)
Charatonik, W., Witkowski, P.: On the complexity of the Bernays-Schönfinkel class with datalog. Full version, http://www.ii.uni.wroc.pl/~pwit/BSD-full.pdf
Fürer, M.: The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems). In: Proceedings of the Symposium ”Rekursive Kombinatorik” on Logic and Machines: Decision Problems and Complexity, London, UK, pp. 312–319. Springer, London (1984)
Grädel, E., Otto, M., Rosen, E.: Undecidability results on two-variable logics. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 249–260. Springer, Heidelberg (1997)
Graedel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: LICS 1997: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA, p. 306. IEEE Computer Society, Los Alamitos (1997)
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive-closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 160–174. Springer, Heidelberg (2004)
Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, pp. 267–281 (1982)
Lahiri, S., Qadeer, S.: Back to the future: revisiting precise program verification using smt solvers. In: POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 171–182. ACM Press, New York (2008)
Leroux, J.: The general vector addition system reachability problem by presburger inductive invariants. In: LICS 2009: Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, pp. 4–13 (2009)
Lipton, R.J.: The Reachability Problem Requires Exponential Space, Technical Report 62, Yale University, Department of Computer Science (January 1976)
Mayr, E.W.: An algorithm for the general petri net reachability problem. SIAM J. Comput. 13(3), 441–460 (1984)
Nas, B.O.: Reachability problems in vector addition systems. The American Mathematical Monthly 80(3), 292–295 (1973)
Pacholski, L., Szwast, W., Tendera, L.: Complexity of two-variable logic with counting. In: LICS 1997: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA, p. 318. IEEE Computer Society, Los Alamitos (1997)
Pacholski, L., Szwast, W., Tendera, L.: Complexity results for first-order two-variable logic with counting. SIAM J. Comput. 29(4), 1083–1117 (2000)
Pratt-Hartmann, I.: Complexity of the two-variable fragment with counting quantifiers. J. of Logic, Lang. and Inf. 14(3), 369–395 (2005)
Yorsh, G., Rabinovich, A., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. Journal of Logic and Algebraic Programming 73(1-2), 111–142 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Charatonik, W., Witkowski, P. (2010). On the Complexity of the Bernays-Schönfinkel Class with Datalog. In: Fermüller, C.G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science, vol 6397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16242-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-16242-8_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16241-1
Online ISBN: 978-3-642-16242-8
eBook Packages: Computer ScienceComputer Science (R0)