Name
Abstract | ||
|---|---|---|
We propose a formalism to model database-driven systems, called database manipulating systems (DMS). The actions of a (DMS) modify the current instance of a relational database by adding new elements into the database, deleting tuples from the relations and adding tuples to the relations. The elements which are modified by an action are chosen by (full) first-order queries. (DMS) is a highly expressive model and can be thought of as a succinct representation of an infinite state relational transition system, in line with similar models proposed in the literature. We propose monadic second order logic (MSO-FO) to reason about sequences of database instances appearing along a run. Unsurprisingly, the linear-time model checking problem of (DMS) against (MSO-FO) is undecidable. Towards decidability, we propose under-approximate model checking of (DMS), where the under-approximation parameter is the "bound on recency". In a k-recency-bounded run, only the most recent k elements in the current active domain may be modified by an action. More runs can be verified by increasing the bound on recency. Our main result shows that recency-bounded model checking of (DMS) against (MSO-FO) is decidable, by a reduction to the satisfiability problem of MSO over nested words.
|
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2902251.2902300 | SIGMOD/PODS'16: International Conference on Management of Data
San Francisco
California
USA
June, 2016 |
Keywords | Field | DocType |
database driven dynamic systems, data aware business processes, relational transition systems, model checking, under-approximation | Transition system,Discrete mathematics,Model checking,Nested word,Relational database,Computer science,Tuple,Boolean satisfiability problem,Algorithm,Theoretical computer science,Decidability,Undecidable problem | Conference |
ISBN | Citations | PageRank |
978-1-4503-4191-2 | 1 | 0.35 |
References | Authors | |
20 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Parosh Aziz Abdulla | 1 | 2010 | 122.22 |
| C. Aiswarya | 2 | 1 | 0.35 |
| Mohamed Faouzi Atig | 3 | 505 | 40.94 |
| Marco Montali | 4 | 1280 | 99.36 |
| Othmane Rezine | 5 | 26 | 3.80 |