License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.308
URN: urn:nbn:de:0030-drops-54221
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5422/
Go to the corresponding LIPIcs Volume Portal

Schwentick, Thomas ; Vortmeier, Nils ; Zeume, Thomas

Static Analysis for Logic-based Dynamic Programs

pdf-format:
19.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{schwentick_et_al:LIPIcs:2015:5422,
  author =	{Thomas Schwentick and Nils Vortmeier and Thomas Zeume},
  title =	{{Static Analysis for Logic-based Dynamic Programs}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{308--324},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5422},
  URN =		{urn:nbn:de:0030-drops-54221},
  doi =		{10.4230/LIPIcs.CSL.2015.308},
  annote =	{Keywords: Dynamic descriptive complexity, algorithmic problems, emptiness, history independence, consistency}
}

Keywords: Dynamic descriptive complexity, algorithmic problems, emptiness, history independence, consistency
Collection: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue Date: 2015
Date of publication: 07.09.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI