Reachability in Database-driven Systems with Numerical Attributes under Recency Bounding
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.
Abdulla, Parosh Aziz
Aiswarya, C.
Faouzi Atig, Mohamed
Montali, Marco
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.
 I am Aishwarya, I am from Chennai Mathematical Institute. This is a joint work with Parosh Aziz Abdullah and Mohamed Fosya, I think, from Uppsala University and Marco Montalhi from University of Bursan, Borsano. I am rather new to this community, so I don't know most of you. You may not know me either. So this is actually a continuation of our work on verification of database-driven systems. This time we add numerical attributes to it. So we will start by looking at the terms on the title to see what they are. And the motivation to study this is, of course, verification of database-driven systems like business processes or something which are working over relational and numerical data. The database-driven systems that we consider are relational databases over unbounded data domain and a finite schema, basically relations with arbitrary RIT. And the system can transform some given database instance to another by performing actions. We will see what this will be more closely. There are various formalisms for database-driven systems as well. The particular one that we use are called database-manipulating systems which are described by these actions. And what can these actions do? These actions will query the current database instance and it will, from the set of answers to that query, it will retrieve one tuple non-deterministically and will delete some tuples from the current instance as dictated by the action and will add some tuples into the relations again as specified by the actions. And these additions can involve new values which are not currently present in the database. So the size of the database instance can grow and it's unbounded. So in general, this graph that you see over there, that can be an infinite graph. So we see an example. This is an example of an action. So the action is a template, let us say. It uses variables. It has a query here and let's consider I1. So the query just asks you to return a U such that R of U is satisfied and there are two possible answers. And we pick non-deterministically one. Let's pick E1. And with this E1, now we will instantiate this transition into a more concrete transition. Of course, we will replace the occurrences of U with E1. That means that we have to delete the element E1 from the relation R and we have to add some things. Now there are two new variables which were not queried. What will I do with those variables? They will be given values which are not in the current database instance. That is exactly the user inputs or new inputs that you can give. So I just give values E5 and E6 there. So then I will get the resulting database as shown there in I3. I removed E1 from R but I added E5 into R. And I also added that E1, E6 into my Q, binary relation Q. So this is how the database instances keep changing over time. So basically we have these database-driven systems and the reachability problem on them. So you are given the set of actions of this description. You are given an initial database instance and some target proposition. The question is can we reach some database instance i in which this proposition is set to true? This problem is undecidable. It's not very surprising. And then that brings us to the notion of frequency bounding. It's an under approximation. In this one we are considering a limited system in which the retrieved objects by an action they must all belong to the most recently accessed objects. Let's say parameterized by a parameter B to the most recently accessed elements. So the question would be like this. The input, you have the set of actions, the initial database instance, the target proposition and the parameter B. And the question is by performing only this B reason C bounded actions, can you reach a database instance i in which the proposition is true? And this problem is decidable. This was a result from POTS 2016 which we did with a VHD student, Northman from Uppsala University. And in that work we did not just reachability but we also did linear time model checking against MSO. And in this work we lift the result on reachability to the setting with numerical data. And the proof technique is different because the result won't go through any way to linear time model checking we will see. And the previous result was by some encoding via nested words or trees if you want and here it is by a reduction to push down automatically. So what are these database driven systems with numerical attributes? So the same thing as before. We have the uninterpreted data and the uninterpreted relations which is given by the schema. And now we add an interpreted data which is rational numbers, the numerical data and an implicit relation on them which is the order. And how do we maintain this? So one possibility there are several ways of doing it. Maybe we can have schemas with type attributes etc. And then the queries will have to do a type checking and we did not want to get into that. So the way we do it is we will just add on every object from the unbounded data domain with a numerical value. And this numerical value is denoted by sharp E. This operator will return a numerical value. So basically the element E comes from the unbounded data domain which is uninterpreted and the sharp E will give you a rational number from this. And of course in the queries you can use the basic atomic objects like you can check whether two uninterpreted objects belong to a relation from your schema. And when you are you can also compare the numerical values for the order relation. And of course the action queries can make use of this. So this is an example of an action now in the new setting. So basically this action ask you to return two values for U and V. U should be in the relation R. But V, U should not be in the relation, binary relation Q. Such that the value of, numerical value of U is smaller than the numerical value of V. And then we delete some tuples and then we add some tuples as before. In fact we can, so notice that here in the right hand side we had the variables V1, V2, V are not using V. In fact we can also make constraints with the newly added values as well. For example, my condition could be that the numerical value of the newly added object V1 is smaller than that of V. So how do these things evolve now? So let's take this one as our example. This is the current database instance. And so in the active domain now we have six elements, E0 to E5. Let's assume that these are the numerical values associated to them. Now suppose, let's also assume that they have some recency index. So this basically means that E3 is the most recent element. This is the recency index is zero. It was just accessed just now. E4 and E5, they were accessed one step before. And E2 were accessed even one more step before. So the recency index is two. So the most recent element is the one with the index zero. The next is the one with index one and so on. Suppose that we want to now execute this particular action. Now let's try to get some assignment that will satisfy this one. For you, for example, we can take something that is in R. Let's take E4, for example. And then for V, we have to find something that is not related to U by Q. I think here I take E1. So this E1 and E4, both of them have recency less than one. So if within a recency bound of one or two, whichever way you want to see it, these are feasible answers. But taking V to be E0 might not be a feasible answer if my recency bound is just one and not two. So this is the kind of restriction that we will put when we put the bound on recency. For the moment, we are not considering the bound on recency, but just on the dynamics. So V can be E1. And now I have to give values for V1 and V2. So I again look at my domain, the huge domain. I have to pick some element, let's say E6, for example. But then I have that condition which says that the numerical value of that is less than the value that I picked, numerical value of V, which is E1. Numerical value of E1 is one. So this is not good enough. So I pick another one, E7. And for V2, since I don't have any constraints, I can pick E6, for example. So that gives a satisfying assignment. And then that instantiates the action template and the action tag can take place. This is basically to add the tuple E4, E6 to the binary relation Q, and to remove E4 and replace it with E7. Now what happens is that the active domain, you have to add these things. And the recency indices needs to be updated. So the elements which are touched by the most recent action, they get the recency index 0 now, the blue ones. The previous ones are, I mean, I did not update them yet. They need to be incremented by one. Well, E1, for example, it's going to be a rewriting. While for E3, for example, it has to be an increment. So we will update them accordingly. So the number of elements in the active domain can grow unbounded. The recency index can also be unbounded. But given the bound B, we want the actions to only retrieve elements from the most B indices, the least B indices. And so then another thing that I wanted to show here was that the numerical value can repeat. The numerical value associated to E6 is same as that was E0. So the numerical values can repeat. There is no such condition assumed for the numerical value. Just the uninterpreted objects are all distinct and unique. And the recency is applied on them. Whether a numerical value is queried or not is not important for the recency. Basically the uninterpreted values are the ones which are going in the tables. And now we consider the reachability problem under recency bounding, which is now it's a database manipulating system with numerical constraints, the initial database instance, the target proposition, and the bound on recency B. The question is, can we reach a database instance I using only B-bounded, B-resency-bounded actions such that the proposition B is true there? And this problem is exponential time complete. So basically we reduce it to a pushdown automaton. Let me see if I can tell you. So roughly a pushdown automaton, what we will do is we will keep every recency index level as some object. So the stack, the inverted stack is what you see there as the recency indices roughly. But then the difficulty now is that we also have the numerical values. We also have to keep the order between them. We will use some symbolic representation. We will keep an ordering between the recency window symbolically. And the number of such possibilities you will have is already exponential. If you have B elements, the number of different orderings between them is already exponential. So using some exponential sized stack alphabet. And this thing you, we can simulate these things using a pushdown automaton. We also need to relate the connections between the current recency window and the next recency window I will be extracting. And every time I need to maintain this. Roughly that's the idea. So we will have a finite abstraction of the order relation on the numerical value of the recent objects. So the recent includes not just the B recent objects, but also some more in order to make a faithful keep tracking of this thing. And this will cause an exponential slice blow up. And we get a pushdown automaton and the problem reduces to reachability in that, which is well, now become, which now becomes exponential time complete. And we also have a reduction in the other way around. Already without the numerical values, the reachability would become extreme hard. Now if we replace the reachability by linear time model checking, the problem becomes undecidable because we can easily have free cell TL for example. Instead using the LTL we can talk about non-repetition of values we can, or we can easily simulate at your contra machine as well. So well, these are our results, the X time completeness and the undecidability of going beyond. Thank you. Thank you.
 I am Aishwarya, I am from Chennai Mathematical Institute.  This is a joint work with Parosh Aziz Abdullah and Mohamed Fosya, I think, from Uppsala  University and Marco Montalhi from University of Bursan, Borsano.  I am rather new to this community, so I don't know most of you.  You may not know me either.  So this is actually a continuation of our work on verification of database-driven systems.  This time we add numerical attributes to it.  So we will start by looking at the terms on the title to see what they are.  And the motivation to study this is, of course, verification of database-driven systems like  business processes or something which are working over relational and numerical data.  The database-driven systems that we consider are relational databases over unbounded data  domain and a finite schema, basically relations with arbitrary RIT.  And the system can transform some given database instance to another by performing actions.  We will see what this will be more closely.  There are various formalisms for database-driven systems as well.  The particular one that we use are called database-manipulating systems which are described  by these actions.  And what can these actions do?  These actions will query the current database instance and it will, from the set of answers  to that query, it will retrieve one tuple non-deterministically and will delete some tuples from the current  instance as dictated by the action and will add some tuples into the relations again as  specified by the actions.  And these additions can involve new values which are not currently present in the database.  So the size of the database instance can grow and it's unbounded.  So in general, this graph that you see over there, that can be an infinite graph.  So we see an example.  This is an example of an action.  So the action is a template, let us say.  It uses variables.  It has a query here and let's consider I1.  So the query just asks you to return a U such that R of U is satisfied and there are two  possible answers.  And we pick non-deterministically one.  Let's pick E1.  And with this E1, now we will instantiate this transition into a more concrete transition.  Of course, we will replace the occurrences of U with E1.  That means that we have to delete the element E1 from the relation R and we have to add  some things.  Now there are two new variables which were not queried.  What will I do with those variables?  They will be given values which are not in the current database instance.  That is exactly the user inputs or new inputs that you can give.  So I just give values E5 and E6 there.  So then I will get the resulting database as shown there in I3.  I removed E1 from R but I added E5 into R.  And I also added that E1, E6 into my Q, binary relation Q.  So this is how the database instances keep changing over time.  So basically we have these database-driven systems and the reachability problem on them.  So you are given the set of actions of this description.  You are given an initial database instance and some target proposition.  The question is can we reach some database instance i in which this proposition is set  to true?  This problem is undecidable.  It's not very surprising.  And then that brings us to the notion of frequency bounding.  It's an under approximation.  In this one we are considering a limited system in which the retrieved objects by an action  they must all belong to the most recently accessed objects.  Let's say parameterized by a parameter B to the most recently accessed elements.  So the question would be like this.  The input, you have the set of actions, the initial database instance, the target proposition  and the parameter B. And the question is by performing only this B reason C bounded actions,  can you reach a database instance i in which the proposition is true?  And this problem is decidable.  This was a result from POTS 2016 which we did with a VHD student, Northman from Uppsala  University.  And in that work we did not just reachability but we also did linear time model checking  against MSO.  And in this work we lift the result on reachability to the setting with numerical data.  And the proof technique is different because the result won't go through any way to linear  time model checking we will see.  And the previous result was by some encoding via nested words or trees if you want and  here it is by a reduction to push down automatically.  So what are these database driven systems with numerical attributes?  So the same thing as before.  We have the uninterpreted data and the uninterpreted relations which is given by the schema.  And now we add an interpreted data which is rational numbers, the numerical data and  an implicit relation on them which is the order.  And how do we maintain this?  So one possibility there are several ways of doing it.  Maybe we can have schemas with type attributes etc.  And then the queries will have to do a type checking and we did not want to get into that.  So the way we do it is we will just add on every object from the unbounded data domain  with a numerical value.  And this numerical value is denoted by sharp E. This operator will return a numerical value.  So basically the element E comes from the unbounded data domain which is uninterpreted  and the sharp E will give you a rational number from this.  And of course in the queries you can use the basic atomic objects like you can check whether  two uninterpreted objects belong to a relation from your schema.  And when you are you can also compare the numerical values for the order relation.  And of course the action queries can make use of this.  So this is an example of an action now in the new setting.  So basically this action ask you to return two values for U and V. U should be in the  relation R. But V, U should not be in the relation, binary relation Q. Such that the  value of, numerical value of U is smaller than the numerical value of V. And then we  delete some tuples and then we add some tuples as before.  In fact we can, so notice that here in the right hand side we had the variables V1, V2,  V are not using V. In fact we can also make constraints with the newly added values as  well.  For example, my condition could be that the numerical value of the newly added object  V1 is smaller than that of V. So how do these things evolve now?  So let's take this one as our example.  This is the current database instance.  And so in the active domain now we have six elements, E0 to E5.  Let's assume that these are the numerical values associated to them.  Now suppose, let's also assume that they have some recency index.  So this basically means that E3 is the most recent element.  This is the recency index is zero.  It was just accessed just now.  E4 and E5, they were accessed one step before.  And E2 were accessed even one more step before.  So the recency index is two.  So the most recent element is the one with the index zero.  The next is the one with index one and so on.  Suppose that we want to now execute this particular action.  Now let's try to get some assignment that will satisfy this one.  For you, for example, we can take something that is in R. Let's take E4, for example.  And then for V, we have to find something that is not related to U by Q.  I think here I take E1.  So this E1 and E4, both of them have recency less than one.  So if within a recency bound of one or two, whichever way you want to see it, these are  feasible answers.  But taking V to be E0 might not be a feasible answer if my recency bound is just one and  not two.  So this is the kind of restriction that we will put when we put the bound on recency.  For the moment, we are not considering the bound on recency, but just on the dynamics.  So V can be E1.  And now I have to give values for V1 and V2.  So I again look at my domain, the huge domain.  I have to pick some element, let's say E6, for example.  But then I have that condition which says that the numerical value of that is less than  the value that I picked, numerical value of V, which is E1.  Numerical value of E1 is one.  So this is not good enough.  So I pick another one, E7.  And for V2, since I don't have any constraints, I can pick E6, for example.  So that gives a satisfying assignment.  And then that instantiates the action template and the action tag can take place.  This is basically to add the tuple E4, E6 to the binary relation Q, and to remove E4  and replace it with E7.  Now what happens is that the active domain, you have to add these things.  And the recency indices needs to be updated.  So the elements which are touched by the most recent action, they get the recency index  0 now, the blue ones.  The previous ones are, I mean, I did not update them yet.  They need to be incremented by one.  Well, E1, for example, it's going to be a rewriting.  While for E3, for example, it has to be an increment.  So we will update them accordingly.  So the number of elements in the active domain can grow unbounded.  The recency index can also be unbounded.  But given the bound B, we want the actions to only retrieve elements from the most B  indices, the least B indices.  And so then another thing that I wanted to show here was that the numerical value can  repeat.  The numerical value associated to E6 is same as that was E0.  So the numerical values can repeat.  There is no such condition assumed for the numerical value.  Just the uninterpreted objects are all distinct and unique.  And the recency is applied on them.  Whether a numerical value is queried or not is not important for the recency.  Basically the uninterpreted values are the ones which are going in the tables.  And now we consider the reachability problem under recency bounding, which is now it's  a database manipulating system with numerical constraints, the initial database instance,  the target proposition, and the bound on recency B.  The question is, can we reach a database instance I using only B-bounded, B-resency-bounded actions  such that the proposition B is true there?  And this problem is exponential time complete.  So basically we reduce it to a pushdown automaton.  Let me see if I can tell you.  So roughly a pushdown automaton, what we will do is we will keep every recency index level  as some object.  So the stack, the inverted stack is what you see there as the recency indices roughly.  But then the difficulty now is that we also have the numerical values.  We also have to keep the order between them.  We will use some symbolic representation.  We will keep an ordering between the recency window symbolically.  And the number of such possibilities you will have is already exponential.  If you have B elements, the number of different orderings between them is already exponential.  So using some exponential sized stack alphabet.  And this thing you, we can simulate these things using a pushdown automaton.  We also need to relate the connections between the current recency window and the next recency  window I will be extracting.  And every time I need to maintain this.  Roughly that's the idea.  So we will have a finite abstraction of the order relation on the numerical value of the  recent objects.  So the recent includes not just the B recent objects, but also some more in order to make  a faithful keep tracking of this thing.  And this will cause an exponential slice blow up.  And we get a pushdown automaton and the problem reduces to reachability in that, which is  well, now become, which now becomes exponential time complete.  And we also have a reduction in the other way around.  Already without the numerical values, the reachability would become extreme hard.  Now if we replace the reachability by linear time model checking, the problem becomes undecidable  because we can easily have free cell TL for example.  Instead using the LTL we can talk about non-repetition of values we can, or we can easily simulate  at your contra machine as well.  So well, these are our results, the X time completeness and the undecidability of going  beyond.  Thank you.  Thank you.
