Static Analysis for Logic-based Dynamic Programs

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.

Authors

• Thomas Schwentick
• Nils Vortmeier
• Thomas Zeume

Keywords

• Dynamic descriptive complexity
• algorithmic problems
• emptiness
• history independence
• consistency