We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Reachability in Database-driven Systems with Numerical Attributes under Recency Bounding

Formal Metadata

Title
Reachability in Database-driven Systems with Numerical Attributes under Recency Bounding
Title of Series
Number of Parts
155
Author
License
CC Attribution 3.0 Germany:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
Language

Content Metadata

Subject Area
Genre
Abstract
A prominent research direction of the database theory community is to develop techniques for verification of database-driven systems operating over relational and numerical data. Along this line, we lift the framework of database manipulating systems citeAbdullaAAMR-pods-16 which handle relational data to also accommodate numerical data and the natural order on them. We study an under-approximation called recency bounding under which the most basic verification problem --reachability, is decidable. Even under this under-approximation the reachability space is infinite in multiple dimensions -- owing to the unbounded sizes of the active domain, the unbounded numerical domain it has access to, and the unbounded length of the executions. We show that, nevertheless, reachability is ExpTime complete. Going beyond reachability to LTL model checking renders verification undecidable.