Abdulla_Aiswarya_Atig_Montali_0_143.png Abdulla_Aiswarya_Atig_Montali_144_1307.png Abdulla_Aiswarya_Atig_Montali_1308_1583.png Abdulla_Aiswarya_Atig_Montali_1584_1895.png Abdulla_Aiswarya_Atig_Montali_1896_3671.png Abdulla_Aiswarya_Atig_Montali_3672_5999.png Abdulla_Aiswarya_Atig_Montali_6000_6983.png Abdulla_Aiswarya_Atig_Montali_6984_8267.png Abdulla_Aiswarya_Atig_Montali_8268_9467.png Abdulla_Aiswarya_Atig_Montali_9468_9827.png Abdulla_Aiswarya_Atig_Montali_9828_11831.png Abdulla_Aiswarya_Atig_Montali_11832_13235.png Abdulla_Aiswarya_Atig_Montali_13236_13859.png Abdulla_Aiswarya_Atig_Montali_13860_14687.png Abdulla_Aiswarya_Atig_Montali_14688_17819.png Abdulla_Aiswarya_Atig_Montali_17820_19151.png Abdulla_Aiswarya_Atig_Montali_19152_19295.png Abdulla_Aiswarya_Atig_Montali_19296_19943.png Abdulla_Aiswarya_Atig_Montali_19944_20099.png Abdulla_Aiswarya_Atig_Montali_20100_20927.png Abdulla_Aiswarya_Atig_Montali_20928_21119.png Abdulla_Aiswarya_Atig_Montali_21120_21263.png Abdulla_Aiswarya_Atig_Montali_21264_22871.png Abdulla_Aiswarya_Atig_Montali_22872_22919.png Abdulla_Aiswarya_Atig_Montali_22920_24791.png Abdulla_Aiswarya_Atig_Montali_24792_24911.png Abdulla_Aiswarya_Atig_Montali_24912_25041.png