Static Analysis for Logic-Based Dynamic Programs

TL;DR

This paper explores the decidability of static analysis problems for logic-based dynamic programs, focusing on restrictions that make these problems decidable, unlike the general case which is undecidable.

Contribution

It identifies the exact boundaries of decidability for static analysis problems in restricted classes of dynamic programs with limited arity and quantification.

Findings

Decidability results for programs with bounded arity and quantification.

Undecidability of static analysis problems for full first-order dynamic programs.

Pinpointing the decidability borderline for restricted dynamic programs.

Abstract

A dynamic program, as introduced by Patnaik and Immerman (1994), maintains the result of a fixed query for an input database which is subject to tuple insertions and deletions. It can use an auxiliary database whose relations are updated via first-order formulas upon modifications of the input database. This paper studies static analysis problems for dynamic programs and investigates, more specifically, the decidability of the following three questions. Is the answer relation of a given dynamic program always empty? Does a program actually maintain a query? Is the content of auxiliary relations independent of the modification sequence that lead to an input database? In general, all these problems can easily be seen to be undecidable for full first-order programs. Therefore the paper aims at pinpointing the exact decidability borderline for programs with restricted arity (of the input and/or auxiliary database) and restricted quantification.