Static Analysis for Logic-based Dynamic Programs

Authors Thomas Schwentick, Nils Vortmeier, Thomas Zeume



PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.308.pdf
  • Filesize: 0.52 MB
  • 17 pages

Document Identifiers

Author Details

Thomas Schwentick
Nils Vortmeier
Thomas Zeume

Cite AsGet BibTex

Thomas Schwentick, Nils Vortmeier, and Thomas Zeume. Static Analysis for Logic-based Dynamic Programs. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 308-324, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CSL.2015.308

Abstract

The goal of dynamic programs as introduced by Patnaik and Immerman (1994) is to maintain the result of a fixed query for an input database which is subject to tuple insertions and deletions. To this end such programs store an auxiliary database whose relations are updated via first-order formulas upon modifications of the input database. One of those auxiliary relations is supposed to store the answer to the query. Several static analysis problems can be associated to such dynamic programs. Is the answer relation of a given dynamic program always empty? Does a program actually maintain a query? That is, is the answer given of the program the same when an input database was reached by two different modification sequences? Even more, is the content of auxiliary relations independent of the modification sequence that lead to an input database? We study the algorithmic properties of those and similar static analysis problems. Since all these problems can easily be seen to be undecidable for full first-order programs, we examine the exact borderline for decidability for restricted programs. Our focus is on restricting the arity of the input databases as well as the auxiliary databases, and to restrict the use of quantifiers.
Keywords
  • Dynamic descriptive complexity
  • algorithmic problems
  • emptiness
  • history independence
  • consistency

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Samir Datta, Raghav Kulkarni, Anish Mukherjee, Thomas Schwentick, and Thomas Zeume. Reachability is in DynFO. In ICALP, pages 159-170, 2015. Google Scholar
  2. Guozhu Dong, Leonid Libkin, and Limsoon Wong. On impossibility of decremental recomputation of recursive queries in relational calculus and SQL. In DBPL, page 7, 1995. Google Scholar
  3. Guozhu Dong, Leonid Libkin, and Limsoon Wong. Incremental recomputation in local languages. Inf. Comput., 181(2):88-98, 2003. Google Scholar
  4. Guozhu Dong and Jianwen Su. Deterministic FOIES are strictly weaker. Ann. Math. Artif. Intell., 19(1-2):127-146, 1997. Google Scholar
  5. Guozhu Dong and Jianwen Su. Arity bounds in first-order incremental evaluation and definition of polynomial time database queries. J. Comput. Syst. Sci., 57(3):289-308, 1998. Google Scholar
  6. Guozhu Dong, Jianwen Su, and Rodney Topor. Nonrecursive incremental evaluation of datalog queries. Annals of Mathematics and Artificial Intelligence, 14, 1995. Google Scholar
  7. Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset nets between decidability and undecidability. In ICALP, pages 103-115, 1998. Google Scholar
  8. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, 1995. Google Scholar
  9. Paul Erdős and Richard Rado. Intersection theorems for systems of sets. Journal of the London Mathematical Society, s1-35(1):85-90, 1960. Google Scholar
  10. Wouter Gelade, Marcel Marquardt, and Thomas Schwentick. The dynamic complexity of formal languages. ACM Trans. Comput. Log., 13(3):19, 2012. Google Scholar
  11. Erich Grädel and Sebastian Siebertz. Dynamic definability. In ICDT, pages 236-248, 2012. Google Scholar
  12. William Hesse. Dynamic Computational Complexity. PhD thesis, University of Massachusetts Amherst, 2003. Google Scholar
  13. John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci., 8:135-159, 1979. Google Scholar
  14. Stasys Jukna. Extremal combinatorics, volume 2. Springer, 2001. Google Scholar
  15. Stefan Kratsch and Magnus Wahlström. Preprocessing of min ones problems: A dichotomy. In ICALP, pages 653-665, 2010. Google Scholar
  16. Leonid Libkin. Elements of Finite Model Theory. Springer, 2004. Google Scholar
  17. Dániel Marx. Parameterized complexity of constraint satisfaction problems. Computational Complexity, 14(2):153-183, 2005. Google Scholar
  18. Marvin L. Minsky. Computation: finite and infinite machines. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1967. Google Scholar
  19. Sushant Patnaik and Neil Immerman. Dyn-FO: A parallel, dynamic complexity class. In PODS, pages 210-221. ACM Press, 1994. Google Scholar
  20. Thomas Schwentick, Nils Vortmeier, and Thomas Zeume. Static analysis for logic-based dynamic programs. CoRR, abs/1507.04537, 2015. Google Scholar
  21. Boris A. Trahtenbrot. Impossibility of an algorithm for the decision problem in finite classes. AMS Translations, Series 2, 23:1-5, 1963. Google Scholar
  22. Nils Vortmeier. Komplexitätstheorie verlaufsunabhängiger dynamischer Programme. Master’s thesis, TU Dortmund University, 2013. In German. Google Scholar
  23. Thomas Zeume. The dynamic descriptive complexity of k-clique. In MFCS, pages 547-558, 2014. Google Scholar
  24. Thomas Zeume and Thomas Schwentick. Dynamic conjunctive queries. In ICDT, pages 38-49, 2014. Google Scholar
  25. Thomas Zeume and Thomas Schwentick. On the quantifier-free dynamic complexity of reachability. Inf. Comput., 240:108-129, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail