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

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.