Paper Info
Title
Reachability in Database-driven Systems with Numerical Attributes under Recency Bounding
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.
Year
DOI
Venue
2019
10.1145/3294052.3319705
Proceedings of the 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems
Keywords
Field
DocType
database-driven systems, numerical constraints, reachability, recency
Model checking,EXPTIME,Relational database,Computer science,Decidability,Reachability,Theoretical computer science,Database theory,Database,Bounding overwatch,Undecidable problem
Conference
ISBN
Citations 
PageRank 
978-1-4503-6227-6
0
0.34
References 
Authors
0
4
Name
Order
Citations
PageRank
Parosh Aziz Abdulla12010122.22
C. Aiswarya231.43
Mohamed Faouzi Atig350540.94
Marco Montali4128099.36