Hypothetical Temporal Reasoning in Databases.
In this paper we integrate a historyencoding based methodology for checking dynamic database integrity constraints into a situation-calculus based specification of relational database updates. By doing this, we are able to: (1) Answer queries about a whole hypothetical evolution of a database, without having to update the entire database and keep all the information associated to the generated states, (2) State and prove dynamic integrity constraints as static integrity constraints, (3). Transform history dependent preconditions for updates into local preconditions.The methodology presented here is based on the introduction of operators of predicate past temporal logic as macros into the specifications, written in the situation calculus, of the dynamics of a database. Temporal subformulas of a query are treated as auxiliary views with the corresponding specification of their dynamics. An implementation of hypothetical temporal query answering is presented.
Introduction
In (Reiter, 1995), as an application of his solution to the frame problem
(Reiter, 1991), Ray Reiter proposed to specify the transaction based
updates of a relational database by means of a particular kind of axioms
written in the situation calculus (SC) (McCarthy et al., 1969).
In (Bertossi et al., 1998) the implementation and the functionalities of
SCDBR, a computational system for doing automated reasoning from
and about those specications (Bertossi et al., 1998), are reported.
We are motivated by the problem of answering queries about dier-
ent states 1 in the evolution of a relational database, when the database
is virtually updated by the execution of a sequence of primitive trans-
actions, that are indecomposable and domain dependent transactions.
Dedicated to the memory of our dear friend and colleague Javier Pinto (1959-
2001), who made important contributions to the logical foundations of the situation
calculus.
y Current address: University of Toronto, Dept. of Computer Science, Toronto,
Canada. marenas@cs.toronto.edu.
1 In this paper we do no make any distinction between states and situations.
c
2001 Kluwer Academic Publishers. Printed in the Netherlands.
For example, we want to consider queries of the form \Has it always
been the case that the database has satised a given condition C?", or
\Has there been a state of the database where a certain condition C has
been satised?", or \Has the salary of some employee decreased along
the database evolution?". Reiter raised this problem in the context of
his specications of transaction based database updates (Reiter, 1995).
Although there is no explicit time in our situation calculus, we call
these queries \temporal queries", due to their similarity with dynamic
constraints (Reiter, 1995), also called \temporal constraints"
(Chomicki, 1995) 2 . Furthermore, we call these queries \hypothetical"
because we start from an initial, physical database at an initial state,
list T of primitive transactions A virtually
update the database, producing new states S we want to
answer a query about the generated sequence of states, without physically
updating the whole database accordingly (and possibly keeping
the data for every intermediate state). We are interested in querying
this whole virtual evolution of the database.
The problem of answering this kind of queries was treated in detail
in (Siu et al., 1996) and a solution was implemented as reported in
(Bertossi et al., 1998). Nevertheless that solution is based on a kind of
minimal progression of the database that depends on a detailed syntactical
processing of the axioms of the specication, and the particular
syntactical form of them.
In this paper we reconsider this problem and we propose a new
solution that relies on processing the query itself, rather than the underlying
axioms. This is done on the basis of (1) a formulation of the
query in a situation calculus language that contains temporal operators
inspired by rst order past temporal logic (FOPTL) (Gabbay et al.,
1994), (2) a reformulation of Chomicki's history encoding methodology
for eciently checking temporal integrity constraints (Chomicki, 1995),
in the context of situation calculus specications of database updates,
and, in particular, (3) a specication in the situation calculus of the
evolution of new history encoding auxiliary relations that are generated
from the query.
It turns out that the methodology we develop for answering queries
can be adapted to give a solution to other reasoning problems. Here
we show how to transform dynamic integrity constraints into static
constraints, so that any available methodology for handling
2 Sometimes, in the literature, they are called \historical queries", but this name
may cause confusions with work done by the temporal databases community that
calls \historical" the queries about valid time, rather than about transaction time
(Snodgrass et al., 1986), which can be better associated to the situations of the
situation calculus.
Hypothetical Temporal Reasoning 3
static integrity constraints can be adapted for the dynamic case. In
particular, we can take advantage of our results on automated proving
of static integrity constraints (Bertossi et al., 1996) when dealing with
the dynamic case.
The other problem we solve consists in transforming preconditions
for action executions that depend on the history of the database into
preconditions that depend on the local, execution state.
This paper is concerned mainly with the problems of modeling and
doing hypothetical reasoning in databases, a subject that has not received
enough attention (but see (Bonner, 1990; Bonner et al., 1998;
Chen, 1997)). We think hypothetical reasoning will become more and
more important in databases that are used for decision support, where
\what if" questions are relevant, as the ones emerging in on-line analytical
processing (OLAP) and datawarehousing (Chaudhuri et al.,
1997). To have computational tools that can be used to explore dierent
courses of action without having to commit to any of them; in partic-
ular, without having to physically update the database, is likely to be
very important in many applications of information systems, specially
in the presence of rich primitive transactions, like ours, that may aect
several tables at the same time.
This paper is structured as follows. In section 2 we brie
y describe
the situation calculus based specications of database updates. In section
2.1, we introduce temporal queries and constraints in a situation
calculus framework. In section 3.1 we introduce our language for posing
temporal queries. In section 3.2 we introduce the elements we need
to evaluate queries, in particular, the specication of the dynamics of
the auxiliary, history encoding, views; and we address the problem of
answering the hypothetical temporal queries. In section 4 we apply the
machinery developed in previous sections to the problem of transforming
dynamic integrity constraints into static integrity constraints. In
section 5 we apply our methodology to the problem of transforming
history dependent transactions, i.e. transactions whose preconditions
are temporal, into transactions with local conditions. In section 6 we
sketch some possible extensions of the methodologies introduced in
the previous sections. In section 7 we compare our work with other
approaches in the literature, we comment on further work, and draw
some conclusions. In appendix A, we illustrate our implementation of
the developed methodology. In appendix B some proofs are given.
2. Specifying the Database Dynamics
We will show the main ingredients of a specication in the situation
calculus of transaction based database updates, as proposed in (Reiter,
1995). The SC is a family of languages of many sorted predicate logic
used to represent knowledge and reason about dynamic domains that
are subject to discrete changes caused by action executions. In its
languages, we nd domain individuals, states and primitive transac-
tions, i.e. domain specic and indecomposable transactions, that we
will also call \actions", and which are at the same rst order level. In
consequence, rst order quantication over all these sorts of individuals
is possible. They are usually denoted by 8x, 8s, 8a, respectively.
Among others we nd the following advantages in using the SC
as a specication language: (1) It has a clear and well understood
semantics. (2) Everything already done in the literature with respect to
applications of predicate logic to DBs can be done here, in particular,
all static and extensional aspects of databases and query languages are
included. (3) Dynamic aspects can be integrated at the same object
level, in particular, it is possible to specify how the database evolves as
transactions are executed. (4) It is possible to reason in an automated
manner from the specication and to extract algorithms for dierent
computational tasks from it. (5) In particular, it is possible to reason
explicitly about DB transactions and their eects. (6) In this form, it
is possible to extend the functionality of usual commercial DBMSs.
In every SC language we nd a constant for an initial state, S 0 , a
function symbol, do, so that do(a; s) denotes the successor state that
results from the execution of action a at state s. We also nd a pred-
icate, Poss(a; s), with the intended meaning that action a is possible
at state s. In a particular SC language we will nd function names for
parameterized primitive transactions (actions), A(x), and names for
tables, F (x; s), that is, predicates with a single state argument 3 . If T
is a sequence of action terms A , to be executed in that order,
we abbreviate the situation
simply do(T ; s).
As in (Lin et al., 1994), we will assume that the following foundational
axioms of the situation calculus underlie any database spec-
ication 4 : 1. Unique Names Axioms for Actions: A i (x) 6= A j (y),
3 They can be seen as usual database tables whose entries have an additional state
stamp that is not stored in the extensional databases. In the knowledge representation
literature they are usually called \
uents". States are used for distinguishing
the successive snapshots of the database.
4 In this paper, a \database specication" always means a specication of the
dynamics of a database.
Hypothetical Temporal Reasoning 5
for all dierent action names A
y]. 2. Unique Names Axioms for States: S 0 6= do(a; s), do(a
3. For some reasoning tasks we need an
Induction Axiom on States: 8P [(P (S 0 )^8s8a (P
A specication of the transaction based updates on a particular
database will contain the following axioms: 4. A set,  0 , of SC
sentences that do not mention any state term other than S 0 . This is
knowledge about the initial state, and state independent knowledge. 5.
Action Precondition Axioms: For each action name A, a precondition
axiom of the form
where A (x; s) is a SC formula that is simple in s, that is, it contains no
state term other than s, in particular, no do symbol, no quantications
on states, and no occurrences of the Poss predicate (Reiter, 1995). 6.
Successor State Axioms (SSAs): For every table F (x; s), an axiom of
the form
where  F is a formula simple in s, in particular, it does not contain the
do symbol. Provided there is complete knowledge at the initial state,
as is usually the case in relational databases, this axiom completely
determines the contents of table F at an arbitrary legal database state,
i.e. reached from S 0 by a nite sequence of transactions that are possible
at their execution states. We are usually interested in reasoning about
the states that are accessible in this form from the initial situation. For
this purpose, an accessibility relation on states, , can be dened on
the basis of the induction axiom by means of the conditions: :s < S 0 ,
We will denote this specication with . It includes the initial data-base
0 and the denition of the accessibility relation.
Example 1. Consider a database of a company, with the following
relations:
Person x is an employee of the company when
the database is in state s.
Person x is a chief executive ocer of the
company, in the state s.
The salary of the person x is p in the state s.
and primitive transactions:
6 Arenas, Bertossi
Person x is hired by the company.
Person x is red by the company.
Person x is promoted to chief executive ocer.
changeSalary The salary of the person x is changed to p
dollars.
The specication of the initial database has the the following formulas:
ernest _
sue ernest ; sue 6= page ;
john ernest ; john 6= page; ernest
That is, John, Ernest and Page are the only employees of the company
at the initial database state.
The relations in this specication have the following successor state
axioms (see
For example, the rst SSA says that x is an employee at an arbitrary
legal successor state if he was just hired or he already was an employee
and he was not red in the transition to the successor state.
Now, assume that we have the following precondition axioms for the
actions in the database.
applied to
a formula containing a successor state returns an equivalent formula
Hypothetical Temporal Reasoning 7
(with respect to the specication) evaluated at the preceding state. This
is done by using the SSAs. More precisely, if predicate F , appearing in
a formula , has a SSA like (2), then the operator, R, applied to ,
replaces each occurrence of an atomic formula of the form F (
t; do(a; s))
in by  F (  t; a; s).
The regression operator is implemented in SCDBR, a computational
system for reasoning about and from specications of database
dynamics as presented in this section (Bertossi et al., 1998).
2.1. Temporal queries and constraints
In the context of such DB specications, a temporal query is a SC sentence
' in which all the states involved, including quantied states, lie
on a nite state path S 0  S 1      S n , with
a sequence of ground actions terms A
some n. The query is true if and only if
Example 2. In example 1, the temporal query \Has Sue been working
in the company in all states generated by sequence T at S 0 ?" can be
expressed in the SC by means of 8s (S 0  s  S n  Emp(sue; s)).
The following sentence could be also a temporal query
It asks whether the salary has not decreased. 2
A static integrity constraint is a formula of the form 8s(S 0  s
'(s)), where '(s) is simple in the state variable s, such that
is expected to hold (Reiter, 1995; Lin et al., 1994).
A dynamic (or temporal) integrity constraint is a SC sentence of
the form 8s 1    8s n (C(S that should be
entailed by . Here, C(S that imposes a linear
order constraint on the states S in terms of the accessibility
predicate  5 .
Example 3. The sentence 8s (S 0  s  8p
could be a static integrity constraint, stating that Sue's salary
can not be lower than 4000. The sentence
5 Dynamic integrity constraints are usually of this form, but the results we will
present in this paper still hold if we admit more involved quantications on several
states, related by the accessibility relation.
8 Arenas, Bertossi
is a dynamic integrity constraint expressing that a salary never de-
creases. 2
In general, we will not have explicit integrity constraints in our spec-
ication, , of the database dynamics. We expect them to be logical
consequences of  (Reiter, 1995; Lin et al., 1994).
In the next section we will introduce temporal operators as found
in past temporal logic into the situation calculus. With these operators
we will formulate queries and constraints, and their new syntactic form
will allow us to process and evaluate them.
3. Answering Queries
In (Chomicki, 1995), the problem of checking temporal constraints
stated in FOPTL was considered. These are constraints that talk about,
and relate, dierent states of the database. There we nd a sequence
of transactions that are physically executed, and in order to minimize
the cost of checking, one progressively updates new dened relations,
or auxiliary views, r  , that correspond to the temporal subformulas, ,
in the constraint. These views encode part of the database evolution
up to a current database state. They are dened and updated in such a
way that they store the historical information that is relevant to give an
answer to the query about the satisfaction of the integrity constraint
once the nal (current) state is reached. Then a new, non-temporal,
but local and static query can be posed at the nal state.
In this paper we will combine our reconstruction of Chomicki's history
encoding in the context of specications of the dynamics of a
database with the possibility, opened by those specications, of reasoning
about the database evolution without having to physically update
the database. In consequence, we will be in position to do hypothetical
temporal reasoning about the database evolution. We can say that
while Chomicki answers the query by positioning at the nal physical
state of the database, we query a single future, virtual state from
the initial, physical state. The fact that we are doing virtual updates
makes it possible to apply our methodology to any temporal query,
whereas, in the presence of physical updates, the queries have to be
xed, predetermined in advance 6 .
6 This is not a limitation if, as in (Chomicki, 1995), one is interested in some
xed dynamic integrity constraints only, but not in arbitrary temporal queries, as
we are.
Hypothetical Temporal Reasoning 9
3.1. A Query Language
As discussed in section 2.1, a temporal query is a sentence ' in which
all the states involved, including the quantied states, lie on a -
nite state path S 0  S 1      S n , with
a sequence of ground actions terms A
In order to answer this kind of queries on an algorithmic basis, we
need to dene them in a precise sense. Thus, we need to dene a query
language for asking about the history of a sequence of states. To achieve
this, we will introduce in the situation calculus some temporal operators
inspired by rst order past temporal logic, and a macro, holds. With
these new elements we will be in position to represent an important
class of temporal queries. Nevertheless, if desired, the application of
holds to a formula with temporal operators could be always rewritten
into a usual situation calculus formula.
The SC contains predicates with a state as an argument. For ex-
ample, we use P (a; s) to state that a is an element of table P in the
state s. We may eliminate the situation term from predicate P , and use
a new meta-predicate, holds, and write holds(P (a);s) with the same
meaning as before. Actually, we would like to extend the application
of holds to more complex formulas, derived from SC formulas, but
keeping the state dependency in the second argument of holds.
Denition 1. A formula ' is state suppressed (an ss-formula) if it is
constructed as usual from state independent predicates, state dependent
predicates (i.e. database tables or
uents) with the state argument
supressed, boolean connectives, and rst order quantications on domain
individuals. 2
For example, the following is an ss-formula: 8x9p (Ceo(x)^Emp(x; p)
7 The state arguments have been suppressed from the
tables. Predicate holds will have an ss-formula in its rst argument,
and a state in the second argument. This would make holds a second
order predicate. We can go back to rst order expressions by considering
holds as a macro, as an abbreviation, as something that can be
rewritten into an expression of the original situation calculus. Thus,
holds(';s), where ' is an ss-formula, is dened recursively as follows:
7 We should use new predicates, say Emp(;
should be no confusion.
is a state independent predicate
holds(F (x);s) := F (x; s), if F is a predicate for a database table
holds(:';s) := :holds(';s)
holds(' _  ;s) := holds(';s) _ holds( ;s)
holds('   ;s) := holds(';s)  holds( ;s)
holds('   ;s) := holds(';s)  holds( ;s)
holds(9x';s) := 9xholds(';s), if x is a variable for domain
individuals
holds(8x';s) := 8xholds(';s), if x is a variable for domain
individuals.
An advantage of using the macro holds is that we can extend the
class of formulas ' in holds(';s), in such a way that they contain
new, temporal operators that represent subformulas with some useful,
natural and common quantication over states. In addition, we can
make the nal, evaluation state, s, explicit. For example, we want to
represent in a compact and distinguishable way the formula 8s 0 (S 0
which says that a is an element of table P in every
state previous to s, without using an explicit quantication over states.
For doing this, we introduce a logical temporal operator, 2, dened by
More precisely, for posing temporal queries, we will introduce in the
SC the four typical temporal operators of rst order past temporal
logic, the same operators considered in (Chomicki, 1995). The intended
meanings of them are: (a) ' for \' was true at the previous moment
of time". (b) ' since for \ was true at some time in the past and
from that time on, ' has been true". (c) 3' for \Sometime in the past
' was true". (d) 2' for \Always in the past ' was true". 8
They will be introduced as macros though, via the holds predicate.
In consequence, the class of ss-formulas (denition 1) has to be extended
by means of the extra rule: If ';   are ss-formulas, then ', ' since ,
3', 2' are also ss-formulas.
8 The last two operators can be dened in terms of the rst two by 3' := True
since ', and 2' := :3:'.
Hypothetical Temporal Reasoning 11
The combinations of holds and the temporal operators are dened
by the following macros, that can be rewritten as SC formulas as
follows:
holds(' since ;s) := 9s 0 (S
This is is a recursive denition. In it, ' and are formulas that
may include connectives :, _, ^,  and ; quantication over domain
individuals; and operators , since, 3 and 2.
From now on, our temporal query language will consist of the formulas
we just dened. More precisely, our temporal queries will be of
the form
where ' is an ss-formula and T is a sequence of ground actions.
Formula ' in (4) will possibly contain temporal operators, that is,
it may contain subformulas starting with an application of a temporal
operator. In section 3.2, to each of these subformulas, , we will
associate a new, auxiliary, history encoding view, R  . Next, for these
views we will derive specications of their dynamics, and use them in
the process of query answering. Before doing this, we present some
examples of temporal queries expressed in terms of the new operators.
Example 4. We can express the queries shown in example 2 as follows.
\Has Sue been working in the company in all states generated by a sequence
of actions T at S 0 ?": holds(Emp(sue)^2Emp(sue);do(T
\Is is true that the salaries have never decreased along the states generated
by action sequence T executed at S 0 ?":
2(Salary
Example 5. The query \Was Joe hired as an employee of a lower rank
before becoming a Chief Executive Ocer (CEO) in all states generated
by a sequence of actions T at S 0 ?" can be expressed by the formula
Example 6. The query \Is there anybody who has always been working
in the company (along the execution of the sequence of actions T from
can be expressed by the formula
)):With the temporal operators we can express an interesting and
natural class of temporal queries. The introduction into the situation
calculus of the temporal operators cannot substitute for the whole
expressive power of the situation calculus (Abiteboul et al., 1996),
nevertheless we can express with them the queries we need in most
common practical applications.
3.2. Evaluating the Query
Our starting point consists of a SC specication  as in section 2,
and a query holds(';S), where ' is an ss-sentence, possibly containing
temporal operators, to be evaluated at the nal state
As expected, this formula implicitly refers to the states between S 0 and
S.
In order to answer the query, we will construct a new SC specication
H that extends , and a new SC sentence, H(';S), such that the
answer to the original query,  coincides with the
answer obtained from the evaluation of H(';S) with respect to H .
The new sentence, H(';S), refers only to the state S, and H contains
a specication of the dynamics of some new, history encoding, auxiliary
relations that correspond to the temporal subformulas in '. Being in
this new scenario, we can use any algorithm for answering that refer to
a single, future state of the database.
First we will generate H(';S), for an ss-formula ' and ground state
S. Next, we will show how to generate H .
1. If ' is of the form t 1  t 2 , where t 1 and t 2 are terms (for domain
2. If ' is of the form P (  is a state independent predicate,
then H(';S) := P (  t).
3. If ' is of the form F (  t), where F is a predicate for database table,
then H(';S) := F (  t; S).
4. If ' is : , then H(';S) := :H( ;S).
Hypothetical Temporal Reasoning 13
5. H(  ;S) := H( ;S)  H(;S), where  is any of the usual binary
propositional connectives.
6. H(Qx ';S) := Qx H(';S), where Q is any of the usual rst order
quantiers.
7. If ' is  (x), 3 (x) or 2 (x), where does not contain any of
the operators , since, 3 and 2, then H(';S) := R ' (x; S), where
R ' is a new table name.
8. If '(x) is (x) since (x), where (x) and (x) do not include
any of the operators , since, 3 and 2, then H(';S) := R ' (x; S),
where R ' is a new table name.
By bottom{up transformation of a formula ' that appears in the
macros holds, we can always obtain such a formula H(';S). Notice that
this is a SC formula that is simple in the state S, i.e. it talks about an
isolated state, S.
Now, we will specify the dynamics of the new tables introduced
in the last two cases in the inductive denition above by means of
appropriate SSAs:
(a) Let (x) be of the form  (x). This formula is true at a given state
i (x) is true at the previous state. Then, the new table R  (x; s)
has the following SSA: 8(a; s)P oss(a; s)  8x(R  (x; do(a; s))
H( (x);s)). At the initial state (x) is false for each
x, because S 0
has no predecessor state, so we specify 8x:R  (x; S 0 ).
(b) Let (x) be of the form (x) since (x). This formula is true at
a state s, with predecessor state s 0 , i ( since ) was true at s 0
and is still true at s, or became true at s and  became true
at s 0 . This is equivalent to saying that (( since ) _ ) is true at
s 0 and is true at s. Then, for R  (x; s) it holds:
This is not a SSA of the form (2), because there is a do(a; s) term
in one of the formulas on the RHS. But we can get rid of it applying
Reiter's regression operator R, that takes a formula, instantiated
at a successor state of the form do(a; s), into a formula instantiated
at the previous state, s (see section 2). So, we obtain:
14 Arenas, Bertossi
Notice that the application of the regression operator leaves the
RHS of the equivalence above as a simple formula in s. Also notice
that when  is a sentence, then the SC formula R
a situation dependent propositional predicate. Finally, we also
specify 8x:R  (x; S 0 ).
(c) Let (x) be of the form 3 (x). Given that 3 (x) := true since
(x), the new table R  has the specication:
Let (x) be of the form 2 (x). Since 2 (x) := :3: (x), R  has
the specication:
Example 7. Assume that the original specication  contains the
following SSA for the table P (x; s):
We want to evaluate the query 9x(P (x) since 3Q(x)) at state
then we introduce a new table R  with SSA:
Introducing R  in the query, we obtain 9x(P (x) since R  (x)). If the
formula inside the quantier is (x), for the new table R  we have
Replacing R[P (x; do(a; s))] by the RHS of the SSA for P , we obtain
the following SSA for R  :
The new query is 9xR  (x; S). 2
The following proposition shows why we can use H and H to answer
queries about a specication , constructed by using holds.
Hypothetical Temporal Reasoning 15
Proposition 1. Let  be a SC specication and T a legal sequence
of ground actions 9 , then
Notice that holds(';do(T ; S 0 )) is instantiated at the nal state
this is the only state mentioned in the formula. So, we
can see that we have transformed our problem of answering a temporal
query with respect to a virtually updated database into the temporal
projection problem of AI (Hanks et al., 1986), that is, the problem of
querying a future state obtained by the execution of a sequence of ac-
tions. To solve this problem we may apply some existing techniques for
Reiter like specications, e.g. Reiter's query regression (Reiter, 1995),
minimal rolling forward of the database based on information that is
relevant to the query (Bertossi et al., 1998; Siu et al., 1996), or even full
progression of the database (Lin et al., 1997). All these methodologies
are supported by the database reasoner SCDBR (Bertossi et al., 1998).
Example 8. We want to know if there is someone who has always
been working in the company, in all states generated by the execution
of the sequences of actions re(john)] from the initial
situation. So, we are asking whether
Applying our methodology we obtain the new SC query
and the original specication extended to H by adding 8xR
and
Then we ask if H
the query is simple in the nal state do(T ; S 0 ).
Running the regression operator twice on the RHS and simplifying
the resulting steps by means of the unique names axioms for actions,
we obtain the following query to be posed to the initial database
Simplifying R  (x; S 0 ) to true, we obtain the equivalent query
9 We say that a sequence of actions
SCDBR can answer this query by calling a conventional DBMS on the
initial database, or a Prolog program if the initial database is a Prolog
database. 2
The implementation in SCDBR of the methodology we have presented
so far is described in appendix A.
4. Transforming Dynamic Integrity Constraints
In section 2 we dened a Static Integrity Constraint (SIC) as a formula
of the form 8s(S 0  s  '(s)), where '(s) was a formula simple in s.
By using the macro holds we can extend this denition by saying that
a static integrity constraint is a formula of the form
If ' is a formula that does not include operators , since, 3 and
2, then the previous formula is a static integrity constraint of the
form showed in section 2. If ' includes these operators, then it can
represent a more complex kind of integrity constraint. In fact, by means
of this operators it is possible to represent several Dynamic Integrity
Constraints (DICs). Thus, by using the equivalence between macros
holds and H it is possible to transform a dynamic constraint in one
specication into static constraint in another specication.
Therefore, we can use our methodology to transform DICs into
SICs. Actually, the work in (Chomicki, 1995) has to do with checking
DICs statically. In our case, with our reformulation of Chomicki's
methodology in terms of a specication of the dynamics of the history
encoding relations, we can rewrite DICs as SC sentences expressing
SICs, which can be proven as such from the (extended) specication
of the database dynamics. In particular, we can use theorem proving
techniques for proving SICs by automated induction, like the ones
presented in (Bertossi et al., 1996), in order to automatically prove
DICs from the specication of the database dynamics.
The following proposition formalizes the idea showed above.
Proposition 2. Given a SC specication . If H is constructed from
as was showed in section 3.2, then
Example 9. Let  be the specication in example 1 and be the DIC
(3) telling that an employee's salary cannot decrease, that must hold
Hypothetical Temporal Reasoning 17
in every legal current state s of the DB. That is, as a sentence, it must
follow from .
We can express this integrity constraint in our extended format as
follows:
If create a table R  with specication:
R
Introducing R  in the rst argument of holds in (6) we obtain:
If is the subformula 2((R
we create a table R  with specication
R
Introducing R  in (8), we obtain
Thus, the original DIC holds in every state if and only if the specica-
tion H , consisting of  plus (7) and (9), entails the SIC:
The IC (10) can be split into the two binary static integrity constraints
As shown in (Pinto,
1994; Bertossi et al., 1998), these constraints can be compiled into the
specication of the extended database dynamics, in this case, modifying
the original SSAs for the new tables R  and R  .
5. History Dependent Transactions
As we saw in section 2, the formalism for specifying DB updates contains
preconditions for action executions that depend on the current
state of the database, only. Many concepts and algorithms that have
originated from this formalism are based on this kind of local action
precondition axioms (APAs). Nevertheless, there are natural scenarios
in which the conditions for executing an action should depend on a
longer history of the database. For example, in a voters database we
might have the following APA for action vote
That is, x can vote for y as long as y is a candidate, x is not younger
than 18, and x has never been in jail. This is a history dependent
transaction.
We can use the macros holds to represent this kind of actions. In
fact, we can extend the denition of action preconditions as follows:
If includes some of the operators , since, 3 or 2, we have a history
dependent action.
We can use the machinery developed so far for transforming history
dependent transactions into local transactions. To do this we only need
to construct a new specication  0
H from H , in its turn obtained from
H( (x);s) as before, but with the original APA (12) replaced by the new
APA:
which is of the form (1). As before, the new specication contains SSAs
for the auxiliary tables introduced by the construction of H( (x);s).
Proposition 3. Let  be a SC specication containing a history dependent
APA for action A and let H be the new SC specication
containing SSAs for the auxiliary relations and the old APA replaced
by the new, local one. If H and Poss H are the possibility predicate and
accessibility relation dened on the basis of the new APA, then it holds:
(a) For every ground state term S, and ground action term of the form
A(c),
Hypothetical Temporal Reasoning 19
(b) For every ground state term S,
proposition says that at every accessible state, action A is possible
in the old sense if and only if it is possible in the new sense and
that both specications dene the same accessible states.
Example 10. We can apply the methodology to the voters example.
In (11), the original APA for vote(x; y) can be expressed by means of
macros holds as follows:
In consequence, we generate a new specication  0
extending , that
includes now:
1. A new table R  (x; s) that contains, at state s, the people x that
have not been in jail before state s, whose specication consists of
2. The original APA for action A replaced by
6. Possible extensions
6.1. Explicit time.
In (Chomicki, 1995), explicit time was also included to extend history
encoding and deal with real-time issues. In (Arenas et al., 1998d) it is
shown how to extend our methodology by introducing explicit time in
the database. This can be done by considering time as a new parameter
for actions (Reiter, 1996). In this way, situations will have their
associated times. Here we give only some hints on how explicit time
can be accommodated into our framework.
As before, primitive actions will be denoted with function symbols,
but now with one extra parameter of a new, temporal sort T . Thus,
a would denote the instantaneous action of borrowing
a book at time t 1 . We also include a new function time from
actions to T , such that, for each action function A(x;
the axiom time(A(x; t. Therefore, if borrow(book is an action
term, then we would have time(borrow(book We also need
a function, start , from situations to times, such that start(s) is the
starting time for situation s. Since actions are instantaneous, we require
that start(do(a; (Reiter, 1998). Nevertheless, situations
may have a duration (Baier et al., 1998).
The specication of the accessibility relation between situations, <,
has to be modied by the axiom
According to this characterization, s 1 < s 2 is true if all the actions
that lead from s 1 to s 2 are possible in the intermediate situations where
they are performed, and their times are in the right order.
We also have to modify the unique names axioms as follows:
In the temporal extension of the situation calculus we will nd temporal
atomic formulas of the form t 1  t 2 , where t 1 and t 2 are temporal terms
and  2 f=; 6=; <; >; ; g. We also have more complex temporal
formulas of the form 3c , where c is a nonnegative integer, stating
that formula is true in some previous time, and the previous and
present times are subject to the constraint  c. For example, if the
time unit is a day, then 3 =5 :Emp(sue) states that ve days ago sue
was not an employee of the company. More precisely, we dene:
For example, since holds(Emp(sue); we have
For a temporal formula '(x) of the form 3c (x), where is a non-temporal
formula, the formula H('(x); S) (see section 3.2) is 9t(R ' (x; t
new table. We use the temporal parameter t
Hypothetical Temporal Reasoning 21
in R ' to store the amount of time that has elapsed since (x) was true.
Thus, if (x) is true at s, then at state do(a; s), in t we store time(a)
start(s). Moreover, if R ' is true, and therefore (x) was true
units of time ago at some state previous to s, at state do(a; s), in t
we store In consequence, R ' t; s) has the
following successor state axiom:
At the initial state we dene R ' by 8(x; t):R ' (x; t; S 0 ).
With this extension to explicit time, now it is possible to express a
metric temporal precondition for the action re saying that it is possible
to re an employee if he/she has been working at least 30 days in the
company:
As before, this precondition can be changed by a new one referring to
the execution state only: if '(x) is 3<30:Emp(x), then
where the new table R ' is dened by
6.2. Open queries
In this paper, we have just considered queries that are sentences, that
is We think this kind of queries is more likely
to occur in hypothetical reasoning, in the sense that they deal with
global properties of an hypothetical state of the world. Nevertheless,
our methodology can be easily applied to open queries that should
return database tuples as answers. Those tuples can be retrieved from
the domain elements appearing in the transaction log and from the
initial database. This can be done, again, by means of the regression
operator that is able to handle free variables. The formulas resulting
Notice that, for a xed value of  x, R' (x; t; do(a; s)) could be true for many
values of t, if (x) was true many times in the past.
22 Arenas, Bertossi
in the process can be easily simplied taking advantage of the unique
names axioms before the nal evaluation process (cf. (Bertossi et al.,
1998) and appendix A).
6.3. Regular expression queries
In this paper we have considered a wide, but restricted class of historical
queries, namely those that can be constructed on the basis of the usual
rst order past temporal logic operators. In (Abiteboul et al., 1996),
predicate calculus and extended temporal logic (ETL) were compared
in terms of expressive power for temporal databases. ETL is a proper
extension of rst order past temporal logic by means of formulas that
are constructed on the basis of regular expressions. History encoding
and our methodology can be extended to include regular expression
queries on nite transaction logs.
7. Discussion and Conclusions
Among the contributions in this paper we nd the following: (1) An
embedding and representation of the operators of rst order past temporal
logic in the situation calculus. (2) An extension of methodology
presented in (Chomicki, 1995) to check dynamic integrity constraints
to the case in which there is a specication of the evolution of the
database. (3) A methodology for doing hypothetical reasoning along a
virtual evolution of the database obtained by the execution of domain
specic primitive transactions, whereas (Chomicki, 1995) concentrates
on xed integrity constraints and physical and usual updates of the
database. (4) A general solution to the problem of answering temporal
queries in the context of Reiter's specications of database updates, and
this solution works both in a progressive as in a regressive way. (5) A
general transformation mechanism of dynamic integrity constraints into
static integrity constraints, in a context like Reiter's, where both kind of
constraints are expected to be logical consequences of the specication.
general mechanism for transforming history dependent preconditions
for action executions into preconditions to be evaluated at the
execution state. (7) An implementation of all these methodologies. (8)
An extension of all the previous results and techniques to the case of
explicit time or metric temporal logic.
Preliminary versions of this work can be found in (Arenas et al.,
1998a; Arenas et al., 1998b). In the rst case, no temporal operators
were considered, and temporal queries were much more complex than
here. In the second case, explicit use of rst order past temporal logic
Hypothetical Temporal Reasoning 23
and translations between it and the SC was made. The current version
combines the best of the two approaches.
We think that the methodologies developed here for relational data-bases
could be applied in other scenarios as well, e.g. (1) hypothetical
reasoning in work
ows (Bonner, 1999; Davulcu, 1998; Trajcevski et al.,
2000), (2) reasoning from and about policies (Chomicki et al., 2000),
and (3) temporal reasoning in AI in general (Chittaro et al., 2000).
7.1. Complexity issues
As already described, in (Chomicki, 1995) a procedure for checking
temporal integrity constraints is presented. It is based on the idea of
history encoding, that we have captured and used in the situation
calculus framework. The history encoding methodology presented in
(Chomicki, 1995) turns out to be polynomially bounded in the sense
that the given an integrity constraint to be checked, the number of
auxiliary relations to be introduced does not depend on the length n
of the transaction log and the amount of historical information stored
in the union of the auxiliary relations does not depend on n, but is
bounded by a polynomial evaluated on the amount of data in initial
database plus the domain values appearing in the transaction log (the
history) and the constraint.
In our SC context, we may have domain dened primitive actions,
possibly appearing in transaction logs, that could have the instantaneous
eect of inserting a huge amount of data in several database
relations at the same time. If we restrict ourselves to most common
situation in which those primitive actions are of the form, that inserts
a tuple
x into table P and deletes a tuple  x from table P , respectively,
then we still have polynomially bounded history encoding in the sense
that the number of auxiliary relations depends on the temporal query
and not on the length n of the transaction log A
(producing states S the amount of data stored in the
union of them is bounded by a polynomial on the number of domain
values appearing in the initial relational database  0 plus A
and '. 11
This situation and analysis is relevant for eciently answering historical
queries by means of a physical progression of the database, in
particular, through materialization of the auxiliary views (see section
3.2). Nevertheless, if we want to answers the query by appealing to a
Our methodology allows us to have as 0 something more general than a relational
database, e.g. a initial database containing more complex rst order formulas.
Nevertheless, as shown in (Lin et al., 1997) progressing the database in this case, in
particular, the historical auxiliary views, might become a very complex process.
solution of the temporal projection problem via query regression (see
section 3.2), and thus avoiding the materialization of the historical
views, we have to analyze things in a dierent way.
In the regression based approach, the number of auxiliary historical
relations does not depend on the length of the transaction log, but
on the original query only. The amount of data potentially stored in
those relations is no longer relevant since they are not materialized.
The problem is that in a general situation, the regression of a given
formula may become exponentially long wrt the original query (Reiter,
2001), and thus leading to exponential time to evaluate the regressed
query. Nevertheless, there are situations in which this evaluation can
be done in polynomial time. This is the case of context-free successor
state axioms (Reiter, 2001). Those are axioms in which there are no
conditions on the database at the execution state for the actions to have
their desired eects (there might be preconditions for their executions,
but they do not appear explicitly in the SSAs). This is a common
situation in databases, in particular, when only actions of the form
insert P (x) and delete P (x) are considered.
Our running example (example 1) contains context-free SSAs only.
For example, the SSA for Emp is
Here, action a = hire(x) will have the eect of having x inserted into
Emp at the succesor state, without any condition. Nevertheles, this
action does have a precondition to be executed, namely:
Notice that the query to be regressed will contain some auxiliary
relations, which have derived SSAs that will be used by the regression
operator. It is an interesting subject for further investigation to nd
conditions under which the derived SSAs will be context-free when
the SSAs for the original database are context-free. For this purpose,
some syntactic techniques introduced in (Arenas et al., 1998c) could be
useful. In general, the complexity of regression based query answering
in knowledge representation and databases requires further research.
7.2. Related work
There has been some work done on hypothetical reasoning in databases.
In (Bonner, 1990), a datalog language, Hypothetical Datalog, that
allows both database specication and hypothetical reasoning, is pre-
sented. There, special rules for hypothetical reasoning are included in
Hypothetical Temporal Reasoning 25
the datalog specication. These rules contain predicates with a sort of
annotations indicating that the predicate will be true if certain tuple is
deleted or inserted into the database. Then, the kind of reasoning they
allow is of the form \Would that predicate be true if these properties are
added/included?". The nal virtual state is evaluated. It is also possible
to specify a sort of hypothetical predicates, whose truth depends on
the execution of future add/delete transactions. Hypothetical Datalog
also benets from the possibility of specifying recursive predicates. The
queries than can be posed at the hypothetical state are limited by
the datalog formalism. In (Bonner, 1990) other related formalisms for
hypothetical reasoning in databases are discussed.
In (Chen, 1997) a language that can be considered as an extension
of Hypothetical Datalog is presented. More complex database updates
are integrated into the language, more precisely, as predicates in the
rules. In addition, hypothetical reasoning with respect to a particular
predicate, L, can be done by evaluating an auxiliary predicate, 3L.
This predicate is evaluated as L, except for the fact that the updates
that appear in the rules that have to do with L are not committed.
After evaluation, the database goes back to the current physical state.
The more interesting and more powerful logic programming formalism
than the two above for specifying and executing updates is
Transaction Logic Programming (Bonner et al., 1998). It also allows doing
hypothetical reasoning. As was discussed in (Bertossi et al., 1998),
Transaction Logic and the Situation Calculus can complement each
other well. In the situation calculus it is possible to specify primitive
transactions, in particular, giving an account of the frame problem for
this kind of transactions; and transaction logic can be used to specify
more complex transactions.
In our case, instead, we restrict ourselves to relational databases (as
opposed to deductive databases), but we have arbitrary domain specic
transactions which are specied in the SC formalism. The hypothetical
situation is created by virtually executing explicit transactions of this
kind. Actually, Reiter's formalism is a language for reasoning about
action executions (but not for executing actions); this makes it perfect
for hypothetical reasoning.
We are in position to query the whole database evolution, with
involved relationships between the generated states; for this we take
advantage of the existence of explicit states in our formalism and quan-
tications over them. Our query language, both for trajectories and
particular states is much more expressive. We do not need extra rules
or auxiliary predicates for doing hypothetical reasoning; we just use
the specication of our database, in particular, we will not get to the
26 Arenas, Bertossi
situation of having to introduce new rules and predicates in the program
which we might have initially forgotten.
With the formalism we have, as it is, we do not have the possibility
of introducing recursive predicates. Nevertheless, recursion could
be introduced as macros as done in Golog (Levesque et al., 1997),
a situation calculus based logic programming language for high level
robot programming. Introducing predicates whose truth depends on
future states does not seem to be a problem in our formalism, because
quantications on states and the do operator should allow doing this.
The problem of answering hypothetical historical queries in the context
of the situation calculus specications of database updates was
posed in (Reiter, 1995), where also some particular cases were treated.
Further work on this problem is presented in (Reiter, 2001), but essentially
the case of context-free successor state axioms is considered. Our
methodology, being much more general, provides the same formulas to
be evaluated against the initial database in those cases, but can be
applied to a wider range of queries.

Acknowledgements

This research has been partially supported by FONDECYT Grants
1980945, #1990089, #1000593). Part of this work has been done
during the second author's sabbatical at the TU Berlin. He is grateful
to Ralf Kutsche and the CIS group for their support and hospitality;
and to the GK \Distributed Information Systems", the DAAD and the
DIPUC for their nancial support.



--R

Temporal versus First-Order Logic to Query Temporal Databases
Hypothetical Temporal Reasoning with History Encod- ing
Hypothetical Temporal Queries in Databases.

Representation of Temporal Knowledge in the Situation Calculus.
http://dcc.

Automating Proofs of Integrity Constraints in the Situation Calculus.
SCDBR: An Automated Reasoner for Spec- i cations of Database Updates
Hypothetical Datalog: Complexity and Expressivity.
Transaction Logic Programming.
Work ow
An Overview of Datawarehousing and OLAP Technology.
Temporal Representation and Reasoning in Arti
Programming with Logical Queries

A Logic Programming Approach to Con ict Resolution in Policy Management.
Logic Based Modeling and Analysis of Work ows.
Temporal Logic: Mathematical Foundations and Computational Aspects.
Reasoning
GOLOG: A Logic Programming Language for Dynamic Domains.
How to Progress a Database.
Some Philosophical Problems from the Standpoint of Arti
Temporal Reasoning in the Situational Calculus.
Towards a Logical Reconstruction of Relational Database Theory.
Mylopoulos and J.
The Frame Problem in the Situation Calculus: a Simple Solution (Sometimes) and a Completeness Result for Goal Regression.
On Specifying Database Updates.
Natural Actions
In Principles of Knowledge Representation and Reasoning:
Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems.
Answering Historical Queries in Databases (extended ab- stract)
Temporal Databases.

--TR
Temporal databases
Hypothetical datalog
The frame problem in situation the calculus
Temporal logic (vol. 1)
Efficient checking of temporal integrity constraints using bounded history encoding
Temporal versus first-order logic to query temporal databases
An overview of data warehousing and OLAP technology
How to progress a database
Logic based modeling and analysis of workflows
Workflow, transactions and datalog
Temporal representation and reasoning in artificial intelligence
Programming with Logical Queries, Bulk Updates, and Hypothetical Reasoning
Automating Proofs of Integrity Constraints in Situation Calculus
Formalizing (and Reasoning About) the Specifications of Workflows
The Dynamics of Database Views
Temporal reasoning in the situation calculus
dynamic integrity constraints;hypothetical reasoning;database dynamics;historical queries