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

Formale Metadaten

Titel
Reachability in Database-driven Systems with Numerical Attributes under Recency Bounding
Serientitel
Anzahl der Teile
155
Autor
Lizenz
CC-Namensnennung 3.0 Deutschland:
Sie dürfen das Werk bzw. den Inhalt zu jedem legalen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen.
Identifikatoren
Herausgeber
Erscheinungsjahr
Sprache

Inhaltliche Metadaten

Fachgebiet
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.