Printer Friendly

An Access Control Model Supporting Periodicity Constraints and Temporal Reasoning.

Access control models, such as the ones supported by commercial DBMSs, are not yet able to fully meet many application needs. An important requirement derives from the temporal dimension that permissions have in many real-world situations. Permissions are often limited in time or may hold only for specific periods of time. In this article, we present an access control model in which periodic temporal intervals are associated with authorizations. An authorization is automatically granted in the specified intervals and revoked when such intervals expire. Deductive temporal rules with periodicity and order constraints are provided to derive new authorizations based on the presence or absence of other authorizations in specific periods of time. We provide a solution to the problem of ensuring the uniqueness of the global set of valid authorizations derivable at each instant, and we propose an algorithm to compute this set. Moreover, we address issues related to the efficiency of access control by adopting a materialization approach. The resulting model provides a high degree of flexibility and supports the specification of several protection requirements that cannot be expressed in traditional access control models.

Categories and Subject Descriptors: H.2.7 [Information Systems]: Database Administration--security, integrity, and protection

General Terms: Security

Additional Key Words and Phrases: Access control, periodic authorization, temporal constraints, time management

1. INTRODUCTION

Data protection from unauthorized accesses is becoming more and more crucial as an increasing number of organizations entrust their data to database systems. Moreover, as organizations and users are becoming more aware of data security issues, more articulate access control policies are being devised. An access control policy establishes for each user (or group of users, or functional role within the organization) the actions the user can perform on each object (or set of objects) within the system and under which circumstances. An example of a policy is that "all programmers can modify the project files every working day except Friday afternoons." Once the organization security policies are devised, they are implemented in terms of the access control model of the DBMS at hand.

The implementation of the security policy in terms of access control models, provided as part of a typical current DBMS, is however quite a difficult task. Current commercial DBMSs are still rather poor with respect to expressiveness of security requirements and therefore unable to directly support many relevant application policies [Jajodia et al. 1997]. Even the preceding simple requirement cannot be directly supported by any current commercial DBMS. As a matter of fact, in most cases the access control policies must be implemented as code in application programs. Such an approach makes it very difficult to verify and modify the access control policies and to provide any assurance that these policies are actually enforced.

An important requirement, common to many application security policies, is related to the temporal dimension of access permissions. In many real-world situations, permissions may hold only for specific time intervals. A further requirement concerns periodic authorizations. In many organizations, authorizations given to users must be tailored to the pattern of their activities within the organization. Therefore, users must be given access authorizations to data only for the time periods in which they are expected to need the data. The preceding requirement concerning programmers and project files is an example of specification requiring an authorization mechanism able to support periodic authorizations. As another example, consider part-time staff that should be authorized for accesses only on working days between 9 AM and 1 PM.

Periodic authorizations are also crucial for optimizing resource usage. In particular, authorizations for application programs, whose execution is very resource-expensive, could be assigned only for specific time periods in which other programs are not likely to be executed. Periodic authorizations are, however, even more difficult to handle than simple, nonperiodic, temporal authorizations. Therefore the solution of implementing periodic authorizations as part of application programs is not viable.

The development of a temporal authorization model entails several issues, including the definition of a formal semantics for the authorization model, the development of strategies for efficient access control, and the development of tools for authorization administration. In this article we address some of these issues by proposing an access control model characterized by temporal authorizations. In the proposed model, a temporal expression is associated with each authorization, identifying the instants in which the authorization applies. The temporal expression is formed by a periodic expression (e.g., 9am to 1pm on Working-days, identifying the periods from 9 AM to 1 PM in all days excluding weekends and vacations), and a temporal interval bounding the scope of the periodic expression (e.g., [2/1997, 8/1997], restricting the preceding periods to those between February and August, 1997).

Another relevant feature provided by our model is the possibility of specifying derivation rules expressing temporal dependencies among authorizations. These rules allow the derivation of new authorizations based on the presence or absence of other authorizations in specific periods of time. By using derivation rules, many protection requirements can be concisely and clearly specified. For example, it is possible to specify that two users, working on the same project, must receive the same authorizations on certain types of objects; or that a user should receive the authorization to access an object in certain periods, only if nobody else was ever authorized to access the same object in any instant within those periods. Derivation rules are specified by constraining the rule application with a temporal expression, by providing the authorization to be derived, by specifying one of the three temporal dependency operators that the model provides, and, finally, by giving the body of the rule in the form of a Boolean expression of authorizations. The three temporal operators correspond to the three main temporal relations among authorizations that we have identified in common protection requirements.

In addition to these temporal capabilities, the model supports both positive and negative authorizations. The capability of supporting explicit denials, provided by negative authorizations, can be used for specifying exceptions to positive authorizations and for supporting a stricter control in the case of decentralized authorization administration [Bertino et al. 1993]. The combination of positive/negative authorizations with temporal authorizations results in a powerful yet flexible authorization model.

A formal semantics has been defined for temporal authorizations and derivation rules, based on the semantics of Datalog programs with negation and periodicity and order constraints. A critical issue is represented by the presence of negation in our derivation rules. Negation, by allowing the derivation of new authorizations based on the absence of other authorizations, augments the expressive power of the model. However, it does not always ensure the derivation of a unique set of authorizations, since the set of authorizations derivable from a given set of authorizations and rules may depend on the evaluation order. To avoid this problem, we impose a syntactical restriction on the set of derivation rules and we show how this condition guarantees the uniqueness of the set of derived authorizations.

Finally, we address the problem of efficient access control by proposing a strategy based on view materialization approaches. Our approach, which is based on a combination of the Dred [Gupta et al. 1993] and Stdel [Lu et al. 1995] approaches, avoids the high costs arising from the evaluation of the deductive rules when performing access control.

Previous Related Work

We first presented a proposal for an authorization model supporting authorizations with temporal intervals and a restricted set of derivation rules in Bertino et al. [1996a]. The current article extends our previous work introducing, among other features, support for periodic access authorizations and rules. This is a major extension, both for the practical relevance of periodic expressions in specifying authorizations and for the related theoretical and performance issues. The language for expressing derivation rules also has two major extensions with respect to the one supported by our previous model: the introduction of a new temporal operator (UPON) and the possibility of using an arbitrary Boolean expression of authorizations as the right-hand side of a rule. These extensions significantly augment the expressiveness of the model in terms of protection requirements that can be supported. A preliminary approach towards the introduction of periodic constraints has been presented in Bertino et al. [1996b]. However, Boolean operators were not considered, nor access control strategies devised. All the relevant theoretical foundations are reported only in this article. To the best of our knowledge, the authorization model we are presenting is the first one proposing features such as periodic authorizations and derivation rules.

In the context of database systems, Ingres [Date 1995] supports some temporal features. In Ingres, when granting an authorization, a user can specify that the authorization is valid only in specific hours and days of the week. For instance, it is possible to give a user the authorization to read a table only between 8:00 AM and 5:00 PM between Tuesday and Thursday. Temporal specifications in Ingres are conditions that can be evaluated, upon access control, by checking the time/day of the request against that of the system's clock. Although representing a first step towards the inclusion of temporal features in authorization specification, Ingres provides only a rudimentary treatment of time-based authorizations. For instance, no start or expiration date can be associated with authorizations and no calendar management, time reasoning, or authorization derivation features are supported.

Other relevant related work can be found in the framework of authentication systems. Kerberos [Steiner et al. 1988], based on a client-server architecture, provides the notion of "ticket," with an associated validity time. The span of the validity time is chosen by the administrator based on a tradeoff between security and convenience (a typical choice is a span of 8-24 hours for all tickets). The ticket is used by a client to require a service from a particular server. Associating a validity time with the ticket saves the client from the need to acquire a ticket for each interaction with the same server. The scope of the temporal ticket mechanism is very different from our access control model. In Kerberos the ticket is only used to denote that a client has been authenticated by the authentication server. It cannot be used to grant access to specific documents or resources managed by the server.

From the side of logical formalisms for security specifications, Woo and Lam [1993] propose a very general formalism for expressing authorization rules. Their language does not have explicit constraints to deal with temporal information. However, the generality of their language, which has almost the same expressive power of first-order logic, makes it possible to model temporal constraints. The main drawback is that the tradeoff between expressiveness and efficiency seems to be strongly unbalanced in their approach. Finally, Abadi et al. [1993] proposed a formal language based on modal logic. However, their language, which is mainly devoted to the modeling of concepts such as roles and delegation of authorities, is not able to support temporal constraints.

Organization of the Article

The remainder of this article is organized as follows. Section 2 describes the formalisms we use to represent periodic time. Section 3 introduces periodic authorizations and derivation rules and gives the formal semantics of our model. Section 4 deals with the problems due to the presence of negation. A sufficient condition to guarantee the uniqueness of the set of derived authorizations and an algorithm for checking this condition are given. In Section 5 an algorithm for deriving the set of implicit and explicit authorizations is presented. Administrative operations are discussed in Section 6. In this section we also discuss implementation issues. Section 7 concludes the article and outlines future work. Appendix A illustrates the Datalog extension we use to represent the semantics of our rules. Finally, formal proofs are reported in Appendix B.

2. PRELIMINARIES

To represent periodic authorizations we need a formalism to denote periodic time. Our choice is to provide a symbolic (user-friendly) formalism for the user that has to specify authorizations, and an equivalent "mathematical" formalism for internal representation. The symbolic formalism consists of a pair <[begin, end], P> where p is a periodic expression denoting an infinite set of time intervals, and [begin, end] denotes the lower and upper bounds that are imposed on time intervals in P. The formalism for internal representation is based on sets of periodicity and gap-order constraints over integer numbers and is inspired by the work in Toman et al. [1994]. A mapping from symbolic periodic expressions into these types of constraints is needed to describe the semantics of periodic authorizations and rules, to prove formal properties of our model, and to perform deductive reasoning.

In the following we take as our model of time the integers Z with the total order relation <.

2.1 Symbolic Expressions

The formalism for symbolic periodic expressions is essentially the one proposed in Niezette and Stevenne [1992], based on the notion of calendars. A calendar is defined as a countable set of consecutive intervals. Each interval of a calendar is numbered by an integer number, called the index of the interval, in such a way that successive intervals are numbered by successive integers.

Example 1. Days, Months, Years are examples of calendars representing, respectively, the set of all the days, the months, and the years.

New calendars can be dynamically constructed from the existing ones. The starting point in the definition of new calendars is the definition of a basic calendar (the tick of the system), from which other calendars can be dynamically defined. In the following, we assume that Hours is the basic calendar with the tick indexed by 1 as the first hour of 1/1/94. A new calendar [C.sub.1] can be defined from an existing calendar [C.sub.0] by means of function "generate()". [C.sub.1] = generate(sp; [C.sub.0]; ([x.sub.1], ..., [x.sub.n])) creates a calendar [C.sub.1] whose first tick is the union of the first [x.sub.1] ticks of calendar [C.sub.0], the second tick is the union of the following [x.sub.2] ticks of [C.sub.0], and so on, cycling through the given values. Parameter sp is the synchronization point; that is, it is the index of the interval of [C.sub.0] that starts at the same time as the first interval of [C.sub.1].

Example 2. Starting from the basic calendar Hours, the following calendars can be defined.

--Days = generate(1; Hours; (24));

--Months = generate(1; Days; (31, 28, ..., 31, 28, ..., 31, 29, ..., 31, 28, ..., 31));

--Weeks = generate(2; Days; (7));

--Years = generate(1; Days; (365, 365, 366, 365)).(1)

Note that, in the definition of Weeks, 2 is used as the synchronization point since the first full week of 1994 starts on Sunday, January 2nd. The definition of Years says to take the first 365 days as the first tick of the calendar, the following 365 days as the second tick, and so on, cycling through the given values.

In our model, we postulate the existence of a set of predefined calendars containing at least the calendars Hours, Days, Weeks, Months, and Years. Given two calendars [C.sub.1] and [C.sub.2], [C.sub.1] is called a subcalendar of [C.sub.2], (written [C.sub.1] ?? [C.sub.2]), if each interval of [C.sub.2] is exactly covered by a finite number of intervals of [C.sub.1]. It is easy to show that the subcalendar relation defines a partial order on calendars, and that, since we take Hours as our basic calendar, Hours ?? C for each calendar C defined in our system.

Calendars can be combined to represent more general sets of periodic intervals, not necessarily contiguous, such as the set of Mondays or the set of the third hour of the first day of each month. Complex sets of periodic intervals, like the preceding ones, are represented by means of periodic expressions, formally defined as follows.

Definition 1. Given calendars [C.sub.d], [C.sub.1], ..., [C.sub.n], a periodic expression is defined as [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], where [O.sub.1] = all, [O.sub.1] [element of] [2.sup.N] [union] {all} and [C.sub.i] ?? [C.sub.i-1] for i = 2, ..., n, [C.sub.d] ?? [C.sub.n], and r [element of] ??.

The symbol ?? separates the first part of the expression, identifying the set of starting points of the intervals it represents, from the specification of the duration of each interval in terms of calendar [C.sub.d]. For example, all.Years + {3, 7}.Months ?? 2.Months represents the set of intervals starting at the same instant as the third and seventh month of every year, and having a duration of two months. [O.sub.i] is omitted when its value is all, whereas it is represented by its unique element when it is a singleton, r.[C.sub.d] is omitted when it is equal to 1.[C.sub.n]. Table I reports a set of periodic expressions with their intuitive meaning.
Table I. Example of Periodic Expressions

periodic expression         meaning

Weeks + {2,6}.Days          Mondays and Fridays
Months + 20.Days            The twentieth of every month (Pay-days)
Years + 7.Months ??         Summer-time
 3.Months
Weeks + {2, ..., 6}.Days    Working-days
Weeks + {2, ..., 6}.Days    Between 9am and 1pm of working-days
 + 10 .Hours ?? 4.Hours


Periodic expressions are a symbolic representation of infinite sets of periodic intervals. The set of time intervals corresponding to periodic expressions is formalized by function [Pi](), defined as follows.

Definition 2. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be a periodic expression, then [Pi](P) is a set of time intervals whose common duration is r [multiplied by] [C.sub.d], and whose set S of starting points is computed as follows.

--If n = 1, S contains all the starting points of the intervals of calendar [C.sub.1].

--If n [is greater than] 1, and [O.sub.n] = {[n.sub.1], ..., [n.sub.k]}, then S contains the starting points of the [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], intervals (all intervals if [O.sub.n] = all) of calendar [C.sub.n] included in each interval of ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]).

For example, if P is the last expression in Table I, then [Pi](P) is the set of time intervals, with a duration of four hours, starting with the tenth hour (9 AM to 10 AM) of the second, third, fourth, fifth, and sixth day of every week.

A symbolic formalism is also needed to express the bounds begin and end that limit the application of the periodic expression. This formalism must guarantee that each expression identifies a single instant in the basic calendar, or, possibly, the special values +/-[infinity]. Although the results of this article do not rely on a particular choice for this formalism, for simplicity we choose a simple date notation.

Definition 3. A date expression has the form mm/dd/yy:hh, where [element of] {1, ..., 12}, dd [element of] {1, ..., 31}, yy [element of] {00, ..., 99}, and hh [element of] {01, ..., 24}.

A date expression denotes a single tick of calendar Hours, according to the intuitive semantics.(2)

We require begin to be a date expression, and end to be [infinity] or a date expression. We sometimes abbreviate date expressions according to the intuitive semantics; for example, when 1/1/94 is used as begin, it denotes the first instant of the first day of January 1994, whereas, as end, it denotes the last instant of 1/1/94.

2.2 Periodicity and Gap-Order Constraints

Symbolic expressions, although convenient for the users, are not easy to manipulate in the deductive process. For this reason, we translate expressions given by the user into expressions in a different formalism. This formalism is based on sets of constraints. Intervals [begin, end], consisting of date expressions, are straightforwardly translated into so-called gap-order constraints [Revesz 1995].

Definition 4. Let u, l be integers, c be a nonnegative integer, and t, t' be integer variables. A gap-order constraint is a formula of the form l [is less than] t, t [is less than] u, t = t', or t + c [is less than] t'.

If begin and end denote instant [t.sub.b] and [t.sub.e], respectively, the corresponding constraints are [c.sub.1] [is less than] t and t [is less than] [c.sub.2], where the constants [c.sub.1] and [c.sub.2] are, respectively, [t.sub.b] - 1 and [t.sub.e] + 1. For brevity, we often write [t.sub.b] [is less than or equal to] t [is less than or equal to] [t.sub.e] for the conjunction of the constraints.(3) Gap-order constraints involving two variables are also used in the reasoning process.

To manipulate periodic expressions we use periodicity constraints over integer numbers, as introduced in Toman et al. [1994]. Periodicity constraints denote infinite periodic sets of integers.

Definition 5. Let K be a finite set of natural numbers, t an integer variable, k an element of K, and c [element of] {0, ..., k - 1}. A simple periodicity constraint is a formula of the form: t [[equivalent].sub.k] c.

Periodicity constraint t [[equivalent].sub.k] c denotes the set of integers of the form c + nk, with n ranging from - [infinity] to + [infinity] in Z. In the following, we use the notation t [[equivalent].sub.k] (y + c)[inverted]Ay = 0, ..., u as a compact representation for the disjunction of simple constraints: t [[equivalent].sub.k] c [disjunction] t [[equivalent].sub.k] c + 1 [disjunction] ... [disjunction] t [[equivalent].sub.k] c + u.

In our model, each access authorization is associated with a periodic expression, and a pair of date expressions defining the lower and upper bounds of its applicability. As shown in the next section, a periodic expression corresponds to a disjunction of simple periodicity constraints, and the lower and upper bounds can be represented by a conjunction of gap-order constraints. Hence, it would be natural to associate with each authorization a complex constraint comprising these two components. However, since the reasoning process requires the manipulation of these constraints by the operations of complement, conjunction, and projection, we need an adequate normal form. For this purpose, we introduce a temporal constraint [Xi] that is represented by the set {([PC.sub.1], [GC.sub.1]), ..., ([PC.sub.m], [GC.sub.m])}, where each [PC.sub.i] is a conjunction of simple periodicity constraints and each [GC.sub.i] is a conjunction of gap-order constraints. [Xi] is associated with a propositional logic formula in disjunctive normal form F([Xi]) = ([PC.sub.1] [conjunction] [GC.sub.1]) [disjunction] ... [disjunction] ([PC.sub.m] [disjunction] [GC.sub.m]), corresponding to the intuitive semantics of [Xi]. [Xi] denotes all the instants t such that there exists i [element of] [1, m] with t satisfying both [PC.sub.i] and [GC.sub.i].

Some basic operations have been defined for simple periodicity constraints in Toman et al. [1994] and for gap-order constraints in Revesz [1993], using a graph for the representation of PCs and GCs. For example, rules are given to compute the constraint equivalent to the conjunction of two constraints on the same variables.

We now define conjunction ([conjunction]*) and complement (??*) on temporal constraints.

Definition 6. Given two temporal constraints [[Xi].sub.1] and [[Xi].sub.2], [Xi] = [[Xi].sub.1] [conjunction]* [[Xi].sub.2] is the set of pairs (PC, GC) whose associated formula F([Xi]) is the disjunctive normal form of F([[Xi].sub.1]) [conjunction] F([[Xi].sub.2]).

Definition 7. Let [Xi]' be a set of pairs (PC, GC). [Xi] = ??*[Xi]' is the set of pairs (PC, GC) whose associated formula F([Xi]) is the disjunctive normal form of ?? F([Xi]).

Any propositional logic formula on PCs and GCs in disjunctive normal form, resulting from the preceding operations, can be represented as a temporal constraint [Xi]. Indeed, each pair in [Xi] corresponds to a disjunct in the formula. If no PC or no GC appears in a disjunct, the always satisfied constraint {true} is used in its place.

Example 3. {[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]},

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Note that conjunction among PCs and among GCs is defined in Toman et al. [1994] and Revesz [1993], and that negation can be easily eliminated. For example, if PC = (t [[equivalent].sub.k] c [conjunction] t' [[equivalent].sub.k'] c'), ??PC is the disjunction of the constraints (PCs) t [[equivalent].sub.k] r with r = 0, ..., c - 1, c + 1, ..., k - 1, and t' [[equivalent].sub.k'] s with s = 0, ..., c' - c' + 1, ..., k' - 1.

Example 4. Consider the periodicity constraints [PC.sub.1] = (t [[equivalent].sub.7] 1 [conjunction] t' [[equivalent].sub.10] 1) and [PC.sub.2] = (t [[equivalent].sub.14] 1). [PC.sub.1] [conjunction] [PC.sub.2] = (t [[equivalent].sub.1] 41 [conjunction] t' [[equivalent].sub.10] 1) whereas ??[PC.sub.1] is the disjunction of the PCs: t [[equivalent].sub.7] 0, t [[equivalent].sub.7] 2, ..., t [[equivalent].sub.7] 6, t' [[equivalent].sub.10] 0, t' [[equivalent].sub.10] 2, ..., t' [[equivalent].sub.10] 9.

2.3 From Symbolic Expressions to Constraints

The following proposition states the correspondence between periodic expressions and sets of periodicity constraints.

PROPOSITION 1. Any symbolic periodic expression can be translated into an equivalent set of simple periodicity constraints.

In Niezette and Stevenne [1992], it is shown how any calendar can be translated into a union of linear repeating intervals. It is easily seen that the translation can be extended to periodic expressions.(4) A linear repeating interval is a mathematical expression of the form kn + (b, e) denoting the set of intervals including the interval (b, e) and all intervals obtained by shifting (b, e) by multiples of k. Any instant t in the intervals defined by kn + (b, e) satisfies one of the constraints t [[equivalent].sub.k] (b + y) [inverted]Ay = 0, ..., e - b and vice versa. Hence, for each periodic expression P, there exists a disjunction of simple periodicity constraints such that the set of its solutions is the set of instants contained in the intervals of [Pi](P).

When the intervals in [Pi](P) have the same length, the simple periodicity constraints corresponding to P can be represented in a compact way:

t [[equivalent].sub.Periodicity(P)] (y + z - 2) [inverted]Ay = 1, ..., Granularity(P), and [inverted]Az [element of] Displacement(P).

The values for the parameters in this formula depend on the calendar used to express the constraints, and on the definition of the calendars appearing in P. For example, if we express the constraints in terms of Hours, then the expression Weeks + {3}. Days, denoting Tuesdays, is translated into t [[equivalent].sub.168] (y + 73 - 2) [inverted]Ay = 1, ..., 24, where 168 is the number of hours in a week (the periodicity of Tuesdays), {73} is the only hour corresponding to the beginning of a Tuesday in each period,(5) and 24 is the number of hours within each Tuesday (the granularity of Tuesdays).

In general, given a symbolic expression P and the basic calendar, the values for Periodicity(P), Displacement(P), and Granularity(P) can be derived as follows.

--Periodicity(P) is the number n of units of the basic calendar that identifies the periodicity with which the time intervals in [Pi](P) repeat themselves. For example, with reference to Table I and assuming Hours as the basic calendar, the periodicity of the first, fourth, and fifth expressions is 168 (a week expressed in hours), whereas the periodicity of the second is 3,506,328 (400 years in terms of hours) that is the period considering leap years.

--Displacement(P) is a set of numbers, each one representing the position within a period where a segment of the span of time defined by p begins. We assume that the first period always starts from tick I of the basic calendar. For example, in Table I, the displacement of the first expression is {2 * 24 + 1, 6 * 24 + 1}, and the displacement of the second is {19 * 24 + 1, 50 * 24 + 1, 78 * 24 + 1,...} (each position of the beginning of the 20th day of each month within the period must be specified).

--Granularity(P) is the length of each segment of time within the period defined by p. The granularity is expressed using the basic calendar, and it can be easily derived from the part of p following the ?? symbol (note that this part can be implicit). For example, in Table I, the granularity of the first, second, and fourth expression is 24 (1 day in hours), and the granularity of the fifth is 4 (4 hours).

When the intervals in [Pi](P) have different length, there is no unique value for Granularity(P). In this case a simple solution is to partition [Pi](P) in sets of equal-length intervals, and representing each of them as shown previously.

3. THE AUTHORIZATION MODEL

In this section we illustrate the basic components of our authorization model. We do not make any assumption on the underlying data model and on the access modes users can exercise on the data objects. This generality makes our authorization model applicable to the protection of information represented with different data models. In the following U denotes the set of users, O the set of objects, and M the set of access modes. We consider as users the identifiers with which users can connect to the system. We suppose identifiers can refer to single users (e.g., Ann or Bob) or to user roles (e.g., staff or manager).

3.1 Periodic Authorizations and Rules

Our model supports the specification of periodic authorizations, that is, authorizations that hold in specific periodic intervals specified by a periodic expression. A time interval is also associated with each authorization, imposing lower and upper bounds on the potentially infinite set of instants denoted by the periodic expression. Periodic authorizations can be positive (representing permissions) or negative (representing explicit denials to exercise privileges on objects).

We start by introducing the definition of authorization.

Definition 8. An authorization is a 5-tuple (s, o, m, pn, g), with s, g [element of] U, o [element of] O, m [element of] M, pn [element of] {+, -}.

For instance, by authorization (Ann, [o.sub.1], read, +, Tom) Tom grants Ann the read access mode on object [o.sub.1]. By contrast, by authorization (John, [o.sub.1], write, -, Tom) Tom prevents John from writing object [o.sub.1].

Periodic authorizations are formally defined as follows.

Definition 9. A periodic authorization is a triple ([begin, end], P, auth), where begin is a date expression, end is either the constant [infinity], or a date expression denoting an instant greater than or equal to the one denoted by begin, P is a periodic expression, and auth is an authorization.

The periodic authorization ([begin, end], P, (s, o, m, pn, g)), states that authorization (s, o, m, pn, g) is granted for each instant in [Pi](P) that is greater than or equal to the instant [t.sub.b] denoted by begin and smaller than or equal to the instant [t.sub.e] denoted by end (if end [is not equal to] [infinity]).

For example, periodic authorization [A.sub.1] = ([1/1/94, [infinity]], Mondays,(6) (Matt, [o.sub.1], read, +, Bob)), specified by Bob, states that Matt has the authorization to read [o.sub.1] each Monday starting from 1/1/94.

A nonperiodic temporal authorization, that is, an authorization that holds continuously for a specific set of time instants, is expressed by a periodic authorization using the basic calendar as the period component. In general, the symbol [perpendicular to] is used to denote this calendar. Note that the corresponding periodicity constraint is t [[equivalent].sub.1] 0, that is equivalent to true, since it is always satisfied.

In what follows, given a periodic authorization A = ([begin, end], P, (s, o, m, pn, g)), we use s(A), o(A), re(A), pn(A), g(A) to denote, respectively, the subject, the object, the privilege, the sign of the authorization (positive or negative), and the grantor in A.

Note that the possibility of expressing negative authorizations introduces potential conflicts. Suppose that authorization [A.sub.2] = ([1/1/95, [infinity]], Working-days, (Matt, [o.sub.1], read, -, Tom)) is specified in addition to authorization [A.sub.1]. We then have for each Monday in the interval [1/1/95, [infinity] both a positive and a negative authorization with the same subject, object, and access mode. We solve this conflict according to the denials-take-precedence principle [Jajodia et al. 1997]. As a consequence, Matt will be allowed to read [o.sub.1] only for the Mondays in [1/1/94, 12/31/94]. We say that a positive authorization A is valid at a given instant t, if (1) a temporal authorization ([begin, end], P, A), with t [element of] [Pi](P) [intersection] {[[t.sub.b], [t.sub.e]]},(7) is specified or it can be derived through the derivation rules, and (2) a negative authorization ([begin', end'], P', A'), with the same subject, object, and access mode as A such that t [element of] [Pi](P') [intersection] {[[t'.sub.b], [t'.sub.e]]} is neither specified nor can be derived through the derivation rules, where begin' and end' denote, respectively, instants [t'.sub.b] and [t'.sub.e]. We say that a negative authorization A is valid at time t if a temporal authorization ([begin, end], P, A)), with t [element of] [Pi](P) [intersection] {[[t.sub.b], [t.sub.e]} is specified or can be derived through the derivation rules. The notion of validity is formalized in Section 3.3.

The second basic component of our model is an inference mechanism based on derivation rules, which express temporal dependencies among authorizations. Derivation rules allow the derivation of new periodic authorizations on the basis of the validity or nonvalidity of other periodic authorizations. Like authorizations, each derivation rule has a bounding time interval and a periodicity, representing the instants at which it can be applied.

Definition 10. A derivation rule is a triple ([begin, end] , P, A <OP> A), where begin is a date expression, end is either the constant [infinity] or a date expression denoting an instant greater than or equal to the one denoted by begin, P is a periodic expression, A is an authorization, A is a Boolean expression of authorizations, and <OP> is one of the operators: WHENEVER, ASLONGAS, UPON.

The notion of validity, previously introduced for authorizations, naturally extends to a Boolean expression of authorizations. Given a Boolean expression of authorizations A and an instant t, we say that A is valid at time t if A evaluates "true" when each authorization in A is substituted by the Boolean value "true" in case the authorization is valid at time t, and by "false" otherwise.

Authorizations derived from derivation rules have as grantor the user who specified the rule.

We now give the intuitive semantics of the different kinds of derivation rules allowed by our model. The formal semantics are given in Section 3.3. In the following we assume all authorizations are granted by the same user and we therefore do not consider the grantor of authorizations in the discussion. Clarifying examples refer to the authorizations and derivation rules illustrated in Figure 1.

Fig. 1. An example of authorizations and derivation rules.
(A1) ([95,5/20/95], [perpendicular to],
   (manager,guidelines,write,+,Sam))

(A2) ([10/1/95,[infinity]], Working-days,
   (technical-staff,guidelines,read,+,Sam))

(A3) ([95,97], Working-days, (staff,document,read,+,Sam))

(A4) ([95,[infinity]],Pay-days, (Tom,pay-checks,write,+,Sam))

(A5) ([96,97], Summer-time, (technical-staff,document,read,+,Sam))

(R1) ([96,98], Working-days, (temporary-staff,document,read,+,Sam)
    ASLONGAS ?? (summer-staff, document,read,+,Sam))

(R2) ([95,[infinity]],Mondays and Fridays,
    (technical-staff,report,write,+,Sam) UPON
    ?? ((manager,guidelines,write,+,Sam)
    [disjunction](staff,guidelines,write,+,Sam)))

(R3) ([95,[infinity]], [perpendicular to],
    (technical-staff,report,write,-,Sam) WHENEVER
    ?? (technical-staff,guidelines,read,+,Sam))

(R4) ([95 ,[infinity]], Summer-time,
    (summer-staff,document,read,+,Sam) WHENEVER
    (staff, document, read, +, Sam) [conjunction] (technical-staff,
    document, read, +, Sam))

(R5) ([95,96] ,Working-days, (Ann,pay-checks ,read,+,Sam) UPON
     (Tom,pay-checks,write,+,Sam))


--([begin, end], P, A WHENEVER A).

We can derive A for each instant in [Pi](P) [intersection] {[[t.sub.b], [t.sub.e]]} for which A is valid. For instance, rule [R.sub.4] states that summer-staff can read document for every instant in Summer-time, from 1/1/1995, in which both staff and technical-staff can read document.

--([begin, end], P, A ASLONGAS A).

Authorization A can be derived for each instant t in [Pi](P) [intersection] {[[t.sub.b], [t.sub.e]]} such that A is valid for each time instant in [Pi](P) that is greater than or equal to [t.sub.b] and smaller than or equal to t. This implies that the ASLONGAS rule can no longer be used to derive authorization A, starting from the first instant t [element of] [Pi](P) [intersection] {[[t.sub.b], [t.sub.e]]} in which A is not valid.

For instance, rule R1 states that temporary-staff can read document each working day in [1/1/96, 12/31/98] until the first working day in which summer-staff will be allowed for that.

--([begin, end], P, A UPON A).

We can derive A for each instant t in [Pi](P) [intersection] {[[t.sub.b], [t.sub.e]]} if there exists an instant t' [element of] [Pi](P) that is greater than or equal to [t.sub.b] or smaller than or equal to t such that A is valid at time t'. For instance, rule [R.sub.5] states that Ann can read pay-checks each working day starting from the first in [1/1/95, 12/31/96] in which Tom can write pay-checks.

A graphical representation of the semantics of the different temporal operators that can appear in a derivation rule is given in Figure 2. Note that, according to the semantics of our temporal operators, the only times of interest in evaluating R are those in [Pi](P) [intersection] {[[t.sub.b], [t.sub.e]]}.

[Figure 2 ILLUSTRATION OMITTED]

Example 5. From the authorizations and rules in Figure 1 we can derive the following authorizations.

--(summer-staff, document, read, +, Sam) for each working day of the summers 1996 and 1997, from rule [R.sub.4] and authorizations [A.sub.3] and [A.sub.5].

--(temporary-staff, document, read, +, Sam) for each working day in [ 1/1/96, 6/30/96 ], from rule [R.sub.1] using rule [R.sub.4] and authorizations [A.sub.3] and [A.sub.5]. The ending time of the derived authorization is determined by the starting time of the authorization derived for summer-staff, from rule [R.sub.4].

--(technical-staff, report, write, +, Sam) for each Monday and Friday from 5/22/95 to [infinity], from rule [R.sub.2], using authorization [A.sub.1]. 5/22/95 is the first Monday in [1/1/95, [infinity]] in which neither manager nor staff can write guidelines.

--(technical-staff, report, write, -, Sam) for each day in [1/1/95, 9/30/95] and for each Saturday and Sunday from 10/1/95 to [infinity], from rule [R.sub.3] using authorization [A.sub.2].

--(Ann, pay-checks, read, +, Sam) for each working day from 1/20/95 to 12/31/96 from rule [R.sub.5] and authorization [A.sub.4]. 1/20/95 is the first payday in [1/1/95, 12/31/95].

A simple extension to the syntax of derivation rules allows the use of the special symbol "*" instead of a user, object, or access mode in the authorizations appearing in rules, with the meaning that any value in the corresponding domain can be used. We refer to rules containing the symbol "*" as parametric derivation rules. The wild card character can be used in the authorization on the left of the operator, that is, in the authorization to be derived, as well as in the authorizations appearing in the formula on the right-hand side of the operator. Each parametric rule is exploded by the system into different rules, one for each value (or combination of values) to which the wild card character can be instantiated. The value substituted for an authorization element (i.e., user, object, or access mode) to the wild card character must be the same for all the authorizations within a rule. Note that the instantiation of occurrences of "*" in the authorization on the left-hand side of the temporal operator is constrained by the authorizations that the grantor of the rule can specify. In particular, since we assume a user can specify only authorizations on the objects he owns, occurrences of the "*" symbol for the object in the authorization A on the left-hand side of the operator will be instantiated to any object owned by g (A).

Example 6. Rule

(R) ([96, 98], Working-days, (part-time-staff, *, read, +, Sam) WHENEVER (staff, *, *, +, Sam) [disjunction] (temporary-staff, *, read, +, Sam))

states that part-time-staff can read, in an instant of a working day in the period 96-98, any object on which either temporary-staff has read privilege or staff has any privilege, for that instant.

Suppose there are three objects on which sam can grant authorizations: document, guidelines, and report; and two access modes: read and write. Rule (R) is expanded into the following rules.

([R.sub.1]) ([96, 98], Working-days, (part-time-staff, document, read, +, Sam)

WHENEVER (staff, document, read, +, Sam) [disjunction] (temporary-staff, document, read, +, Sam))

([R.sub.2]) ([96, 98], Working-days, (part-time-staff, document, read, +, Sam)

WHENEVER (staff, document, write, +, Sam) [disjunction] (temporary-staff, document, read, +, Sam))

([R.sub.3]) ([96, 98], Working-days, (part-time-staff, guidelines, read, +, Sam)

WHENEVER (staff, guidelines, read, +, Sam) [disjunction] (temporary-staff, guidelines, read, +, Sam))

([R.sub.4]) ([96, 98], Working-days, (part-time-staff, guidelines, read, +, Sam)

WHENEVER (staff, guidelines, write, +, Sam) [disjunction] (temporary-staff, guidelines, read, +, Sam))

([R.sub.5]) ([96, 98], Working-days, (part-time-staff, report, read, +, Sam)

WHENEVER (staff, report, read, +, Sam) [disjunction] (temporary-staff, report, read, +, Sam))

([R.sub.6]) ([96, 98], Working-days, (part-time-staff, report, read, +, Sam)

WHENEVER (staff, report, write, +, Sam) [disjunction] (temporary-staff, report, read, +, Sam))

3.2 Expressiveness and Minimality of the Temporal Operators

Temporal operators that can appear in our derivation rules have been chosen to express three intuitive temporal relations among authorizations. The derivation of new authorizations is obtained with WHENEVER by considering authorizations valid in the same time instants, and with ASLONGAS by considering the validity of authorizations in a whole span of time, whereas UPON allows the expression of triggering conditions. The relevance of these relations with respect to others that could be identified in a general temporal context, is motivated by the particular domain of access control.

Consider, for example, the derivation rules reported in Figure 1. In Rule [R.sub.4] the WHENEVER operator is used to give summer-staff the authorization to read a certain document at a certain time if, at the same time, both staff and technical-staff have the authorization to read that document. The set of instants at which this rule can be applied is restricted, by the constraints associated with the rule, to those included in each summer since the one in 1995. The same operator can be used to derive authorizations based on the absence of other authorizations at the same instants. This form of derivation can be useful in practice when two subjects must be authorized for an access over complementary intervals. Another example of the use of WHENEVER is given by rule [R.sub.3]: technical-staff is given a negative authorization to write a report for the instants at which it is not authorized to read the guidelines. The WHENEVER operator is sufficient to model many practical rules of an access control system.

Other protection requirements need the ability of the system to derive an authorization only if a certain combination of authorizations has been continuously valid through a whole span of time. The existence of one instant in this span in which the combination of authorizations is not valid must prevent the derivation of the new authorization. The ASLONGAS operator has been introduced for this purpose. In Figure 1, rule [R.sub.1] derives an authorization for temporary-staff to read a document at a certain time t only if in each working day from 1996 up to t there was no authorization for summer-staff to read the document.

Finally, there are protection requirements that are based on some triggering conditions (expressed again as a combination of authorizations) to derive authorizations for future instants. In this case, it is sufficient that the condition is verified in a single instant to derive the authorization for all future instants according to the rule's constraints. The UPON operator, used by rules [R.sub.2] and [R.sub.5] in Figure 1, has been introduced to meet these requirements. By rule [R.sub.5] an authorization to user Tom for writing paychecks in a working day within 1995 or 1996 is used as a triggering condition to issue an authorization to user Ann for reading pay-checks in any subsequent working day up to the last one in 1996.

Although the relations expressed by the temporal operators are intuitively very different from each other, a question can arise about the minimality of the set of operators that we have chosen to express these relations. Technically, when the interval associated with each rule is finite, any ASLONGAS or WHENEVER rule can be simulated by a set of UPON rules. For example, the same derivations obtained by R = ([begin, end], P, A WHENEVER A) can be obtained by the set:

([[t.sub.b], [t.sub.b]], P, A UPON A)

([[t.sub.b] + 1, [t.sub.b] + 1], P, A UPON A)

...

([[t.sub.e], [t.sub.e]], P, A UPON A)

where [t.sub.b] and [t.sub.e] are the instants corresponding to begin and end, respectively. The simulation is much more complex for ASLONGAS rules. Technical details are not appropriate for this discussion, but it suffices to note that this simulation requires the introduction of twice the number of "auxiliary" authorizations as there are instants satisfying the constraints associated with the rule. It is easily seen that these simulations are highly impractical from a representational point of view, and that the access control algorithm would be extremely inefficient if operating on such a representation. Moreover, the simulation is not possible for rules with unbound intervals. We conclude that there are both expressiveness and efficiency arguments supporting the choice of the three temporal operators.

3.3 Formal Semantics

In this section we give the formal semantics of periodic authorizations and derivation rules. We start by introducing the concept of a TAB.

Definition 11. A temporal authorization base (TAB) is a set of periodic authorizations and derivation rules.

In the following, we use symbol [A.sub.i] as a shorthand for the 5-tuple ([s.sub.i], [o.sub.i], [m.sub.i], [pn.sub.i], [g.sub.i]), whereas [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] forces [pn.sub.i] = `-', and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] forces [pn.sub.i] = `+'.

The semantics of a TAB is given as a set of [Datalog.sup.not, [equivalent]Z, [is less than]Z] clauses. [Datalog.sup.not, [equivalent] Z,[is less than]Z] is the extension of Datalog with nonmonotonic negation, periodicity, and gap-order constraints on the integers (see Appendix A). Programs corresponding to TABs are a very restricted class of [Datalog.sup.not, [equivalent]Z, [is less than]Z] programs: the only predicate symbols are valid(), [valid.sup.f](), once_[valid.sup.f](), once_not_[valid.sup.f](), denied(), and CNSTR(). A set of nontemporal constants ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [A.sub.1], [A.sub.1], ..., [s.sub.i], [o.sub.1], [m.sub.1], ..., +, -, [P.sub.1], ...) is provided to denote positive and negative authorizations, authorizations regardless of their sign, Boolean expressions of authorizations, users, objects, access modes, sign of authorizations, and periodic expressions.(8) Periodicity and order constraints only involve temporal variables and do not use the function +.

Like Falaschi et al. [1988] and Gottlob et al. [1996], we consider nonground interpretations of our programs, defined as sets of constrained atoms of the form (B, [Xi]), where B is a predicate and [Xi] is a temporal constraint. Each constrained interpretation has an equivalent, possibly infinite, Herbrand interpretation containing only ground atoms.

Table II reports the clause/set of clauses in [Datalog.sup.not, [equivalent]Z, [is less than]Z] corresponding to each type of authorization and rule allowed by our model. For brevity, we use the form t" [is less than or equal to] t' [is less than] t as a shortcut for the disjunction (using two clauses) of t' = t" and t" [is less than] t' [is less than] t. In defining the semantics we assume that the Boolean formula A appearing on the right-hand side of the temporal operator in a derivation rule is in disjunctive normal form. Moreover, we assume that, in each conjunct, authorizations preceded by ?? appear before authorizations not preceded by ??. More precisely, we assume A = [C.sub.1] [disjunction] ... [disjunction] [C.sub.n], where [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], where [A.sub.ji], j = 1, ..., m, i = 1, ..., n, are authorizations, k [element of] [0, m], m [element of] [Z.sup.+].

Table II. Semantics of Periodic Authorizations and Rules
([begin, end], P, [A.sup.-]):
valid(t, [A.sup.-]) [left arrow] [t.sub.b] [is less than or equal
  to] t [is less than or equal to] [t.sub.e], CNSTR(P, t)

([begin, end],P, [A.sup.+]) :
valid(t, [A.sup.+]) [left arrow] [t.sub.b] [is less than or equal
  to] t [is less than or equal to] [t.sub.e], CNSTR(P,t),
  not(denied(t,s([A.sup.+]),o([A.sup.+]),m([A.sup.+]))

([begin, end], P, [A.sup.-] WHENEVER A) :
valid(t, [A.sup.-]) [left arrow] [t.sub.b] [is less than or equal
  to] t [is less than or equal to] [t.sub.e], CNSTR(P, t),
  [valid.sup.f] (t,A)

([begin, end], P, [A.sup.+] WHENEVER A) :
valid(t, [A.sup.+]) [left arrow] [t.sup.b] [is less than or equal
  to] t [is less than or equal to] [t.sup.e], CNSTR(P, t),
  [valid.sup.f](t, A), not(denied(t,s([A.sup.+]),[o(A).sup.+],
  m([A.sup.+]))

([begin, end], P, [A.sup.-] ASLONGAS A) :
valid(t, [A.sup.-]) [left arrow] [t.sub.b] [is less than or equal
  to] t [is less than or equal to] [t.sub.e], CNSTR(P, t),
  [valid.sup.f] (t, A), not(once-not-[valid.sup.f] ([t.sub.b],
  t,P,A))

([begin, end],P, [A.sup.+] ASLONGAS A) :
valid(t, [A.sup.+]) [left arrow] [t.sub.b] [is less than or equal
  to] t [is less than or equal to] [t.sub.e], CNSTR(P, t),
  [valid.sup.f] (t, A), not(once_not_[valid.sup.f] ([t.sub.b]t,
  t,P,A)), not (denied(t,s([A.sup.+]),o([A.sup.+]),m([A.sup.+]))

([begin, end], P, [A.sup.-] UPON A) :
valid(t, [A.sup.-]) [left arrow] [t.sub.b] [is less than or equal
  to] t [is less than or equal to] [t.sub.e], CNSTR(P, t),
  once_[valid.sup.f] ([t.sub.b], t,P,A)

(/begin, end],P, A+ UPON A) :
valid(t, [A.sup.+]) [left arrow] [t.sub.b] [is less than or equal
  to] t [is less than or equal to] [t.sub.e], CNSTR(P, t),
  once_[valid.sup.f] ([t.sub.b], t,P,A), not (denied(t,s([A.sup.+]),
  o([A.sup.+]),m([A.sup.+]))

Auxiliary clauses:

denied(t, s, o, m) [left arrow] valid(t, s, o, m, -, g)

{CNSTR(P, t) [left arrow] t [[equivalent].sub.periodicity(P)] y}
[inverted]Ay such that t [[equivalent].sub.periodicity(P)] y ??
  t [element of] [Pi](P)

{once_[valid.sup.f] (t", t,P,A) [left arrow] t" [is less than or
  equal to] t' [is less than or  equal to] t, CNSTR(P, t'),
  [valid.sup.f] (t', A)}
[inverted]A distinct pair (P,A) appearing
  in an UPON rule

{once_not_[valid.sup.f] (t", t,P,A) [left arrow] t" [is less than
  or equal to] t, [is less than] t, CNSTR(P, t'),not([valid.sup.f]
  (t', A))}
[inverted]A distinct pair (r,A) appearing in an ASLONGAS
  rule

{[valid.sup.f] (t, A) [left arrow] not(valid(t, [A.sub.1])), ...,
  not(valid(t, [A.sub.k])), valid(t, [A.sub.k+1]), ...,
  valid(t, [A.sub.m])}
[inverted]A distinct conjunct C = [MATHEMATICAL EXPRESSION
  NOT REPRODUCIBLE IN ASCII], and [inverted]A distinct A
    appearing in a derivation rule


Intuitively, predicate valid() represents the validity of authorizations at specific instants. The fact that (valid(t, A), [Xi]) belongs to an interpretation means that A is valid according to that interpretation at all instants t satisfying [Xi]. Predicate [valid.sup.f] is analogous for Boolean expressions of authorizations. The auxiliary predicates denied(), once_not_[valid.sup.f](), and once_[valid.sup.f]() are introduced to avoid quantification, denied(t, s, o, m) is true in an interpretation if there is at least one negative authorization A such that s(A) = s, o(A) = o, m(A) = m, valid at instant t according to that interpretation, once_not_[valid.sup.f](t", t, P, A) (once_[valid.sup.f] (t", t, P, A), resp.) is true in an interpretation if there is at least one instant t', with t" [is less than or equal to] t' [is less than] t and t and t' [element of] [Pi](P), at which A is not valid (valid, resp.) according to that interpretation.

We denote with [P.sub.TAB] the [Datalog.sup.not,[equivalent]Z,[is less than]Z] program corresponding to a TAB. We consider stable model semantics of logic programs with negation [Gelfond and Lifschitz 1988] to identify the models(9) of [P.sub.TAB]. The notion of constrained interpretation previously presented naturally extends to constrained (nonground) stable models.

We are now ready to formally introduce the notion of valid authorization.

Definition 12. Let M be a model of [P.sub.TAB]. An authorization A is valid at time t with respect to M if there exists (valid(t, A), [Xi]) in M with t satisfying [Xi]. If [P.sub.TAB] has a unique ground model and M is one of its nonground representations, then we simply say that A is valid at time t.

4. A UNIQUE SET OF VALID AUTHORIZATIONS

The presence of negation in our derivation rules introduces the problem of generating a unique set of valid authorizations from a given set of periodic authorizations and rules. There are situations in which different sets of authorizations are generated, depending on the rule evaluation order.

Example 7. Consider a TAB consisting of the following rules.

([R.sub.1]) ([97, 98], Working-days, (manager, report, read, +, Sam)

WHENEVER ??(technical-staff, report, write, +, Sam))

([R.sub.2]) ([97, 98], Working-days, (technical-staff, report, write, +, Sam)

WHENEVER ??(manager, report, read, +, Sam))

If we evaluate [R.sub.1] first, we derive authorization (manager, report, read, +, Sam) for each working day of 1997 and 1998, and we cannot derive any authorization from [R.sub.2]. If we evaluate [R.sub.2] first, we derive (technical-staff, report, write, +, Sam) for each working day of 1997 and 1998, and we cannot derive any authorization from [R.sub.1].

From the point of view of the semantics, the property of always having a unique set of valid authorizations is guaranteed only if all the models of the program corresponding to a TAB identify the same set of valid authorizations at any instant (or equivalently, there exists a unique ground stable model of [P.sub.TAB]).

In the remainder of this section we formally define restrictions on sets of rules that guarantee a unique ground model for [P.sub.TAB], and present an algorithm for checking the satisfaction of these restrictions. Intuitively, the restrictions require the existence of a unique evaluation order reflecting the intuitive semantics of derivation rules.

4.1 Restrictions on Rules

We use the term past operator (PASTOP) to refer to ASLONGAS and UPON.

Dependencies among authorizations in TAB are identified by the binary relationships affects (??)) and strictly affects (??) defined as follows.

--If there is a rule ([begin, end] , P, [A.sub.m] <OP> A) in TAB, where OP is an arbitrary operator, then for each t [element of] {[[t.sub.b], [t.sub.e]] [intersection] [Pi](P) and for each [A.sub.k] appearing in A, we say that [A.sub.k] at time t affects [A.sub.m] at time t (written [A.sub.k] [t] ?? [A.sub.m] [t]). If authorization [A.sub.k] is preceded by ?? in A, we say that [A.sub.k] at time t strictly affects [A.sub.m] at time t (written [A.sub.k] [t] ?? [A.sub.m] [t]).

--If there is a rule ([begin, end], P, [A.sub.m] <PASTOP> A) in TAB, then for each t, t' [element of] {[[t.sub.b], [t.sub.e]]} [intersection] [Pi](P), with t [is less than] t', and for each authorization [A.sub.k] appearing in A, we say that [A.sub.k] at time t affects [A.sub.m] at time t' (written [A.sub.k][t] ?? [A.sub.m][t']). If authorization [A.sub.k] is preceded by ?? in A or PASTOP = ASLONGAS, we say that [A.sub.k] at time t strictly affects [A.sub.m] at time t' (written [A.sub.k][t] ?? [A.sub.m][t']).

Note that [A.sub.k][t] ?? [A.sub.m][t'] implies [A.sub.k][t] ?? [A.sub.m][t'], for any t, t'. Based on these relationships, we can define the more complex notion of priority among periodic authorizations. Intuitively, an authorization [A.sub.n] at time t has higher priority than authorization [A.sub.m] at time t', if the validity of [A.sub.m] at time t' can be evaluated only after evaluating the validity of [A.sub.n] at time t.

Definition 13. Authorization [A.sub.n] at time t has higher priority than authorization [A.sub.m] at time t' (written [A.sub.n] [t] [is greater than] [A.sub.m] [t']) if one of the following conditions holds.

--A sequence [A.sub.n][t] = [A.sub.1][[t.sub.1]], ..., [A.sub.k-1][[t.sub.k-1]], [A.sub.k][[t.sub.k]] = [A.sub.m][t'] exists such that each element in the sequence affects the successor and there exists one that strictly affects it.

--Two sequences [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] exist such that each element affects the successor in the sequence, and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII];

--An authorization [A.sub.l] and an instant t" exist such that [A.sub.n][t] [is greater than] [A.sub.l][t"] and [A.sub.l][t"] [is greater than] [A.sub.m][t'].

The second condition in the preceding definition implies that negative authorizations have higher priority than their positive counterparts at the same instant.

We are now ready to formally characterize critical sets of derivation rules, that is, sets of rules that could lead to the derivation of different sets of authorizations depending on the evaluation order.

Definition 14. A TAB contains a critical set of rules if and only if there exist an authorization [A.sub.m] in TAB and an instant t such that [A.sub.m] has priority over itself at time t (i.e., [A.sub.m][t] [is greater than] [A.sub.m][t]).

Example 8. It is easy to verify that the rules of Example 7 form a critical set. Take t as an arbitrary instant within a working day of 1997. By the first condition in Definition 13 and rule [R.sub.1] we have (technical-staff, report, write, +, Sam) [t] [is greater than] (manager, report, read, +, Sam) [t]. Similarly, by rule [R.sub.2] we have (manager, report, read, +, Sam)[t] [is greater than] (technical-staff, report, write, +, Sam)[t]. Applying the third condition in Definition 13 (transitivity) we have (technical-staff, report, write, +, Sam) [t] [is greater than] (technical-staff, report, write, +, Sam)[t].

The CSD (critical set detection) algorithm, described in the next section, recognizes and rejects a TAB containing a critical set.

4.2 The CSD Algorithm

Before illustrating the CSD algorithm we need to introduce some notions.

Given a TAB, we introduce its constraint version, denoted as [TAB.sub.CNS], as the set of pairs of the form <x, [Xi]>, where x is either an authorization or rule in TAB and [Xi] is the temporal constraint, corresponding to the values of [begin, end] and P associated with x in TAB. If [A.sub.m] is specified more than once in TAB with different temporal constraints, the constraint [Xi] associated with [A.sub.m] in [TAB.sub.CNS] will be the disjunction of these constraints. Derivation rules are transformed in an analogous way. In the following, given an authorization [A.sub.m] in TAB, [[Xi].sub.m] denotes the temporal constraint associated with [A.sub.m] in [TAB.sub.CNS]. Analogously, [[Xi].sub.R] denotes the temporal constraint associated with rule R in [TAB.sub.CNS].

The algorithm for detecting critical sets is illustrated in Figure 3. It receives as input [TAB.sub.CNS], that is, the constraint version of TAB. It returns FALSE if a critical set exists. Otherwise, it returns a sequence of levels <[L.sub.1], ..., [L.sub.k]> representing a partition of the set of pairs <A, t> for each authorization A appearing, either explicitly or in a derivation rule, in [TAB.sub.CNS] and [t.sub.min] [is less than or equal to] t [is less than or equal to] max-time, where [t.sub.min] is the minimum constant appearing in a gap-order constraint in [TAB.sub.CNS], and max-time is an upper bound for the instant after which the validity of any authorization becomes periodic, max-time is determined as [[bar]t.sub.max] + [bar]k [multiplied by] [P.sub.max], where [[bar]t.sub.max] is the maximum finite constant appearing in a gap-order constraint in [TAB.sub.CNS], [P.sub.max] is the least common multiple (lcm) of all the periodicities appearing in [TAB.sub.CNS], and [bar]k is the maximum number of ASLONGAS and UPON rules in TAB plus one (see Lemma 3 in Appendix B). The reason for introducing max-time is to ensure the finiteness of the instants to be considered in the partition, and hence, the termination of the CSD algorithm. The motivation behind how max-time is determined is that the levels produced by the CSD algorithm are used to determine the set of authorizations valid according to the TAB. Intuitively, for each instant greater than max-time the validity of each authorization can be evaluated considering the corresponding instant in the time period before max-time. Hence, derivation of authorizations can be limited to instants smaller than or equal to max-time, and then extended to [infinity].

[Figure 3 PROGRAM LISTING NOT REPRODUCIBLE IN ASCII]

Each level [L.sub.i] is a set of pairs <[A.sub.j], [[Xi].sub.j,i]>, where [[Xi].sub.j,i] denotes the constraint associated with [A.sub.j] at level [L.sub.i]. In the following, we say that authorization [A.sub.j] appears at level i for instant t if t satisfies [[Xi].sub.j,i]. The intuitive semantics of the levels is that authorizations appearing at lower levels for a certain set of instants have higher priority for evaluation than authorizations appearing at higher levels (for the same or for a different set of instants). In other words, let [A.sub.i] and [A.sub.j] be two authorizations and [t.sub.i] and [t.sub.j] be two time instants. If the level of [A.sub.i] at instant [t.sub.i] is lower than the level of [A.sub.j] at instant [t.sub.j], then the validity of [A.sub.i] at time [t.sub.i] must be evaluated before the validity of [A.sub.j] at time [t.sub.j]. Note that since levels represent a partition of the pairs <A, t>, each authorization belongs to exactly one level for each time instant considered. Levels therefore define an order, from the lowest to the highest level, that must be followed when determining the set of temporal authorizations valid according to the given TAB.

The CSD algorithm works as follows. In Step 1, max-time is substituted to all occurrences of [infinity] in the gap-order constraints of authorizations and rules appearing in [TAB.sub.CNS]. In Step 2, the maximum number of levels max-levels to be generated is determined as the number of authorizations in [TAB.sub.CNS] multiplied by max-time. Intuitively, max-level is the number of different pairs <A, t> to be partitioned. In Step 3, variable top-level, representing the number of levels actually generated, is initialized to 1. Then, in Step 4, all the authorizations appearing in [TAB.sub.CNS] are put at level 1 for all time instants between [t.sub.min] and max-time. In Step 5, the algorithm considers the dependencies caused by negative authorizations (Step 5.1) and by derivation rules (Steps 5.2 and 5.3), and possibly moves authorizations to higher levels. Two operations allow changes to levels: add and delete. They insert in (delete from) levels, pairs of the form <[A.sub.m], [Xi]>. Deleting pair <[A.sub.m], [Xi]> from level h means updating [[Xi].sub.m,h] to be [[Xi].sub.m,h] [conjunction]* ??*[Xi]. Similarly, adding pair <[A.sub.m], [Xi]> to level k means updating [[Xi].sub.m,k] to include all the pairs (PC, GC) present in [Xi]. If [A.sub.m] does not appear in [L.sub.k] before the execution of the add operation, the result of the operation is the insertion of pair <[A.sub.m], [Xi]> in [L.sub.k]. The algorithm uses procedure "move()" to move authorizations to higher levels, move([A.sub.h], [Xi], lev) checks all levels i below lev for which [Xi]' = [[Xi].sub.h,i] [disjunction]* [Xi] [is not equal to] 0. Hence, it deletes <[A.sub.h], [Xi]'> from [L.sub.i] and adds it to [L.sub.lev]. Intuitively, move ([A.sub.h], [Xi], lev) moves authorization [A.sub.h] to level lev for each instant satisfying [Xi] for which [A.sub.H] appears in levels lower than lev. Step 5 is repeated until no changes to the levels are necessary (i.e., all the priorities are satisfied), or the number of levels becomes greater than max-level. In the first case, the levels generated are re turned. In the latter case, a FALSE is returned indicating the presence of a critical set.

Example 9. Consider a TAB containing authorizations [A.sub.1], [A.sub.2], [A.sub.3] and rules [R.sub.1], [R.sub.2], and [R.sub.3] appearing in Figure 1. For brevity, here and in the following examples we assume Days as our basic calendar and Sunday 1/1/95 as our tick 1. Moreover, we do not use the normal form to represent the constraint [Xi], but the more compact form: ({t [[equivalent].sub.k] (y + c)[inverted]Ay = [l.sub.1] ... [l.sub.p]}, [c.sub.1] [is less than or equal to] t [is less than or equal to] [c.sub.2]). [TAB.sub.CNS] is as follows.
   {<(manager, guidelines, write, +, Sam), {(true}, {1/1/95 [is less than or
   equal to] to [is less than or equal to] 5/20/95})}>, <(technical-staff,
   guidelines, read, +, Sam) {({t [[equivalent].sub.7] (y + 1)[inverted]Ay =
   0, ..., 4}, {10/1/95 [is less than or equal to] t})}>, <(staff, document,
   read, +, Sam) {({t [[equivalent].sub.7] (y + 1)[inverted]Ay = 0, ..., 4},
   {1/1/95 [is less than or equal to] t [is less than or equal to]
   12/31/97})}>, <(temporary-staff, document, read, +, Sam) ASLONGAS
   ??(summer-staff, document, read, +, Sam), {({t [[equivalent].sub.7] (y + 1)
   [inverted]Ay = 0, ..., 4}, {1/1/96 [is less than or equal to] t is less
   than or equal to] 12/31/98})}>, <(technical-staff, report, write, +, Sam)
   UPON ??(manager, guidelines, write, +, Sam) [disjunction] ??(staff,
   guidelines, write, +, Sam) {({t [[equivalent].sub.7] (y + 1) y = 0, 4},
   {1/1/95 [is less than or equal to] t})}>, <(technical-staff, guidelines,
   read, +, Sam) {({true}, {1/1/95 [is less than or equal to] t})}>.}.


We then have: [[bar]t.sub.max] = 12/31/98, [t.sub.min] = 1/1/95, [bar]k = 3, [P.sub.max] = 7 (i.e., the periodicity of Weeks), and max-time = 1/21/99. [TAB.sub.CNS] is modified by substituting 1/21/99 to all occurrences of [infinity]. All the authorizations appearing in [TAB.sub.CNS] are initially inserted at level 1 with constraints {({true}, {1/1/95 [is less than or equal to] t [is less than or equal to] 1/21/99})}.

The algorithm then cycles moving authorizations to higher levels as follows.
   1st Iteration.

   Since (technical-staff, report, write, -, Sam) is at level 1: move
   <(technical-staff, report, write, +, Sam), {({true}, {1/1/95 [is less than
   or equal to] t [is less than or equal to] [is less than or equal to]
   1/21/99})}} to level 2.

   Considering rule [R.sub.1]: move <(temporary-staff, document, read, +,
   Sam), {({t [[equivalent].sub.7] (y + 1)[inverted]Ay = 0, ..., 4}, {1/1/96
   [is less than or equal to] t [is less than or equal to] 12/31/98})}} to
   level 2.

   Considering rule [R.sub.3]: move < (technical-staff, report, write, -,
   Sam), {({true}, {1/1/95 [is less than or equal to] t [is less than or equal
   to][is less than or equal to] 1/21/99})]} to level 2.

   2nd Iteration.

   Since (technical-staff, report, write, -, Sam) is at level 2: move
   <(technical-staff, report, write, +, Sam), {({true}, {1/1/95 [is less than
   or equal to] t [is less than or equal to] [is less than or equal to]
   1/21/99})}) to level 3.

   3rd Iteration.


All dependencies are satisfied. No further changes to the levels are necessary and the algorithm terminates returning the levels illustrated in Figure 4.

[Figure 4 PROGRAM LISTING NOT REPRODUCIBLE IN ASCII]

Note that several optimizations are possible on the algorithm in Figure 3, which are not reported here for the sake of simplicity. For instance, the "move()" procedure could keep track of the instants moved and stop if [A.sub.m] has been moved, for all instants satisfying [Xi], without the need to check all levels down to the first one.

The number of levels produced by the CSD algorithm is potentially very high. However, the maximum number of levels can be reached only if either (1) the TAB contains a critical set, or (2) the TAB does not contain any critical set but the priorities are such that the maximum number of levels needs to be produced. Case (1), representing an anomaly in the authorization specifications, should be very unlikely to occur. As for Case (2), if the maximum number of levels is reached, each level must contain exactly one authorization with an associated constraint identifying a single instant. In terms of the authorization specifications this can happen only if there exists a cycle involving ASLONGAS rules. More precisely, two ASLONGAS rules spanning to [infinity] must exist such that each of them contains, in the formula on the right of the operator, the authorization that appears on the left of the operator in the other rule. For instance, it is easy to see that the pair of rules: [R.sub.1] = ([1, [infinity]], [perpendicular to], [A.sub.sub.1] ASLONGAS [A.sub.2]) and [R.sub.2] = ([1, [infinity]], [perpendicular to], [A.sub.2] ASLONGAS [A.sub.1]) would require the computation of all levels up to max-level. A possible solution to this problem is to reject the insertion of any rule causing a cycle in the TAB, regardless of the operators involved in the rules and authorizations causing the cycle. This can be easily accomplished by changing the definition of critical set considering all the affects relationships as strict affects relationships. In this way the worst case performance of the CSD algorithm would be greatly enhanced since the maximum number of levels that can be produced becomes dependent only on the number of authorizations and rules in TAB. However, we prefer to adopt a less restrictive approach, and refuse the insertion of a derivation rule only if its insertion into the existing TAB leads to a corresponding logic program that is neither locally stratified [Gelder et al. 1991], nor equivalent to a locally stratified logic program, and, hence, with a nonclear choice for the rules evaluation order. We accept the insertion of all other rules, even those that could cause the generation of a high number of levels. We believe that real-world specifications will generally require the computation of a very small number of levels.

4.3 Formal Properties

The following theorems state that the partition produced by the CSD algorithm obeys the priority relationships existing in TAB. These theorems extend the results reported in Bertino et al. [1996a] to the consideration of periodic authorizations and derivation rules. Proofs are reported in Appendix B.

THEOREM 1. Let [A.sub.n] and [A.sub.m] be two authorizations appearing in TAB and t, t' be two time instants between [t.sub.min] and max-time. If [A.sub.n][t] ?? [A.sub.m][t'], then either the CSD algorithm returns FALSE or, at the end of the execution, authorization [A.sub.m] for instant t' appears at a level higher than or equal to that of authorization [A.sub.n] for instant t. If [A.sub.n][t] ?? [A.sub.m][t'], then the level is necessarily higher.

THEOREM 2. Let [A.sub.n] and [A.sub.m] be two authorizations appearing in TAB with the same subject, object, and access mode but with different signs. Then, either the CSD algorithm returns FALSE or, at the end of the execution, the positive authorization appears at a level higher than that of the negative authorization for each time instant between [t.sub.min] and max-time.

The correctness of the CSD algorithm is stated by the following theorem.

THEOREM 3. Given a TAB, (1) the CSD algorithm terminates and (2) it returns FALSE iff the TAB contains a critical set.

The authorization state of the system is unique if and only if [P.sub.TAB] has a unique ground model. The uniqueness of the model in absence of critical sets is guaranteed by the following theorem.

THEOREM 4. Given a TAB with no critical sets, the corresponding logic program [P.sub.TAB] has a unique ground model.

Note that more than one finite constrained nonground model of [P.sub.TAB] equivalent to the unique ground model can exist, since the same set of instants can be represented by different constraints.

5. ACCESS CONTROL

Determining whether an access request from user s to exercise access mode m on object o at time t can be authorized requires the system to verify whether an authorization (s, o, m, +, g) valid at time t exists. Two different strategies can be used to enforce access control: run-time derivation and materialization. Under the first approach, the system verifies whether the access request can be authorized by evaluating the derivation rules in TAB according to a top-down strategy. This approach has the advantage that limited actions are required upon modification of the TAB. In particular, addition and removal of authorizations as well as removal of rules can be executed without further actions. Insertion of new rules requires the verification that no critical sets are introduced. However, access control may require the evaluation of several rules, to determine the validity of authorizations and to compute the derived authorizations.

Under the materialization approach, the system permanently maintains all the valid authorizations derivable from a TAB. Access control therefore becomes very efficient: there is no difference in costs between explicit and derived authorizations. As a drawback, the materialization has to be properly updated every time the TAB is modified or whenever an object is created or deleted by a user who specifies rules parametric with respect to the object.(10) In the implementation of the proposed model we have adopted the materialization approach. The main reason behind this choice is that in real systems access requests are generally considerably more frequent than requests modifying authorizations and/or rules. As for creation/deletion of objects subject to parametric rules, we believe that those rules, though possible, will seldom be used in practice. As a matter of fact, although rules parametric with respect to the access mode (allowing the owner to grant any access on an object) or to the subject (allowing the owner to grant an access to everybody or to grant an access if somebody can exercise it) can be imagined to be common in reflecting real-world situations, rules parametric with respect to the object, by which a user can grant access to all objects he owns (or will own) certainly have a much stricter applicability.

In the remainder of this section we illustrate how to compute, given a TAB, the corresponding set of valid authorizations. We start with the following definition originally from Bertino et al. [1996a].

Definition 15. The temporal authorization base extent ([TAB.sub.EXT]) of TAB is the set of valid authorizations derived from TAB.

Authorizations are maintained in [TAB.sub.EXT] using a compact representation similar to that of [TAB.sub.CNS]. Each [A.sub.k] is associated with a temporal constraint [[Omega].sub.k]. <[A.sub.k], [[Omega]k]> is in [TAB.sub.EXT] if authorization [A.sub.k] is valid at each instant t satisfying [[Omega].sub.k].

Given two temporal constraints [Xi] and [Xi]', we say that [Xi] is shift-equivalent to [Xi]' (written [Xi] ??* [Xi]'), if the instants satisfying [Xi] are a transposition of the instants satisfying [Xi]' on the time axis. Formally, [Xi] ??* [Xi]' if [exist][bar] t [element of] N such that t + [bar]t satisfies [Xi]' whenever t satisfies [Xi]. For instance, [Xi] = {({1/1/97 [is less than or equal to] t [is less than or equal to] 1/31/97}, {true})} ?? {((1/1/98 [is less than or equal to] t [is less than or equal to] 1/31/98), {true})} = [Xi]', since for each instant t, t + 365 satisfies [Xi]' whenever t satisfies [Xi].

Figure 5 presents an algorithm for computing [TAB.sub.EXT]. The algorithm is based on the model computation for (locally) stratified [Datalog.sup.not,[equivalent]Z,[is less than]Z] programs given in Appendix A. This computation is represented in the algorithm by an iteration of the inner repeat-until cycle. The termination of each iteration is guaranteed by using a finite constant as an upper bound in constraints and computing [TAB.sub.EXT] only up to that value. The periodicity of our rules and their semantics guarantees that the derivation of authorizations can be performed only for instants smaller than or equal to the finite constant max-time and then extended to [infinity] (Step 3), where max-time = [[bar]t.sub.max] + [bar]k [multiplied by] [P.sub.max] is the constant introduced in the presentation of the CSD Algorithm. However, there are many cases in which it is not necessary to compute the [TAB.sub.EXT] up to max-time. This is the reason for the outer repeat-until cycle. In particular, the algorithm considers two contiguous time intervals after [[bar]t.sub.max] of length equal to the common periodicity in TAB ([P.sub.max]) and checks whether the constraints associated with the derived authorizations and restricted to these intervals are shift-equivalent (Step 2.3). If not, and if the considered intervals do not exceed max-time, it proceeds with another iteration of Step 2, generating a larger [TAB.sub.EXT] using the constant of the previous iteration incremented by [P.sub.max] (Step 2.1). Otherwise, the repeat-until cycle terminates.

[Figure 5 PROGRAM LISTING NOT REPRODUCIBLE IN ASCII]

The following theorem states the termination and the correctness of the algorithm.

THEOREM 5. (1) Algorithm 2 terminates and (2) an authorization A is valid at time [bar]t if and only if there exists <A, [Omega]> in [TAB.sub.EXT] such that [bar]t satisfies [Omega].

In practice, we expect the algorithm to terminate at the first iteration in most cases.

Example 10. Consider the TAB of Example 9. The levels computed by the CSD algorithm are illustrated in Figure 4. We now apply the algorithm for [TAB.sub.EXT] generation. At the first iteration of the repeat-until cycle, k = 2 and current_max = 1/14/99 (12/31/98 + 2 [multiplied by] 7), where 7 is the periodicity of Weeks. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be the [TAB.sub.EXT] resulting from the evaluation of level [L.sub.i]. We have:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] .

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] .

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] .

From <(temporary-staff, document, read, +, Sam) ASLONGAS ?? (summer-staff, document, read, +, Sam), {([t [[equivalent].sub.7] (y + 1)[inverted]Ay = 0, ..., 4}, {1/1/96 [is less than or equal to] t [is less than or equal to] 12/31/98})}> and the authorizations in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] we derive: <(temporary-staff, document, read, +, Sam), {({t [[equivalent].sub.7] (y + 1) [inverted]Ay = 0, ..., 4}, {1/1/96 [is less than or equal to] t [is less than or equal to] 12/31/98))}>. From <(technical-staff, report, write, -, Sam) WHENEVER ??(technical-staff, guidelines, read, +, Sam), {({true}, {1/1/95 [is less than or equal to] t})}>} we derive: <(technical-staff, report, write, -, Sam), {({true}, {1/ 1/95 [is less than or equal to] t [is less than or equal to] 9/30/95}), ({t [[equivalent].sub.7] y y = 0, 6}, {10/1/95 [is less than or equal to] t [is less than or equal to] 1/14/99})}>. Thus,

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

From <(technical-staff, report, write, +, Sam) UPON ??(manager, guidelines, write, +, Sam) [conjunction] ??(staff, guidelines, write, +, Sam), {({t [[equivalent].sub.7] (y + 1) y = 0, 4}, {1/1/95 [is less than or equal to] t})}>} and the authorizations in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] we derive: <(technical-staff, report, write, +, Sam), {({t [[equivalent].sub.7] (y + 1) y = 0, 4}, {10/1/95 [is less than or equal to] t [is less than or equal to] 1/14/99})}>. Hence,

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

success is set to true and the repeat-until cycle terminates. The last step of the algorithm substitutes [infinity] to each value [bar]t such that 1/7/99 [is less than] [bar]t [is less than or equal to] 1/14/99. Hence, [TAB.sub.EXT] is equal to:
   {<(manager, guidelines, write, +, Sam), {({true}, {1/1/95 [is less than or
   equal to] t [is less than or equal to] 5/20/95})}>, <(technical-staff,
   guidelines, read, +, Sam), {({t [[equivalent].sub.7] (y + 1) [inverted]Ay =
   0, ..., 4}, {10/1/95 [is less than or equal to] t})}>, <(staff, document,
   read, +, Sam), {({t [[equivalent].sub.7] (y + 1) [inverted]Ay = 0, ..., 4},
   {1/1/95 [is less than or equal to] t [is less than or equal to]
   12/31/97})}>, <(temporary-staff, document, read, +, Sam), {({t
   [[equivalent].sub.7] (y + 1) [inverted]Ay = 0, ..., 4}, {1/1/96 [is less
   than or equal to] t [is less than or equal to] 12/31/98})>,
   <(technical-staff, report, write, -, Sam), {({true}, {1/1/95 [is less than
   or equal to] t [is less than or equal to] 9/30/95}), ({t
   [[equivalent].sub.7] y y = 0, 6}, {10/1/95 [is less than or equal to]
   t})}>, <(technical-staff, report, write, +, Sam), {({t [[equivalent].sub.7
   (y + 1) y = 0, 4}, {10/1/95 [is less than or equal to] [is less than or
   equal to] t})}>}.


Once we have generated [TAB.sub.EXT], an access request from user [s.sub.1] to exercise access mode [m.sub.1] on object [o.sub.1] at time t will be allowed only if <A, [Omega]> exists in [TAB.sub.EXT] such that s(A) = [s.sub.1], o(A) = [o.sub.1], m(A) = [m.sub.1], pn(A) = "+," and t satisfies [Omega].

6. AUTHORIZATION UPDATES

Valid authorizations can change due to modifications of the TAB. In this section we discuss administrative operations for changing the TAB and illustrate a strategy to incrementally maintain [TAB.sub.EXT] upon the execution of administrative operations.

6.1 Administrative Operations

Administrative operations allow users to specify, delete, or modify authorizations and derivation rules. In our model we assume ownership: the user who creates an object is considered its owner and can, as such, regulate access by others to the object. By regulating access we mean that the user can specify authorizations on the object, either directly or through derivation rules. In other words, the user can specify any authorization on the object and any rule where the object appears on the left-hand side of the operator. Authorizations and derivation rules can then be removed or changed only by the user who specified them.

Administrative operations can be carried out directly on the TAB, that is, allowing users direct access and modification to authorizations/rules, or through specifications in a language for administrative operations. This language would act as an interface between the user and the TAB by interpreting users' requests to add, remove, or modify authorizations and rules and translating them appropriately on the TAB. For instance, a language such as the one presented in Bertino et al. [1996a] can be used.

The development of an administrative policy for the specification of temporal authorizations and rules is beyond the scope of this article. This is the reason behind the choice of the ownership policy, which provides decentralized administration (each user administers her own objects) without the complications that can be introduced by the delegation of administrative privileges. We note, however, that the administrative policy is orthogonal to the authorization model and, therefore, any administrative policy can be applied to our model. For instance, delegation of administration through either administrative privileges (as in Bertino et al. [1996a]) or through grant option (as in Bertino et al. [1997]) can be considered. A user would then be allowed only to specify authorizations/rules if he is so authorized by the administrative policy.

We note that the administrative policy has some effects on how parametric rules are expanded by the system. Remember that parametric rules can contain the wild card character, meaning any value, in place of the subject, object, or access mode in the authorizations. Parametric rules specified by a user can produce only authorizations that the user can specify. In our case, they produce only authorizations on objects owned by the user who specified the rules. To clarify, consider Example 6 and suppose there were two additional objects in the system owned by another user, Jim. The resulting rules would be exactly the same. Note, however, that ownership limits only the value that the object element in the authorization on the left of the operator (the authorization to be derived) can assume. It does not limit the value of the object elements in the authorizations on the right of the operator. Rules specified by a user can refer to objects that the user does not own.(11) In the case of parametric rules, if the wild card character appears for the object in the authorization on the left of the operator, it will be instantiated only to objects owned by the user who specified the rules. By contrast, if the wild card character appears only in authorizations on the right of the operator, it can be instantiated to any value.

6.2 Implementation Issues

Administrative operations, by changing the TAB, may change the validity of authorizations and, consequently, require changes to the corresponding [TAB.sub.EXT]. For instance, consider the deletion of a derivation rule. The first effect of this operation is the deletion from [TAB.sub.EXT] of the authorizations, if any, derivable from it. However, the rule deletion may have several other effects on the [TAB.sub.EXT], such as the deletion of other authorizations in addition to the one directly derivable from the rule. This happens if the authorization on the left-hand side of the deleted rule appears on the right-hand side of other derivation rules, not preceded by the ?? operator. By contrast, if the authorization on the left-hand side of the deleted rule appears on the right side of other derivation rules preceded by the ?? operator, then the deletion of the rule may cause the insertion of other authorizations in [TAB.sub.EXT]. The rule deletion may also require updating the TAB stratification. Further effects are possible if the deleted rule allows the derivation of a negative authorization. In this case the deletion of the rule may also cause the insertion in [TAB.sub.EXT] of the positive authorizations, if any, that were invalidated by the presence of the negative authorization derivable from the rule. The following example clarifies these concepts.

Example 11. Consider the TAB of Example 9 and the corresponding [TAB.sub.EXT] computed in Example 10. Suppose that rule [R.sub.3] is removed. Authorization (technical-staff, report, write, -, Sam), {({true}, {1/1/95 [is less than or equal to] t [is less than or equal to] 9/30/95}), ({t [[equivalent].sub.7] y y = 0, 6}, {10/1/95 [is less than or equal to] t})}, derived from [R.sub.3], must be removed from [TAB.sub.EXT]. Due to this deletion, now rule [R.sub.2] allows the derivation of authorization (technical-staff, report, write, +, Sam) for each Monday and Friday after 5/20/95, since in the interval [5/21/95, 9/30/95] authorization (technical-staff, report, write, +, Sam) is no longer invalidated by the removed negative authorization. Therefore, authorization (technical-staff, report, write, +, Sam), ({t [[equivalent].sub.7] (y + 1) y = 0, 4}, {5/21/95 [is less than or equal to] t [is less than or equal to] 9/30/95})] must be added to [TAB.sub.EXT]. Moreover, the TAB stratification, illustrated in Figure 4, must be modified. <(technical-staff, report, write, -, Sam), {({true}, {1/1/95 [is less than or equal to] t [is less than or equal to] 1/21/99})}) must be removed from the stratification since R3 was the only element in TAB in which (technical-staff, report, write, -, Sam) appeared. Consequently, <(technical-staff, report, write, +, Sam), {((true}, {1/1/95 [is less than or equal to] t [is less than or equal to] 1/21/99})}> must be moved from level 3 to level 2.

Note that updates similar to those illustrated in Example 11 are required for all the other operations that enforce changes to the TAB. We have devised a set of algorithms for incrementally maintaining the [TAB.sub.EXT] and the TAB stratification without the need for recomputing them upon the execution of administrative operations. The algorithms are based on techniques similar to those used for the maintenance of materialized views in constraint and deductive databases [Gupta et al. 1993; Lu et al. 1996, 1995]. These techniques can be successfully employed in our context due to the correspondence between a TAB and a constraint logic program, shown in Section 3.3. All our algorithms (see Ferrari [1998] for a detailed description) are based on both the Dred [Gupta et al. 1993] and the Stdel algorithm [Lu et al. 1995] for view maintenance, and extend them to the consideration of negative authorizations. The maintenance algorithms we have developed for the periodic model are optimizations of the ones developed for the nonperiodic model [Bertino et al. 1996a], which were based on the Dred algorithm only.

Note that in the worst case the maintenance algorithms must recompute the whole [TAB.sub.EXT] and the TAB stratification. It should be noted, however, that an analysis of the worst-case complexity of the maintenance algorithms is not very significant, since this case is very unlikely to be reached in practice. The worst case arises only if all of these conditions are satisfied:

(1) all the derivation rules in TAB form a unique chain; that is, the set R = {[R.sub.1], ..., [R.sub.n]} of derivation rules in TAB is such that [inverted]Ai [element of]{1, ..., n - 1}: [R.sub.i] = [A.sub.i] <OP> [A.sub.i], [R.sub.i+1] = [A.sub.i+1] <OP> [A.sub.i+1] with [A.sub.i+1] appearing in [A.sub.i];

(2) no pairs of temporal constraints in the derivation rules in TAB are disjoint; and

(3) the administrative operation affects the last rule in the chain.

This is a very unlikely situation. We expect that the size of the chains of derivation rules will be very small in real cases. This expectation is also supported by the experiments we have carried out for the nonperiodic model [Bertino et al. 1996a], which have shown that the materialization strategy can be successfully adopted in practice [Bertino et al. 1996c]. The experiments have been carried out on a HP9000/720 with 64Mb of RAM under the HP-UX 10.01 operating system. The prototype system used to perform the experiments has been implemented on top of the INFORMIX DBMS [Informix Software 1995], using the INFORMIX-ESQL/C language. In particular, the data structures used to implement the authorization model are based on the INFORMIX system catalogues. The graphical interface has been implemented using the OSF/Motif toolkit [Foundation 1993]. In order to test the feasibility of the materialization strategy, the prototype system implements an algorithm enforcing the run-time derivation strategy and all the algorithms to incrementally maintain [TAB.sub.EXT] and the TAB stratification upon the execution of administrative operations. Experiment tests, with TABs of different sizes and characteristics, have shown that the materialization strategy is always preferable to a run-time derivation approach when administrative operations are less than 15-20% of the number of access requests submitted to the system. This is a reasonable assumption in real situations, since, generally, access requests are considerably more frequent than administrative requests.

Based on the prototype system developed for the nonperiodic model, we are currently implementing a prototype system for the model presented in this article. This has required modifying the nonperiodic prototype along two main directions: the implementation of the maintenance algorithms we have developed for the periodic model, and an extension related to the management of periodic time. As we have seen in Section 2, we provide both a symbolic and a constraint formalism to represent periodic time. We are currently implementing a procedure to convert any symbolic expression into an equivalent set of simple periodicity constraints, along the lines sketched in Section 2.3.

Moreover, we are currently investigating efficient algorithms to perform the operations (i.e., union, complement, and intersection) on temporal constraints associated with authorizations and rules, using a preprocessing technique at the symbolic level. Performing the operations at the symbolic level has several advantages, in terms of user friendliness, saving of storage space, and computational cost. However, it seems that, in certain "critical cases," executing the operations necessarily requires a translation into the constraint formalism. The idea is therefore to operate as much as possible at the symbolic level and shift to periodicity and gap-order constraints only when required.

7. CONCLUSIONS AND FUTURE WORK

Existing authorization models are based on the use of authorizations stating permissions of subjects (users, groups, or roles) to access objects. An authorization is considered continuously valid from the time it is granted to the time it is revoked. Mapping real-life protection requirements onto this paradigm often becomes very cumbersome. As a matter of fact, many practical requirements call for more expressiveness and flexibility in specifying authorizations. In this article we have presented an authorization model where authorizations can be periodic and have a limited time of validity. The model also allows users to specify rules for the automatic derivation of new (periodic) authorizations. The resulting model is therefore very flexible and powerful in terms of the kinds of protection requirements that it can represent. Obviously, the flexibility provided to the users requires a nontrivial underlying formal model where temporal constraints, periodicity constraints, and derivation rules can be represented.

We are currently extending our work in several directions. A first direction concerns the investigation of security requirements for new applications, such as workflow systems and computer-supported cooperative work, to assess whether our model is adequate to express those requirements. A second direction concerns the investigation and use of different resolution policies to solve conflicts between positive and negative authorizations. In the article we have assumed the use of the denials-take-precedence policy. This policy has the advantage of always taking the safest solution (i.e., denying the access) in case of conflicts. However, it does not support all forms of exceptions; for instance, it is not possible to specify positive exceptions to negative authorizations. A third direction concerns the enrichment of the authorization specification language. For instance, in the article we have assumed that parametric authorizations can be specified by using a special symbol (the wild card character) that varies across all the values of a domain. Rules can be extended to the consideration of multiple variables, varying over the same domain, in the authorizations within a rule. A fourth direction concerns the development of tools supporting authorization administration. A final direction concerns the investigation of alternative implementation techniques for our model, such as the use of database triggers.

(1) The definitions of Months and Years are not precise, since a period of 400 years should be considered to take into account all the exceptions for leap years.

(2) In our examples, we consider yy as corresponding to year 19yy if yy [is greater than or equal to] 94 and to year 20yy if yy [is less than] 94.

(3) If end = [infinity], no constraint for the upper bound is needed.

(4) It can be shown that any periodic expression [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] can be reduced to the form all. C ?? r.[C.sub.d] where C is a calendar. Then, if C is defined by generate(sp; [C.sub.d]; ([l.sub.1], ..., [l.sub.s])), the corresponding disjunction of linear repeating intervals is given by the formula: [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], where period is the periodicity of C in terms of [C.sub.d].

(5) Note that, since we fixed hour 1 as the first hour of 1/1/1994, the period always starts on a Saturday.

(6) Here and in the following we use intuitive names for periodic expressions, assuming that theyare defined with the syntax shown in Section 2.

(7) We use a set of disjoint intervals T = {[[t.sub.i], [t.sub.j]}, ..., {[t.sub.r], [t.sub.s]]} as a compact notation for the set of natural numbers included in these intervals. Hence, the operation of intersection ([T.sub.1] [intersection] [T.sub.2]) has the usual semantics of set intersection.

(8) Note that when A appears as a predicate argument it denotes a constant that we associate with a Boolean expression of authorizations. Similarly, P denotes a nontemporal constant that we associate with a periodic expression.

(9) Due to the properties of the resulting program, in this case stable models are identical to well-founded models [Gelder et al. 1991].

(10) Note that the creation/deletion of an object subject to a parametric rule can be seen as the insertion/removal of the rule instantiations corresponding to the object.

(11) Administrative privileges can be considered that restrict the objects to which users can refer in rules [Bertino et al. 1996a].

(12) [P.sub.i] contains rules of stratum i, i = 1, ..., n.

REFERENCES

ABADI, M., BURROWS, M., LAMPSON, B., AND PLOTKIN, G. 1993. A calculus for access control in distributed systems. ACM Trans. Program. Lang. Syst. 15, 4 (Sept.), 706-734.

BERTINO, E., BETTINI, C., FERRARI, E., AND SAMARATI, P. 1996a. A temporal access control mechanism for database systems. IEEE Trans. Knowl. Data Eng. 8, 1 (Feb.), 67-80.

BERTINO, E., BETTINI, C., FERRARI, E., AND SAMARATI, P. 1996b. Supporting periodic authorizations and temporal reasoning in database access control. In 22nd International Conference on Very Large Databases (VLDB'96) Proceedings (Mumbay, India, Sept. 3-6), 472-483.

BERTINO, E., BETTINI, C., FERRARI, E., AND SAMARATI, P. 1996c. On using materialization strategies for a temporal authorization model. In Post-SIGMOD Workshop on Materialized Views: Techniques and Applications Proceedings (Montreal, Que., June 6), 34-81.

BERTINO, E., BETTINI, C., FERRARI, E., AND SAMARATI, P. 1997. Decentralized administration for a temporal access control model. Inf. Syst. 22, 4, 223-248.

BERTINO, E., SAMARATI, P., AND JAJODIA, S. 1993. Authorizations in relational database management systems. In First ACM Conference on Computer and Communications Security Proceedings (Fairfax, VA, Nov. 3-5). ACM, New York, 130-139.

DATE, C. 1995. An Introduction to Database Systems, 6th edition. Addison-Wesley, Reading, MA.

FALASCHI, M., LEVI, G., MARTELLI, M., AND PALAMIDESSI, C. 1988. A new declarative semantics for logic languages. In Fifth International Conference and Symposium on Logic Programming Proceedings (Seattle, WA, Aug. 15-19), 993-1005.

FERRARI, E. 1998. Access control mechanisms for database systems: Formal models and architectural aspects. Ph.D. Thesis, Dipartimento di Scienze dell'Informazione, Universita di Milano.

FOUNDATION, O.S. 1993. OSF/Motif Programmer's Guide. Prentice-Hall, Englewood Cliffs, NJ.

GELDER, A. V., Ross, K., AND SCHLIPF, J.S. 1991. The well-founded semantics for general logic programs. J. ACM 38, 3 (July), 620-650.

GELFOND, M. AND LIFSCHITZ, V. 1988. The stable model semantics for logic programming. In Fifth International Conference and Symposium on Logic Programming Proceedings (Seattle, WA, Aug. 15-19), 1070-1080.

GOTTLOB, G., MARCUS, S., NERODE, A., SALZER, G., AND SUBRAHMANIAN, V. 1996. A nonground realization of the stable and well-founded semantics. Theor. Comput. Sci. 166, 1&2, 221-262.

GUPTA, A., MUMICK, I., AND SUBRAHMANIAN, V. 1993. Maintaining views incrementally. In ACM SIGMOD International Conference on Management of Data Proceedings (Washington D.C., May 26-28), 157-166.

INFORMIX SOFTWARE. 1994. The Informix Guide to SQL: Reference and Using Triggers, 1/e, Prentice Hall, Englewood Cliffs, NJ.

JAJODIA, S., SAMARATI, P., SUBRAHMANIAN, V., AND BERTINO, E. 1997. A unified framework for enforcing multiple access control policies. In ACM SIGMOD International Conference on Management of Data Proceedings (Tucson, AZ, May 13-15).

LU, J., LUDASCHER, B., SCHU, J., AND SUBRAHMANIAN, V. 1996. Well-founded views in constraint databases: Incremental materialization and maintenance. Tech. Rep., University of Maryland.

LU, J., MOERKOTTE, G., SCHU, J., AND SUBRAHMANIAN, V. 1995. Efficient maintenance of materialized mediated views. In ACM SIGMOD International Conference on Management of Data Proceedings (San Jose, CA, May 22-25).

NIEZETTE, M. AND STEVENNE, J. 1992. An efficient symbolic representation of periodic time. In First International Conference on Information and Knowledge Management Proceedings. (Baltimore, MD, Nov. 2-5).

REVESZ, P. 1993. A closed form evaluation for Datalog queries with integer (gap)-order constraints. Theor. Comput. Sci. 116, 1, 117-149.

REVESZ, P. 1995. Safe stratified Datalog with integer order programs. In First International Conference on Principles and Practice of Constraint Programming Proceedings (Cassis, France, Sept. 19-22), 154-169.

STEINER, J. G., NEUMAN, C., AND SCHILLER, J.I. 1988. Kerberos: An authentication service for open network systems. In USENIX Conference Proceedings (Dallas, TX, Winter 1988), 191-202.

TOMAN, D., CHOMICKI, J., AND ROGERS, D. 1994. Datalog with integer periodicity constraints. In International Logic Programming Symposium Proceedings (Ithaca, NY, Nov. 13-14), 189-203.

WOO, T. AND LAM, S. 1993. Authorizations in distributed systems: A new approach. J. Comput. Sec. 2, 2&3, 107-136.

Received May 1997; revised November 1997; accepted December 1997

APPENDIX A. [DATALOG.sup.NOT, [equivalent]Z,[is less than]Z]

In this article we used [Datalog.sup.not,[equivalent]Z,[is less than]Z] to specify the semantics of a set of periodic authorizations and rules, and the algorithm to generate implicit authorizations mimics a fixpoint computation of the model of a [Datalog.sup.not,[equivalent]Z,[is less than]Z] program. [Datalog.sup.not,[equivalent]Z,[is less than]Z] is a simple extension of [Datalog.sup.not,[equivalent]Z,[is less than]Z] [Toman et al. 1994] with nonmonotonic negation [Gelder et al. 1991]; however, to our knowledge, it was never considered in the literature. [Datalog.sup.not,[equivalent]Z,[is less than]Z] programs are defined as follows.

Definition A. 1. A [Datalog.sup.not,[equivalent]Z,[is less than]Z] program P is a finite set of (functionfree) clauses of the form

B [left arrow] [D.sub.1], ..., [D.sub.m], not[D.sub.m.+1], ..., not[D.sub.m+n], PC, GC,

where B, [D.sub.1], ..., [D.sub.m+n] are atoms, PC is a satisfiable conjunction of simple periodicity constraints, GC is a satisfiable conjunction of gap-order constraints, and not represents nonmonotonic negation.

Bottom-up evaluation of [Datalog.sup.not,[equivalent]Z,[is less than]Z] programs requires the execution of operations on temporal constraints, that we have defined as sets of pairs (PC, GC). In addition to the operations of conjunction ([disjunction]*) and complement (??*), defined in Section 2.2, we need the operations of subsumption and projection ([Pi]) defined in Toman et al. [1994]. Intuitively, if x, y, and z are the variables in both PC and GC, then [[Pi].sub.xy] (PC, GC) returns a set of pairs ([PC.sub.i], [GC.sub.i]) obtained from (PC, GC) by dropping all the constraints involving variable z, after computing and adding all the constraints on the remaining variables implied by the dropped ones. The [Pi] operation also discards any resulting pair that is inconsistent. The subsumption operation has its intuitive semantics: a pair ([PC.sub.1], [GC.sub.1]) is subsumed by ([PC.sub.2], [GC.sub.2]) (having the same set of variables) if any assignment satisfying ([PC.sub.1], [GC.sub.1]) also satisfies ([PC.sub.2], [GC.sub.2]). Subsumption and projection operations can be easily extended to operate on temporal constraints, similarly to [disjunction]* and ??*.

Temporal constraints serve as a basis to define a nonground interpretation for [Datalog.sup.not,[equivalent]Z,[is less than]Z] programs. A ([equivalent], [is less than]) interpretation is any set of pairs of the form (B, [Xi]), where B is a predicate symbol, and [Xi] is a temporal constraint.

Given a [Datalog.sup.not,[equivalent]Z,[is less than]Z] program P we can define an operator [TP.sup.not,[equivalent]Z,[is less than]Z] that maps ([equivalent], [is less than]) interpretations to ([equivalent], [is less than]) interpretations. In the following we denote with [Pi]* the projection operation on sets [Xi].

Definition A.2. Let P be a [Datalog.sup.not,[equivalent]Z,[is less than]Z] program and I a ([equivalent], [is less than]) interpretation.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where Var(B) denotes the set of free variables in atom B. The variables of the periodicity and gap-order constraints are renamed using the variable names in the associated atoms of the clauses.

We know from the literature that the model of a positive logic program can be computed by the so-called fixpoint iteration method; starting from the empty interpretation all the possible inferences from rules in the program are drawn until a fixpoint is reached.

If we restrict our attention to stratified (or locally stratified) [Gelder et al. 1991] [Datalog.sup.not,[equivalent]Z,[is less than]Z] programs, the following procedure, based on the fixpoint iteration method, can be used to evaluate programs.

Algorithm A.1. (Naive Bottom-up evaluation of stratified [Datalog.sup.not,[equivalent]Z,[is less than]Z] programs). Let P be a [Datalog.sup.not,[equivalent]Z,[is less than]Z] program; let [P.sub.1], ..., [P.sub.n] be a stratification of P.(12)
I := [Phi]
For i := 1 to n do
  repeat
    [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]
    until I does not change
  endfor
  return I


Termination of Algorithm A. 1 is not guaranteed for any stratified [Datalog.sup.not,[equivalent]Z,[is less than]Z] program, as [Datalog.sup.not,[equivalent]Z,[is less than]Z] programs can express any Turing computable function [Revesz 1993]. There is then the necessity to devise syntactic restrictions of stratified [Datalog.sup.not,[equivalent]Z,[is less than]Z] to guarantee termination. One of these restrictions is [Datalog.sup.not,[equivalent]Z,[is less than]D], where D is a finite subset of Z; that is, the gap-order constraints are on a finite subset of the integers. We prove that for any stratified [Datalog.sup.not,[equivalent]Z,[is less than]D] program, Algorithm A.1 terminates returning a nonground representation of the unique (ground) model of the program. The ground model can be obtained with the standard bottom-up evaluation, that is, by replacing in Algorithm A.1 [TP.sup.not,[equivalent]Z,[is less than]D] with the standard TP operator. Finally note that Algorithm A.1 may return different nonground models for the same input program. This simply means that there may be several finite representations for the same ground model. The following theorem formalizes these concepts.

THEOREM A.1. Algorithm A.1 terminates for any stratified [Datalog.sup.not,[equivalent]Z,[is less than]D] program P. Let [M.sub.p] be any output of Algorithm 3 on P. Let [G.sub.p] be the output of the standard bottom-up evaluation of P, then for any predicate symbol B in P:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII],

where [x.sub.1], ..., [x.sub.k] are the free variables in atom B, [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]] denotes the substitution of those variables with constants [c.sub.1], ..., [c.sub.k], and F([Xi]) is the Boolean formula associated with [Xi] (cfr. Section 2.2).

PROOF (TERMINATION). The algorithm consists of a finite iteration, bound by the number of strata in the input program, containing an inner repeat-until cycle. The repeat-until cycle always terminates except in the case where at each iteration either a new element (B, [Xi]) is added to I or a new constraint is generated for a predicate B appearing in I. We show that this is not possible. First of all, the number of predicates in P is finite. Moreover, only a finite number of gap-order constraints can be generated, since we assume that gap-order constraints are on a finite domain. Let us consider periodicity constraints. Let [pc.sub.1], ..., [pc.sub.m] be the set of all the simple periodicity constraints appearing in P. Let [k.sub.i] be the modulo factor in [pc.sub.i], i = 1, ..., m. It is easy to show that the operations performed on simple periodicity constraints by the TP operator ensure that the modulo factor of each simple periodicity constraint appearing in I must be less than or equal to lcm{[k.sub.1], ..., [k.sub.m]}. Hence, only a finite number of simple periodicity constraints can be generated. Therefore, we can conclude that the algorithm terminates.

We prove the second part of the theorem by induction on the number of strata in P. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be the output of the ith iteration of the standard bottom-up evaluation, and let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], be the output of the ith iteration of Algorithm A.1. We prove, by induction on i that, for any predicate symbol B in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] iff there exist [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [c.sub.1], ..., [c.sub.k] such that [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]] [satisfies] F([Xi]), where {[x.sub.1], ..., [x.sub.k]} are the free variables in atom B. In what follows we denote with [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] the output of the jth rule application in the ith iteration of the standard bottom-up evaluation. Similarly, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] denotes the output of the jth rule application in the ith iteration of Algorithm A. 1.

(Basis: i = 1). Proving the thesis is equivalent to proving, by induction on j, that: (a) if [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] such that [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]] [satisfies] F([Xi]), and (b) if there exist [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [c.sub.1], ..., [c.sub.k] such that [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]] [satisfies] F([Xi]), then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

(Basis: j = 1). Let us first consider (a). Let [P.sub.1], ..., [P.sub.n] be the stratification of P. By the definition of a stratified program [Gelder et al. 1991], clauses in stratum [P.sub.1] do not contain negative literals. Therefore, if [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then the first rule applied is a rule B [left arrow] PC, GC. Let Var = {[x.sub.1], ..., [x.sub.k], [y.sub.1], ..., y.sub.l]} be the variables in the rule. If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then there exists a substitution A = [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k], [d.sub.1]/[y.sub.1], ..., [d.sub.l]/[y.sub.l] such that A satisfies PC and GC. Consider the evaluation of B [left arrow] PC, GC by Algorithm A.1. (B, [Xi]) is added to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] if it is not subsumed by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], where [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By hypothesis A [satisfies] F ([Theta]) and, by Lemma 4.7 in Toman et al. [1994], [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]] [satisfies] F([Xi]). Thus, if (B, [Xi]) is not subsumed by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], the thesis holds. If (B, [Xi]) is subsumed by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], it means that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] such that [Xi]' subsumes [Xi]. Therefore [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]] [satisfies] F([Xi]'). Thus, the claim holds. Let us now prove point (b). If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then the first rule application in the first iteration of Algorithm A.1 uses a rule B [left arrow] PC, GC of [P.sub.1], such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], where [Theta] = {(PC, GC}. Let Var = {[x.sub.1], ..., [x.sub.k], [y.sub.1], ..., [[y.sub.l]} be the variables in the rule. By Lemma 4.7 in Toman et al. [1994], [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]] [satisfies] F([Xi]) implies that there exists A = [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]], [d.sub.1]/[y.sub.1], ..., [d.sub.l]/[y.sub.l]], such that A [satisfies] F([Theta]). Thus, when the rule B [left arrow] PC, GC is considered by the standard bottom-up evaluation, B([c.sub.1], ..., [c.sub.k]) is added to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

(Induction). Suppose we have proved the thesis for j; we prove it for j + 1. Consider point (a) first. Suppose that the (j + 1)th rule application of the first iteration of the standard bottom-up evaluation uses rule B [left arrow] [D.sub.1], ..., [D.sub.m], not[D.sub.m+1], ..., not[D.sub.m+n], PC, GC of [P.sub.1]. Let Var = {[x.sub,1], ..., [x.sub.k], [y.sub.1], ..., [y.sub.l]} be the variables in the rule. If B([c.sub.1], ..., [c.sub.k]) is added to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then there exists A = [[[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]], [d.sub.1]/[y.sub.1], ..., [d.sub.l]/[y.sub.l]} such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], A satisfies PC and GC, where [t.sub.r] is the tuple obtained by applying A to [D.sub.r], r = 1, ..., m + n. By inductive hypothesis [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] implies that there exist [[Xi].sub.1], ..., [[Xi].sub.m], such that [t.sub.r] satisfies [[Xi].sub.r], and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Hence, A [satisfies] F([[Xi].sub.r]), r = 1, ..., m. By contrast, the inductive hypothesis implies that since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then there is no ([D.sub.r], [E.sub.r]) in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] such that [t.sub.r] satisfies [[Xi].sub.r], r = m + 1, ..., m + n. Thus, A [satisfies] F (??*[[Xi].sub.r]), r = m + 1, ..., m + n. Therefore, consider the evaluation of B [left arrow] [D.sub.1], ..., [D.sub.m], not[D.sub.m+1], ..., not[D.sub.m+n], PC, GC by Algorithm A.1. (B, [Xi]) is added to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], if it is not subsumed by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], where [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By hypothesis A [satisfies] F([[Xi].sub.r]), r = 1, ..., m and A [satisfies] F(??*[[Xi].sub.r]), r = m + 1, ..., m + n. Moreover, A satisfies PC and GC. Thus, A [satisfies] F([Theta]), and, by Lemma 4.7 in Toman et al. [1994], [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]] [satisfies] F([Xi]). Therefore, if (B, [Xi]) is not subsumed by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], such that [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]] [satisfies] F([Xi]), which proves the thesis. Suppose that (B, [Xi]) is subsumed by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Then, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] such that [Xi]' subsumes [Xi]. This implies that [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]] [satisfies] F([Xi]), if (B, [Xi]), and therefore we can conclude the thesis.

Let us now prove point (b). Suppose that the (j + 1)th rule application of the first iteration of Algorithm A. 1 uses rule B [left arrow] [D.sub.1], ..., [D.sub.m], not[D.sub.m+1], ..., not[D.sub.m+n], PC, GC of [P.sub.1], and let Var = {[x.sub.1], ..., [x.sub.k], [y.sub.1], ..., [y.sub.l]] be the variables in the rule. If (B, [Xi]) is added to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], it means that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], where [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [[Xi].sub.r] is the constraint associated with [D.sub.r] in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By hypothesis, there exist [c.sub.1], ..., [c.sub.k] such that [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]] [satisfies] F([Xi]). This implies, by Lemma 4.7 in Toman et al. [1994], that there exists A = [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]], [d.sub.1]/[y.sub.1], ..., [d.sub.l]/[y.sub.l]] such that A [satisfies] F([Xi]). Then, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and A satisfies PC and GC. Let [t.sub.r] be the projection of A onto the variables in [[Xi].sub.r], r = 1, ..., m + n. Thus, [t.sub.1] satisfies [[Xi].sub.1], ..., [t.sub.m] satisfies [[Xi].sub.m], [t.sub.m+1] satisfies ??*[[Xi].sub.m]+1, ..., [t.sub.m+n] satisfies ??*[[Xi].sub.m+n. By inductive hypothesis, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [t.sub.r] satisfies [[Xi].sub.r], imply [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Similarly, [t.sub.r] satisfies ??*[[Xi].sub.r], implies [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Therefore, when the rule B [left arrow] [D.sub.1], ..., [D.sub.m], not[D.sub.m+1], ..., not[D.sub.m+n], PC, GC is considered by the standard bottom-up evaluation, B([c.sub.1], ..., [c.sub.k]) is added to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

(Induction). Suppose we have proved the thesis for i; we prove it for i + 1; that is, we prove that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] iff there exist (B, [Xi]) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [c.sub,1], ..., [c.sub.k] such that [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]], [satisfies] F([Xi]). Analogously to the basis case, proving the thesis is equivalent to proving, by induction on j, that: (a) if [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] such that [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]], [satisfies] F([Xi]), and (b) if there exist [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [c.sub.1], ..., [c.sub.k] such that [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]], [satisfies] F([Xi]), then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

(Basis: j = 1). We start by proving point (a). Suppose that the first rule application of the (i + 1)th iteration of the standard bottom-up evaluation uses rule B [left arrow] [D.sub.1], ..., [D.sub.m], not[D.sub.m+1], ..., not[D.sub.m+n], PC, GC of [P.sub.i+1. Let Var = {[x.sub.1], ..., [x.sub.k], [y.sub.1], ..., [y.sub.l]} be the variables in the rule. If B([c.sub.1], ..., [c.sub.k]) is added to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then there exists A [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]], [d.sub.1]/[y.sub.1], ..., [d.sub.l]/[y.sub.l]] such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and A satisfies PC and GC, where [t.sub.r] is the tuple obtained by substituting A into [D.sub.r], r = 1, ..., m + n. By inductive hypothesis, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] implies [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], such that [t.sub.r] satisfies [[Xi].sub.r], r = 1, ..., m. Hence, A [satisfies] F([[Xi].sub.r]), r = 1, ..., m. By contrast, the inductive hypothesis implies that since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then there is no ([D.sub.r], [[Xi].sub.r]) in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] such that [t.sup.r] satisfies [[Xi].sub.r], r = m + 1, ..., m + n. Hence, A [satisfies] F (?? *[[Xi].sub.r]), r = m + 1, ..., m + n. Therefore, consider the evaluation of B [left arrow] [D.sub.1], ..., [D.sub.m], not[D.sub.m+1], ..., not[D.sub.m+n], PC, GC by Algorithm A.1. (B, [Xi]) is added to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], if it is not subsumed by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], where [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [Theta] = [[Xi].sub.1] [conjunction]* ... [conjunction]* [[Xi].sub.m] [conjunction]* ?? * [[Xi].sub.m+1] [conjunction]* ... [conjunction]* ?? * [[Xi].sub.m+n] [conjunction]* {(PC, GC)}. Using the same reasoning we used to prove the corresponding case in the inductive step when i = 1, we can conclude that this implies [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] such that [[c.sub.1]/[x.sub.1], ..., [c.sub.k]/[x.sub.k]] [satisfies] F([Xi]'), which proves the thesis.

We omit the proof of point (b) since it is analogous to the proof of the corresponding case in the inductive step when i = 1

(Induction). We omit the proof of the inductive step as it is analogous to the corresponding case for i = 1. []

APPENDIX B. PROOFS

In the following we use P instead of [P.sub.TAB] to denote the logic program associated with a TAB. We start by introducing some definitions and lemmas that are used in the proofs. Let [P.sub.(t [is less than or equal to][bar]t])] be the program P where for each temporal variable t appearing in a rule, we add the gap-order constraint t [is less than or equal to] [bar]t to the body of the rule, where [bar]t is a temporal constant. [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is its ground stable model, whereas [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] denotes any nonground representation of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. The following lemma says that if we are interested in the validity of authorizations at a given instant, we can ignore any ground rule involving instants greater than the given one.

LEMMA B.1. For any instant [bar]t, valid([bar]t, A) [element of] [G.sub.P] iff valid([bar]t, A) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

PROOF (SKETCH). For each type of rule with valid([bar]t, A) in the head, no literal in the body contains a temporal variable that can take values greater than [bar]t for the same rule instance. []

Let P' be the subset of all instantiated (ground) rules in P obtained dropping any rule with a trivially false atom in the body (e.g., 2 [is less than or equal to] 1 [is less than or equal to] 3 or 3 [[equivalent].sub.2] 4). Similarly to [P.sub.(t [is less than or equal to] [bar]t)], we can define [P'.sub.(t [is less than or equal to] [bar]t])], obtaining a finite set of rules where each temporal variable has been substituted by a constant less than or equal to [bar]t. Consider now the program [P".sub.(t [is less than or equal to] [bar]t])] obtained from [P'.sub.(t [is less than or equal to] [bar]t])] by the following substitutions:

(a). each literal not([once_not_valid.sup.f]([t.sub.b], [t.sub.k], P, A)) appearing in the body of a rule is replaced by the set of literals {[valid.sup.f](t', A)|[t.sub.b] [is less than or equal to] t' [is less than] [t.sub.k] [conjunction] t' [element of] [Pi](P)};

(b). each literal not(denied([t.sub.k], s, o, m)) appearing in the body of a rule is replaced by the set of literals {not(valid([t.sub.k], A))|A = (s, o, m, -, g) appears in TAB};

(c). each rule r containing the literal [once_valid.sup.f]([t.sub.b], [t.sub.k], P, A) in its body is replaced by the set of rules obtained by substituting [once_valid.sup.f]([t.sub.b], [t.sub.k], P, A) in r with the elements in the set {[valid.sup.f](t', A)|[t.sub.b] [is less than or equal to] t' [is less than or equal to] [t.sub.k] [conjunction] t' [element of] [Pi](P)};

(d). each rule r containing the literal [valid.sup.f]([t.sub.k], A), with A = [C.sub.1] [disjunction] ... [disjunction] [C.sub.n], and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], for k [element of] [0, m] m, n [element of] [Z.sup.t], and i = 1, ..., n, in its body is replaced by n rules obtained by substituting [valid.sup.f]([t.sub.k], A) in r with the conjunction of literals obtained by replacing each ?? [A.sub.ji] [element of] [C.sub.i] with not(valid([t.sub.k], [A.sub.ji])) and each [A.sub.li] [element of] [C.sub.i] with valid([t.sub.k], [A.sub.li]), for each i = 1, ..., n.

(e). each rule r containing the literal CNSTR(P, [t.sub.k]) in its body is replaced by the set of rules obtained by substituting CNSTR(P, [t.sub.k]) in r with the elements in the set {[t.sub.k] [[equivalent].sub.periodicity(P)] y|(CNSTR(P, [t.sub.k]) [left arrow] [t.sub.k] [[equivalent].sub.periodicity(P)] y, t [is less than or equal to] [bar]t) [element of] [P'.sub.(t [is less than or equal to] [bar]t])}.

(f). any rule having [valid.sup.f](), [once_valid.sup.f](), [once_not_valid.sup.f](), denied(), and CNSTR() as head is deleted.

Since we have shown that any symbolic periodic expression can be translated into an equivalent finite set of simple periodicity constraints, and we are considering rule instances where t is bound, the resulting set of rules in [P".sub.(t [is less than or equal to] [bar]t])] is finite. Note that all the rules in [P".sub.(t [is less than or equal to] [bar]t])] have predicate valid() as head. The following lemma formally states the equivalence between [P".sub.(t [is less than or equal to] [bar]t])] and [P.sub.(t [is less than or equal to] [bar]t])].

LEMMA B.2. For any instant [bar]t, valid([bar]t, A) [element of] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] iff valid([bar]t, A) [element of] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

PROOF (SKETCH). Considering the preceding transformation it is easy to verify that each atom valid() can be derived using a rule in P' iff it can be derived using the corresponding rule in P". Then, it is sufficient to remember that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is equal to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. []

In the following, we denote with [C.sub.i] (Configuration i) the valid authorizations at instants contained in the ith maximum period after [bar][t.sub.max], where [bar][t.sub.max] is the maximum finite constant in TAB. Formally, [C.sub.i] = [valid(t, A) | valid(t, A) [element of] [G.sub.P"] (t [is less than or equal to] [[bar]t.sub.max] + i [multiplied by] [P.sub.max]) and [[bar]t.sub.max] + (i - 1) [multiplied by] [P.sub.max] [is less than] t [is less than or equal to] [[bar]t.sub.max] + i [multiplied by] [P.sub.max]}. It is easy to verify that [C.sub.i] is a subset of [G.sub.P"] (t [is less than or equal to] [[bar]t.sub.max] + j [multiplied by] [P.sub.max]), for each j [is greater than or equal to] i. We define [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] as true if for each atom in [C.sub.i] a corresponding one (with the same authorization) can be found in [C.sub.j] by "shifting" the temporal instant by the value (j - i) [multiplied by] [P.sub.max], and vice versa.

LEMMA B.3. There exists an integer [bar]k such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for each k [is greater than] [bar]k. The integer [bar]k is limited by one plus the number of ASLONGAS and UPON rules in TAB having an unbound associated interval.

PROOF. To prove the thesis it is sufficient to consider the derivation of atoms valid() at instants greater than [bar][t.sub.max]. Since any derivation of atoms valid() with a constant greater than [bar][t.sub.max] is possible only through a rule with an unbound associated interval (a constraint [t.sub.b] [is less than or equal to] t with no upper bound), we only consider authorizations and rules in TAB with an unbound associated interval. The proof is articulated in the following main steps.

(1) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] implies that there exists a pair of rules in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] instantiating the same rule in TAB for two instants t and t' in the ith period with t [is less than] t', such that (1) either the rule operator is ASLONGAS and the rule with t fires and the one with t' does not, or (2) the operator is UPON and the rule with t does not fire and the one with t' does. Intuitively, this statement says that, in the ith period, either an ASLONGAS rule "expires" or an UPON rule "triggers." To prove this statement we first note that if only explicit authorizations and WHENEVER rules are present in TAB, then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Hence, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] implies the existence of a pair of rules in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], corresponding to the same ASLONGAS rule [R.sub.a] or to the same UPON rule [R.sub.u], and of an authorization A such that the rules derive valid(t, A) and not valid(t + [P.sub.max], A), or vice versa. Consider first the ASLONGAS case with [R.sub.a] = [begin, [infinity]], P, A ASLONGAS A, and let t' with t [is less than] t' [is less than or equal to] t + [P.sub.max] be the first instant, satisfying the periodicity constraint, for which a rule in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] corresponding to [R.sub.a] cannot derive valid(t', A). Thus, a literal L (corresponding to an element of the A expression) in the body of the rule is false for time t'. t' could be in the ith period in which case the preceding statement would be proved, or in the (i + 1)th period. In this last case, since it is the first instant, we have that literal L is true for t' - [P.sub.max] and false for t'. Then, we can recursively apply the same reasoning for L as for valid(t, A). It is easily seen that, eventually, either we find an ASLONGAS rule that "expires" in the ith period, or we find a literal derived by an UPON rule.

Similar reasoning can be done for the UPON rule case; that is, we consider the first instant t' for which the rules in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] corresponding to [R.sub.u] can derive valid(t', A). Eventually, either we find an UPON rule that "triggers" in the ith period, or we find a literal derived by an ASLONGAS rule. Hence, the statement in item (1) holds.

(2) Given two pairs ([C.sub.i], [C.sub.i+1]) and ([C.sub.k], [C.sub.k+1]) such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], the rules expiring (triggering, resp.) in the ith period and in the kth period, as stated previously, correspond to different ASLONGAS (UPON, resp.) derivation rules in TAB. Indeed, consider the case of ASLONGAS. We assume, without loss of generality, that i [is less than] k. Let [R.sub.a] be one of the ASLONGAS derivation rules expiring in the ith period, and let [R.sub.t], be the rule in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] corresponding to [R.sub.a] for the first instant t' in the ith period (as chosen previously), such that [R.sub.t], cannot be fired to derive valid(t', A). Hence, at least one of the literals in [R.sub.t], is false. We know that the literals corresponding to temporal constraints in [R.sub.t], evaluate to true. It is easily seen from the semantics of ASLONGAS that all the other literals will be present in all [R.sub.t"] with t" [is greater than or equal to] t' and t" satisfying the periodicity constraint of [R.sub.a]. Suppose, by contradiction, that a rule [R.sub.[bar]t] expires in the (k + 1)th period, that is, a rule in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] corresponding to the same [R.sub.a] in TAB with [bar]t an instant in the kth period. Then, all literals in [R.sub.[bar]t] would have to evaluate to true, including those that evaluated to false in [R.sub.t']. This is clearly a contradiction. The arguments for UPON are similar and we omit them. This proof immediately leads to the result that the maximum number of "different" [C.sub.i]s is limited by one plus the maximum number of ASLONGAS and UPON rules in TAB. Indeed, each rule can be responsible for (at most) one relation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

(3) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] implies [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], for each j [is greater than] i. To prove this statement it is sufficient to show that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] implies [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Suppose by contradiction that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] but [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By the preceding item (1), this means that there exists a pair of rules in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] instantiating the same rule in TAB for two instants t and t' in the (i + 1)th period with t [is less than] t', such that (1) either the rule operator is ASLONGAS and the rule with t fires while the one with t' does not, or (2) the operator is UPON and the rule with t does not fire while the one with t' does. Consider Case (1), and let valid(t, A) be the atom derived by the rule. Hence, valid(t, A) [element of] [C.sub.i+1] and valid(t', A) [is not an element of] [C.sub.i+1]. However, since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then valid(t' - [P.sub.max], A) [is not an element of] [C.sub.i]. This means that rule [R.sub.a] expired in the ith period and this contradicts the fact that the same rule can derive valid(t, A) in the (i + 1)th period. Consider Case (2), and let valid(t', A) be the atom derived by the rule. Hence, valid(t', A) [element of] [C.sub.i+1] and valid(t, A) [is not an element of] [C.sub.i+1]. However, since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then valid(t' - [P.sub.max], A) [element of] [C.sub.i]. This means that rule [R.sub.u] triggered in the ith period and this contradicts the fact that the same rule cannot derive valid(t, A) in the (i + 1)th period.

From items 2 and 3, we can easily conclude the thesis. []

In the following, we denote with max-time the constant [[bar]t.sub.max] + [bar]k [multiplied by] [P.sub.max], where [bar]k is the finite constant defined in Lemma B.3. This constant is used in many of the following proofs.

The next two lemmas are essential steps toward the proofs of Theorems 1, 2, and 3.

LEMMA B.4. Let [A.sub.m] be an authorization appearing in [TAB.sub.CNS]. Then, either the CSD algorithm returns FALSE or authorization [A.sub.m] is in one and only one level for each time instant between [t.sub.min] and max-time. Formally, [[inverted]A.sub.m], t ([A.sub.m] appears in [TAB.sub.CNS] and [t.sub.min] [is less than or equal to] t [is less than or equal to] max-time) ?? [exists]! [L.sub.i] such that <[A.sub.m], [[Xi].sub.m,i]> [element of] [L.sub.i] and t satisfies [[Xi].sub.m,i].

PROOF. Suppose that the algorithm does not return FALSE. After execution of Step 4, each authorization [A.sub.m] in [TAB.sub.CNS] appears in level [L.sub.1] for each t such that [t.sub.min] [is less than or equal to] t [is less than or equal to] max-time. Any change in levels, made either directly in Step 5.1 or through a call of procedure move in Steps 5.2 or 5.3, can be always reduced to a pair of delete-add operations: the first deletes <[A.sub.m], [Xi]> from some level l, the second adds <[A.sub.m], [Xi]> at some level k. Deleting <[A.sub.m], [Xi]) from level 1 means updating [[Xi].sub.m,l] to be [[Xi].sub.m,l] [conjunction]* ??*[Xi]. Adding <[A.sub.m] [Xi]> to level [L.sub.k] means updating [[Xi].sub.m,k] to be [[Xi].sub.m,k] [union] [Xi]. Consider a t such that t satisfies [[Xi].sub.m,l] before the execution of such a pair of delete-add operations. Suppose t satisfies [Xi]. Then, after execution of these operations, t does not satisfy [[Xi].sub.m,l] and t satisfies [[Xi].sub.m,k] Suppose t does not satisfy [Xi]. Then, after execution of these operations, t satisfies [[Xi].sub.m,l] and t does not satisfy [[Xi].sub.m,k]. Hence, after these operations <[A.sub.m], t> still appears in exactly one level. []

Given Lemma B.4, in the following, we refer to the level i such that t satisfies [[Xi].sub.m,i] as L([A.sub.m][t]).

LEMMA B.5. Let <x, [[Xi].sub.R]> be an element in [TAB.sub.CNS] such that x = [A.sub.m] <OP>A, and let [A.sub.n] be an authorization appearing in A. Then either the CSD algorithm returns FALSE or the following implications hold.

-- [inverted]A t satisfying [[Xi].sub.R]: L([A.sub.m][t]) [is greater than or equal to] L([A.sub.n][t]). The disequality is strong ([is greater than]) if [A.sub.n] appears preceded by ?? in A;

-- if OP = PASTOP, then: [inverted]A t, t' satisfying [[Xi].sub.R], t [is less than] t': L([A.sub.m][t']) [is greater than or equal to] L([A.sub.n][t]). The disequality is strong ([is greater than]) if either [A.sub.n] appears preceded by ?? in A or OP = ASLONGAS.

PROOF. Suppose the algorithm does not return FALSE. Then top-level [is less than or equal to] max-level and the algorithm has terminated because there were no changes in the last cycle of the repeat-until statement in Step 5. Since all the elements in [TAB.sub.CNS] are evaluated in each repeat-until cycle, element <x, [[Xi].sub.R]> has also been evaluated. We prove the lemma by proving that: (1) after each evaluation of <x, [[Xi].sub.R]> by the algorithm, the implications held and (2) no evaluations of the other elements in [TAB.sub.CNS] during the last iteration of the algorithm can have changed the property in (1). The proof is based on the fact, which can be trivially proven, that after the execution of move ([A.sub.h], [Xi] lev), L([A.sub.h][t]) [is less than or equal to] lev for all t satisfying [Xi].

(1) Suppose OP = WHENEVER. Consider an instant t satisfying [[Xi].sub.R] and let l be the level such that l = L([A.sub.n][t]). Then t satisfies [Xi] = [[Xi].sub.R] [conjunction] * [[Xi].sub.n,l]. Hence, according to the call made to procedure move(), after execution of Step 5.2, L([A.sub.m][t]) = l + i [is greater than] l = L([A.sub.n][t]) if [A.sub.n] appears in A preceded by ??, and L([A.sub.m][t]) = l = L([A.sub.n][t]) otherwise. Hence the preceding implications are satisfied. Suppose OP = (PASTOP>. Let [PC.sub.1], ..., [PC.sub.k] be the periodicity constraints in [[Xi].sub.R]. Consider t, t' satisfying [[Xi].sub.R] such that t [is less than] t' and let l be the level such that l = L([A.sub.n][t]). Then there exists a [t.sub.l] [is less than or equal to] t such that [t.sub.l] satisfies [[Xi].sub.R] [conjunction] * [[Xi].sub.n,l]. Hence, according to the call made to procedure move(), after execution of Step 5.3, L([A.sub.m][t]) = L([A.sub.m][t']) = l + 1 [is greater than] l = L([A.sub.n][t]) if [A.sub.n] appears in A preceded by ??. Otherwise, L([A.sub.m][t]) = L([A.sub.m][t']) = l = L([A.sub.n][t]) if OP = UPON, whereas L([A.sub.m][t]) = L([A.sub.m][t']) = l + 1 [is greater than] l = L([A.sub.n][t]) for [t.sub.l] [is less than] t and L([A.sub.m][[t.sub.l]]) = l = L([A.sub.n][[t.sub.l]]) if OP = ASLONGAS. Hence the preceding implications are satisfied.

(2) Levels are changed either directly in Step 5.1 or, through procedure move(), in Steps 5.2 and 5.3. In Step 5.1, pairs <[A.sub.m], [Xi]> are possibly deleted from a given level h and added to level l + 1, with h < l + 1. Procedure move() deletes a pair <[A.sub.m], [Xi]> from a level i and adds it to level lev, with i [is less than or equal to] lev. Then, pairs <[A.sub.m], [Xi]> can be moved only to higher levels; that is, the level of an authorization for an instant is never lowered. Then, the property in (1) can be changed, in the last iteration of the algorithm, only by raising the level of [A.sub.n] [t] after the evaluation of <x, [[Xi].sub.R]). But this cannot be since it would contradict the assumption that no changes have been made in the last cycle of the repeat-until statement in Step 5. []

Before proving Theorem 1 it is important to note that [TAB.sub.CNS] is only a compact representation of the authorizations and rules in TAB. Then, the levels in which the authorizations appearing in [TAB.sub.CNS] are partitioned by the CSD algorithm apply also to the authorizations appearing in TAB. Given this, in the following, we consider TAB and [TAB.sub.CNS] as equivalent.

PROOF (THEOREM 1). Theorem i descends directly from Lemma B.5 and from the fact that, according to the definition of ?? and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and

-- if t = t', then there exists a rule R = ([begin, end] , P, [A.sub.m] <OP>A) in TAB with t [element of] {[[t.sub.b], [t.sub.e]]} [intersection] [Pi](P) and [A.sub.n] appears in A. Moreover, [A.sub.n] appears preceded by ?? in A if [A.sub.n] strictly affects [A.sub.m];

-- if t [is less than] t', then there exists a rule R = ([begin, end], P, [A.sub.m] <PASTOP>A) in TAB with t [element of] {[[t.sub.b], [t.sub.e]]} [intersection] [Pi](P), and An appears in A. Moreover, if [A.sub.n] strictly affects Am, then either OP = ASLONGAS or [A.sub.n] appears preceded by ?? in A. []

PROOF (THEOREM 2). We need to prove that either the algorithm returns FALSE or for each pair of authorizations [A.sub.m] and [A.sub.n] appearing in TAB such that s ([A.sub.m]) = s ([A.sub.n]), o ([A.sub.m]) = o ([A.sub.n]), m ([A.sub.m]) = m ([A.sub.n]), pn ([A.sub.m]) = "+," pn ([A.sub.n]) = "-," at the end of the execution L([A.sub.m][t]) [is greater than] L([A.sub.n][t]) for each instant t such that [t.sub.min] [is less than or equal to] t [is less than or equal to] max-time. Suppose that the algorithm does not return FALSE. Then, top-level [is less than or equal to] max-level and the algorithm has terminated because there was no change in the last cycle of the repeat-until statement of Step 5. Since all negative authorizations are considered at each iteration of Step 5 (Step 5.1), [A.sub.n] has also been considered. We prove the theorem by proving that: (1) after the evaluation of [A.sub.n] by the algorithm, L([A.sub.m][t]) [is greater than] L([A.sub.n][t]) for any t such that [t.sub.min] [is less than or equal to] t [is less than or equal to] max-time, and (2) nothing in the execution of the last iteration of the algorithm can have changed the property in step (1).

(1) Consider a t such that [t.sub.min] [is less than or equal to] t [is less than or equal to] max-time and let l be the level such that l = L([A.sub.n][t]). Then t satisfies [[Xi].sub.i] for some set [S.sub.i] at level l. Since each authorization appears at some level for every instant between [t.sub.min] and max-time, t satisfies [[Xi].sub.m,h], for some level h. If h [is greater than] l the implication is trivially satisfied, since levels above l are not changed by Step 5.1. Suppose h [is less than or equal to] l. Then, t satisfies [Xi] = [[Xi].sub.m,h] [conjunction] * [[Xi].sub.i]. Hence, after the execution of the delete-add operations, L([A.sub.m][t]) = l + 1 [is greater than] l = L ([A.sub.n][t]).

(2) The proof is the same as that of point (2) in Lemma B.5. []

PROOF (THEOREM 3).

(1) The only step that may introduce a loop in the algorithm is Step 5. Step 5 is a repeat-until cycle composed of three substeps. These substeps iterate either considering all the levels down to level I or considering all the elements in a finite set. Hence, they necessarily terminate. Consider the outer repeat-until cycle. Suppose that it never stops. Then, at each iteration, the statement in the repeat-until evaluates to true; that is, changes have occurred in some level and top-level [is less than or equal to] max-level. Changes can only move authorizations to higher levels and every time a new level is created top-level is increased by 1. If changes keep occurring at every iteration, eventually top-level will reach max-level, and the repeat-until cycle terminates, which contradicts the assumption. Hence, the algorithm terminates.

(2) We first prove that if the TAB contains a critical set then the algorithm returns FALSE. Suppose that a critical set exists in the TAB; that is, an authorization [A.sub.m] and an instant t exists such that [A.sub.m][t] [is greater than] [A.sub.m][t]. Then, at least one of the conditions in Definition 13 is satisfied. (Note that the algorithm considers only the time instants up to max-time. However, there is no need to consider all time instants up to [infinity]. If a dependency between two authorizations exists for a time instant after max-time it also exists for a time instant lower than or equal to max- time.)

Suppose that the first condition is satisfied. A sequence [A.sub.m][t] = [A.sub.1][t], ..., [A.sub.k-1][t], [A.sub.k][t] = [A.sub.m][t] exists such that each element in the sequence affects the successor and there exists one that strictly affects it. By Theorem 1, each ?? relation implies a [is less than or equal to] relationship on the resulting levels and each [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] relation implies a [is less than] relationship among levels. Then, we should have L([A.sub.m][t]) [is less than] L([A.sub.m][t]), which cannot be since, according to Lemma B.4, L([A.sub.m][t]) is unique.

Suppose that the second condition is satisfied. Two sequences [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] exist such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and each element in each sequence affects the successor and there exists one that strictly affects it. Note that the time instant must be the same along the two sequences since, by definition of ??, and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], the time instant on the right-hand side of the relationships is always either greater than or equal to the time instant on the left-hand side and by assumption [A.sub.m][t] initiates the first sequence and terminates the second. Then, from Theorem 1, L([A.sub.m][t]) [is less than] L([A.sub.l][t]) and L(Al+l[t]) [is less than] L(Am[t]). Moreover, from Theorem 2 L([A.sub.l][t]) [is less than] L([A.sub.l+1][t]). Hence, again we should obtain L([A.sub.m][t]) [is less than] L([A.sub.m][t]), which cannot be because of the uniqueness of L([A.sub.m][t]) (Lemma B.4).

The proof for the last case of Definition 13 descends directly from the previous ones.

We now prove that if the algorithm returns FALSE, then a critical set exists in TAB. Suppose the algorithm returns FALSE. Then, top-level [is greater than] max-level, top-level is increased by 1 by the algorithm whenever a pair <[A.sub.m], [Xi]> needs to be put at a level l + 1 [is greater than] top-level (Step 5.1 of the algorithm or procedure move() called in Steps 5.2 and 5.3). We first show that the request to delete <[A.sub.m], [Xi]> from a given level and put it to level l + 1 implies that, for each instant t' satisfying [Xi] either:

(1) pair <[A.sub.n], [[Xi].sub.n,l]) [element of] [L.sub.l] exists such that s ([A.sub.m]) = s ([A.sub.n]), o ([A.sub.m]) = o ([A.sub.n]), m([A.sub.m]) m([A.sub.n]), pn([A.sub.n]) = "," pn([A.sub.m]) "+," and t' satisfies [[Xi].sub.n,l], or

(2) pair <[A.sub.n], [[Xi].sub.n,l]> [element of] [L.sub.l] exists such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some t satisfying [[Xi].sub.n,l].

Suppose that the level is changed in Step 5.1. Then, t' satisfies [[Xi].sub.n,l] [conjunction] * [[Xi].sub.i]. According to the definition of [[Xi].sub.i], there exists [[Xi].sub.n,l] such that t' satisfies [[Xi].sub.n,l], <[A.sub.n], [[Xi].sub.n,l]> [element of] [S.sub.i], and pn ([A.sub.n]) = "-." Moreover, since [A.sub.m] satisfies the condition in the for cycle, s ([A.sub.m]) = s ([A.sub.n]), o ([A.sub.m]) = o ([A.sub.n]), and m ([A.sub.m]) = m ([A.sub.n)]. Then, condition 1 is verified.

Suppose that the level is changed by a call of procedure move() made in Step 5.2. Then, t' satisfies [[Xi].sub.R] [conjunction] * [[Xi].sub.n,l] and [[Xi].sub.R] and n are such that an element <[A.sub.m] WHENEVER A, [[Xi].sub.R]) was evaluated and [A.sub.n] appeared in A preceded by ??. Then, condition 2 is satisfied with t = t'.

Suppose that the level is changed in Step 5.3 by the evaluation of an element <[A.sub.m](PASTOP>A, [[Xi].sub.R]>. Let [PC.sub.1], ..., [PC.sub.k] be the periodicity constraints in [[Xi].sub.R]. Procedure move() is called to move [A.sub.m] to level l + 1 if there exists an authorization [A.sub.n] such that <[A.sub.n], [[Xi].sub.n,l]> [element of] [L.sub.l], [[Xi].sub.R] [conjunction] * [[Xi].sub.n,l] [is not equal to] [Phi] and t' satisfies [[Xi].sub.R] [conjunction] * [[Xi].sub.n,l], and either [A.sub.n] appears in A preceded by ??, or OP = ASLONGAS. In both cases, condition 2 is satisfied with t = [t.sub.l], where [t.sub.l] is the first instant satisfying [[Xi].sub.R] [conjunction] * [[Xi].sub.n,l].

Since top-level [is greater than] max-level, top-level has been increased by 1 at least max-level times. This means that max-level times a relationship of type 1 or 2, above, which required the creation of a new level, has been found by the algorithm. Suppose all relationships were of type 2. Then, a chain of max-level [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] relations [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] exists. Since the total number of different elements [A.sub.x][[t.sub.y]] is max-level, an authorization [A.sub.m] and an instant t exists such that [A.sub.m][t] appears twice in the chain. Then, according to Definition 14, a critical set exists, represented by the subchain starting from [A.sub.m][t] and ending at the other [A.sub.m][t].

Suppose that k relationships, among the max-level found which caused the creation of a new level, were of type 1. Then, k chains of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] relationships exist where the last element [A.sub.v] [t"] in chain h and the first element [A.sub.u][t"] in chain h + 1 are such that s([A.sub.v]) = s([A.sub.u), O([A.sub.v]) = O([A.sub.u]), m ([A.sub.v]) = m ([A.sub.u]), pn ([A.sub.v]) = '-', and pn([A.sub.u]) = `+'. Then, again, since the number of different elements [A.sub.x][[t.sub.y]] is max-level, an authorization [A.sub.m] and an instant t exists such that [A.sub.m][t] appears twice either in the same chain, or in two different chains. In the first case, again a critical set exists because of the subchain of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] relationships going from [A.sub.m][t] to the other [A.sub.m][t]. In the second case a critical set exists represented by the subsequence of chains going from the first [A.sub.m][t] that appears to the other instance of [A.sub.m][t], according to Definition 14. []

PROOF (THEOREM 4). We first show that the absence of critical sets implies the local stratification of PTAB (as defined just after Lemma B.1).

LEMMA B.6. Given a TAB with no critical sets, the logic program [P'.sub.TAB]s is locally stratified.

PROOF. Since TAB has no critical set, the CSD algorithm gives a partition in a finite number of levels of the pairs <A, t> where A is an authorization in TAB and t an instant in {[t.sub.min], ..., max-time}. Using this partition, we define a partition [H.sub.1], ..., [H.sub.[Alpha]] of the (ground) Herbrand base of [P.sub.TAB], where [Alpha] is a countable ordinal. It is obtained applying the following steps in the given order.

(1) Each atom of the form t [is less than or equal to] t' [is less than or equal to] t", t [is less than or equal to] t' [is less than] t", t [[equivalent].sub.k] c, and CNSTR(P, t) is in [H.sub.1];

(2) if valid(t, A) is in the Herbrand Base, but A does not appear in TAB, then valid(t, A) is in [H.sub.1];

(3) each atom [once_valid.sup.f](t, t, A) and [once_not_valid.sup.f](t, t, A) is in [H.sub.1];

(4) each atom valid(t, A) with t [is less than or equal to] max-time is in [H.sub.k] if <A, [Xi]> with t satisfying [Xi] is assigned to level k/3 by the CSD algorithm;

(5) each atom valid(t, A) with t [is greater than] max-time is in [H.sub.k] if valid(r, A) is in [H.sub.s], where r = ((t - [[bar]t.sub.max]) MOD [P.sub.max]) + (max-time - [P.sub.max]), and k = s + n-auth [multiplied by] [P.sub.max] [multiplied by] ((t - [[bar]t.sub.max]) DIV [P.sub.max]); if s [is less than or equal to] 3 then valid(t, A) is in [H.sub.s];

(6) each atom [valid.sup.f](t, A) is in [H.sub.k] where k = max{j | (valid(t, [A.sub.i]) [element of] [H.sub.j] and [A.sub.i] [element of] A) or (valid(t, [A.sub.i]) [element of] [H.sub.j-1] and ??[A.sub.i] [element of] A)};

(7) each atom [once_valid.sup.f](t", t, A) with t" [is less than] t is in [H.sub.k] with k = max{j | [valid.sup.f](t', A) [element of] [H.sub.j] and t" [is less than or equal to] t ' [is less than or equal to] t};

(8) each atom [once_not_valid.sup.f](t", t, A) with t" [is less than] t is in [H.sub.k] where k = 1 + max{j | [valid.sup.f](t', A) [element of] [H.sub.j] and t" [is less than or equal to] t' [is less than] t};

(9) each atom denied(t, s, o, m) is in [H.sub.k] where k = max{j | valid(t, s, o, m, -, g) [element of] [H.sub.j] for any grantor g};

(10) any other atom is in [H.sub.1].

By definition, [P'.sub.TAB] is locally stratified if, for each of its rules C [left arrow] [L.sub.1], ..., [L.sub.n], not[B.sub.1], ..., not [B.sub.m], with C [element of] [H.sub.k], we have [L.sub.i] [element of] [[union].sub.j [is less than or equal to] k] [H.sub.j] for i = 1, ..., n and [B.sub.l] [element of] [[union].sub.j [is less than] k] [H.sub.j] for l = 1, ..., m. This condition is satisfied considering the partition shown previously. For brevity, here we report the proof for only two types of rules in [P'.sub.TAB].

(a) Consider a rule corresponding to a single positive authorization in TAB. We have C = valid(t, [s.sub.1], [o.sub.1], [m.sub.1], +, [g.sub.1]), [L.sub.1] = [t.sub.b] [is less than or equal to] t [is less than or equal to] [t.sub.e], and [L.sub.2] CNSTR(P, t). By Step 1, [L.sub.1], [L.sub.2] [element of] [H.sub.1] and k [is greater than or equal to] 1. [B.sub.1] = denied(t, [s.sub.1], [o.sub.1], [m.sub.1]) and, by Step 9, [B.sub.1] [element of] [H.sub.w] with w = max{j | valid(t, [s.sub.1], [o.sub.1], [m.sub.1], -, g) [element of] [H.sub.j]}. If w [is not equal to] 1 and t [is less than or equal to] max-time, then, by Step 4, valid(t, [s.sub.1], [o.sub.1], [m.sub.1], -, g) [element of] [H.sub.j] if the pair <([s.sub.1], [o.sub.1], [m.sub.1], - g), [Xi]> with t satisfying [Xi] was assigned to level j/3 by the CSD algorithm. Similarly, C [element of] [H.sub.k] because of Step 4, and because the pair (([s.sub.1], [o.sub.1], [m.sub.1], +, [g.sub.1]), [Xi]') with t satisfying [Xi]' was assigned to level k/3 by the CSD algorithm. Theorem 2 ensures that the level of a positive authorization is always greater than that of the corresponding negative authorization for the same instant (if that negative authorization is not in TAB, by Step 2, its corresponding valid() is in [H.sub.1]). Hence, k/3 [is greater than] j/3 and we can easily conclude that k [is greater than] w. If t [is greater than] max-time (this implies that [t.sub.e] = [infinity]), by Step 5, if C [element of] [H.sub.k] it means that valid(r, [s.sub.1], [o.sub.1], [m.sub.1], +, [g.sub.1]) [element of] [H.sub.s] with r = ((t - [[bar]t.sub.max]) MOD [P.sub.max]) + (max-time - [P.sub.max]), and k = s + n-auth [multiplied by] [P.sub.max] ((t - [[bar]t.sub.max]) DIV [P.sub.max]) if k [is greater than] 3, and k = s otherwise. Considering [B.sub.1], the index w of its stratum is given, as shown previously, by Step 9. In this case (t [is greater than] max-time), for any grantor g such that valid(t, [s.sub.1], [o.sub.1], [m.sub.1], -, g) [element of] [H.sub.j], by Step 5, valid(r, [s.sub.1], [o.sub.1], [m.sub.1], -, g) [element of] [H.sub.s'], with j = s' + n-auth [multiplied by] [P.sub.max] [multiplied by] ((t - [[bar]t.sub.max]) DIV [P.sub.max]) if j [is greater than] 3 and [H.sub.j] = [H.sub.s], if j [is less than or equal to] 3. Since r [is less than or equal to] max-time, Theorem 2 can be applied, ensuring that (s/3) [is greater than] (s'/3), and, hence, we have k [is greater than] j. Since, by Step 9 w is the maximum among these js, we conclude k [is greater than w.

(b) Consider now a rule corresponding to an ASLONGAS rule in TAB. If the head of the rule [A.sub.1] is a positive authorization, the corresponding clause has a negative literal denied(). The proof that its stratum is less than k is identical to that shown for Case (a). If A1 is negative, C = valid(t, [A.sub.1]), [L.sub.1] = [t.sub.b] [is less than or equal to] t [is less than or equal to] [t.sub.e], [L.sub.2] = CNSTR(P, t), [L.sub.3] = [valid.sup.f](t, A), and [B.sub.1] = [once_not_valid.sup.f]([t.sub.b], t, A). C, by the stratification given by the CSD algorithm, and by Steps (4) and (5), belongs to [H.sub.k] with k [is greater than or equal to] 3. By Step 1, [L.sub.1], [L.sub.2] [element of] [H.sub.1]. It is also easy to show that [L.sub.3] is assigned to a stratum equal or below that of C. Let us consider the more critical case of [B.sub.1]. If [t.sub.b] = t then [B.sub.1] [element of] [H.sub.1] by Step 3, and k [is greater than or equal to] 3. Otherwise (t [is greater than] [t.sub.b]), by Step 8, [B.sub.1] [element of] [H.sub.s] where s = 1 + max{m | [valid.sup.f](t', A) [element of] [H.sub.m] and [t.sub.b] [is less than or equal to] t' [is less than] t}. For each [t.sub.b] [is less than or equal to] t' [is less than] t, [valid.sup.f](t', A) [element of] [H.sub.m] implies, by Step 6, valid(t', [A.sub.i]) [element of] [H.sub.j] with j [is less than or equal to] m for each [A.sub.i] [element of] A and valid(t', [A.sub.l]) [element of] [H.sub.r] with r [is less than] m for each ?? [A.sub.l] [element of] A. We now distinguish two cases: (a) t [is less than or equal to] max-time, and (b) t [is greater than] max-time. Considering (a), we also have t' [is greater than] max-time and, by Step 4, <[A.sub.i], [[Xi].sub.i]> with t' satisfying [[Xi].sub.i] is assigned to level j/3 by the CSD algorithm, and each <[A.sub.i], [[Xi].sub.l]) with t' satisfying [[Xi].sub.l] is assigned to level r/3. Lemma B.5 states that in this case, the level assigned by the CSD algorithm to ([A.sub.1], [[Xi].sub.1]) with t satisfying [[Xi].sub.1] is strictly greater than the level of any <[A.sub.i], [[Xi].sub.i]> with [A.sub.i] [element of] A or ?? [A.sub.i] [element of] A and t' satisfying [[Xi].sub.i] for each [t.sub.b] [is less than or equal to] t' [is less than] t [is less than or equal to] max-time. By Step 4, <[A.sub.1], [[Xi].sub.1]) with t satisfying [[Xi].sub.1] is assigned to level k/3. Hence, by Lemma B.5, k/3 [is greater than] j/3 and k/3 [is greater than] r/3 for each j and r considered previously. Since k/3 and j/3 must be natural numbers greater than 1, k [is greater than] j + 2 and k [is greater than r + 2. Since tn can be at most equal to j or to r + 1 and s = 1 + max{m | [valid.sup.f](t', A) [element of] [H.sub.m] and [t.sub.b] [is less than or equal to] t' [is less than] t} we can conclude that k [is greater than] s.
   We are left with case (b); that is, t [is greater than] max-time. In this
   case we should consider Step 5 instead of Step 4 used previously. Thus, if
   C [element of] [H.sub.k], then  valid(z, [A.sub.1]) is in [H.sub.w], where
   z = ((t - [t.sub.max]) MOD [P.sub.max]) + (max-time - [P.sub.max]), and k =
   w + n-auth [multiplied by] [P.sub.max] [multiplied by] ((t -
   [[bar]t.sub.max]) DIV [P.sub.max]). Similarly, the valid() atoms
   corresponding to literals in A are assigned to strata based on the strata
   assigned to corresponding atoms for instants in the last maximum period. It
   is easily seen that Lemma B.5 can still be applied, since these values are
   (like z) smaller than max-time. Then, the relation on the CSD levels
   imposed by the lemma can be raised to values greater than max-time
   considering how strata for atoms with these values are assigned in Step 5.

   The proof for the other types of rules is analogous. []


To conclude the proof of Theorem 4, note that if a program is locally stratified, then it has a well-founded model, and that model is the unique stable model [Gelder et al. 1991]. Since Lemma B.6 states that [P'.sub.TAB] is locally stratified, and [P.sub.TAB] has the same stable models as [P'.sub.TAB], we can conclude that [P.sub.TAB] has a unique ground stable model. []

PROOF (THEOREM 5). By Definition 12, proving point (2) of the thesis is equivalent to proving: given [bar]t [element of] [Z.sup.+], for all authorization A, and sets of constraints [Xi], [Omega], (valid(t, A), [Xi]) [element of] [M.sub.p], with [bar]t satisfying [Xi], iff [exists]<A, [Omega]> in the [TAB.sub.EXT] computed by the algorithm, such that [bar]t satisfies [Omega].

We prove point (2) by showing that the algorithm computes a finite representation of [G.sub.P"],. Note that the second step of Algorithm 2 considers only instants less than a finite constant. This finite constant represents the maximum value that variable current_max can assume during the execution of Step 2. current_max is initially set equal to [[bar]t.sub.max] + 2 [multiplied by] [P.sub.max] and incremented by [P.sub.max] at each iteration until either it reaches the value [[bar]t.sub.max] + k [multiplied by] [P.sub.max], where k is the first positive integer such that [inverted]A<A, [Omega]> in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] or it reaches the value max-time = [[bar]t.sub.max] + k [multiplied by] [P.sub.max]. In the following, we denote with max the finite constant [[bar]t.sub.max] + k* [multiplied by] [P.sub.max], where k* is the minimum between [bar]k and k. Then, the third step of the algorithm extends the result of the second step to infinity. Therefore the thesis can be proved by these steps: we first prove that the second step of the algorithm computes a finite representation of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (Lemma B.7) and thus of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Then, we show that the extension performed by the third step of the algorithm computes [M.sub.p] .

LEMMA B.7. The second step of Algorithm 2 computes [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

PROOF (SKETCH). In the following we use P" for [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. It is easy to show that P" is locally stratified. In the proof of Theorem 4 we have given the local stratification of P'. The stratification of P" can be simply obtained assigning stratum k to a rule, if its head atom is in stratum k as constructed in the stratification of P'. Empty strata can then be collapsed. In Appendix A we have defined an algorithm, based on a fixpoint iteration method, to compute the model of a stratified [Datalog.sup.not, [equivalent]Z, [is less than] Z] program. Moreover, Theorem A. 1 guarantees that for [Datalog.sup.not, [equivalent] Z, [is less than] Z] programs in which gap-order constraints are on a finite subset of the integer the algorithm always terminates returning a nonground representation of the unique ground model of the program. The method used in Algorithm A.1 and the result of Theorem A.1 naturally extend to locally stratified [Datalog.sup.not, [equivalent] Z, [is less than] Z] programs, and therefore to program P", whose gap-order constraints are defined on the finite set {0, ..., max}. Algorithm 2 performs exactly the procedure defined by Algorithm A. 1 trying to consider multiple rules in a single step using operations on constraints. Each iteration of Step 2.2 computes [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Each iteration of the repeat-until cycle in Step 2.2 computes the fixed point of derivations for a certain stratum i. Step 2.2.a computes the set of rules applicable at a certain stratum. Note that elements in [X.sub.i], where i is the stratum, denote the authorizations/rules in TAB that correspond to clauses of [P".sub.(t [is less than or equal to] current_max)] of level i. More precisely, if (x, [Xi]) [element of] [X.sub.i], where x = [A.sub.m] or x = <[A.sub.m](OP)A>, then the set of clauses corresponding to <x, [Xi]) in [P".sub.(t [is less than or equal to] current_max)] contains at least a clause of level i. This is easily proved since the stratification of P" is done according to the output of the CSD algorithm, and [X.sub.i] is computed using the same output. After the execution of Step 2.2.a the constraint [Theta] denotes the set of rules of [P".sub.(t [is less than or equal to] current_max)] corresponding to <x, [Xi]>, which are applicable at stratum i: one for each t satisfying [Theta].

It is easy to show that for each element in [X.sub.i] the application of Steps 2.2.b and 2.2.c is equivalent to trying to fire the equivalent rules in [P".sub.(t [is less than or equal to] current_max)] using the same procedure as Algorithm A.1. The cases for explicit authorizations and WHENEVER rules are straightforward. Consider an UPON rule; that is, suppose that <x, [Xi]> = <[A.sub.m] UPON A, [Xi]>. For the sake of simplicity, we suppose that [A.sub.m] is a negative authorization. The proof for positive authorizations is analogous. Let [Xi] = {([PC.sub.1], GC), ..., ([PC.sub.k], GC)} and let A = [C.sub.1] [disjunction] ... [disjunction][C.sub.n], n [element of] [Z.sup.+] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. For each conjunct [c.sub.i] the set of rules of level i of [P".sub.(t [is less than or equal to] current_max)] corresponding to ([A.sub.m] UPON A, [Xi]) is: {valid ([bar]t, [A.sub.m]) [left arrow] [PC.sub.i]/[bar]t, GC/[bar]t, not(valid(t, [A.sub.ji])), ..., not (valid(t, [A.sub.ki])), valid(t, [A.sub.li]), ..., valid(t, [A.sub.mi])| [bar]t satisfies [Theta], ([PC.sub.i], GC) [element of] [Xi], [PC.sub.i]/[bar]t and GC/[bar]t do not contain any trivially false constraints, t [is less than or equal to] [bar]t and t satisfies [Xi]}, where [PC.sub.i]/[bar]t (resp., GC/[bar]t) denotes the conjunction of simple periodicity constraints (resp., gap-order constraints) obtained by replacing the unique temporal variable appearing in [PC.sub.i] (resp., GC) with constant [bar]t. The preceding set is equivalent to the rule: valid(t, [A.sub.m]) [left arrow] [Xi] [conjunction]* [Theta], [Xi]/t' A [conjunction]{(true, t' [is less than or equal to] t)}, not(valid(t', [A.sub.ji]), ..., not(valid(t', [A.sub.ki])), valid(t', [A.sub.li], ..., valid(t', [A.sub.mi]), where [Xi]/t' is obtained by replacing the unique temporal variable in [Xi] with t'. By construction of [Theta], the preceding rule is equivalent to: valid(t, [A.sub.m]) [left arrow] [Theta], [Xi]/t' [conjunction] {(true, t' [is less than or equal to] t)}, not(valid(t', [A.sub.ji]), ..., not(valid(t', [A.sub.ki])), valid(t', [A.sub.li], ..., valid(t', [A.sub.mi]). Thus the set of rules of level i of [P".sub.(t [is less than or equal to] current_max)] corresponding to <[A.sub.m] UPON A, [Xi]> is: {valid(t, [A.sub.m]) [left arrow] [Theta], [Xi]/t' [conjunction] {(true, t' [is less than or equal to] t)}, not(valid(t', [A.sub.ji]), ..., not(valid(t', [A.sub.ki])), valid(t', [A.sub.li]), ..., valid(t', [A.sub.mi])| i = 1, ..., n}. Step 2.2.b computes the first instant [bar]t such that (1) [bar]t satisfies [Xi] and (2) A is valid in [TAB.sub.EXT] at time t. Then it takes the intersection of [Theta] with {(true, t [is greater than or equal to] [bar]t)}. Verification is immediate that this is equivalent to evaluating the previous set of rules using Algorithm A.1. A similar proof can be obtained for ASLONGAS rules. The repeat-until cycle in Step 2.2 ends when the fixed point for the current stratum is reached. Step 2.2 ends when the fixed point for the upper stratum is reached, that is, when the model of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] has been computed. Then, Step 2 is iteratively executed till current-max reaches either the value max-time or the value [[bar]t.sub.max] + k [multiplied by] [P.sub.max], that is, till current_max reaches the value max. Hence, we can conclude the thesis. []

We are now ready to prove the theorem.

(1) (Termination). The only step that may introduce an infinite loop is Step 2. Step 2 consists of an outer repeat-until cycle that is iterated until either variable success evaluates to true or current_max reaches the value max-time, and an inner repeat-until cycle which is executed until [TAB.sub.EXT] does not change. Termination of the inner repeat-until cycle is guaranteed by using a finite constant as an upper bound in the gap-order constraints and computing [TAB.sub.EXT] only up to that value. Termination of the outer repeat-until is ensured by Lemma B.3. Hence, the algorithm terminates.

(2) We first prove that if [exists](valid(t, A), [Xi]) [element of] [M.sub.P] such that [bar]t satisfies [Xi], then [exists]<A, [Omega]) [element of] [TAB.sub.EXT] with [bar]t satisfying [Omega]. By definition of ground model, (valid(t, A), [Xi]) [element of] [M.sub.P] and [bar]t satisfies [Xi] imply valid(t, A) [element of] [G.sub.P]. By Lemma B.1, valid([bar]t, A) [element of] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and by Lemma B.2, valid([bar]t, A) [element of] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By Lemma B.7, the second step of the algorithm computes [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] Hence, if [bar]t [is less than or equal to] max, the [TAB.sub.EXT] computed by the algorithm includes an element <A, [Omega]>, such that [bar]t satisfies [Omega]. Let us suppose [bar]t [is greater than] max. By definition, max = [[bar]t.sub.max] + k* [multiplied by] [P.sub.max], where k* is the minimum between [bar]k (i.e., the finite constant defined in Lemma B.3) and k. By Lemma B.7 and by the definition of k, this implies that k* is equal to the minimum between [bar]k and the first positive integer k greater than two such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Let us first suppose max = [[bar]t.sub.max] + [bar]k [multiplied by] [P.sub.max]. Let n [element of] [Z.sup.+] be the first positive integer such that [bar]t [is less than] [[bar]t.sub.max] + n [multiplied by] [P.sub.max]. valid([bar]t, A) [element of] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] implies valid([bar]t, A) [element of] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]). Thus, valid([bar]t, A) [element of] [C.sub.n]. By Lemma B.3, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. This implies valid([bar]t - (n - [bar]k) [multiplied by] [P.sub.max], A) [element of] [C.sub.k]. Lemma B.7 ensures that the [TAB.sub.EXT] computed by the second step of the algorithm includes <A, [Omega]>, with t satisfying [Omega]', where t is the instant in [[bar]t.sub.max] + ([bar]k - 1) [multiplied by] [P.sub.max] + 1, [[bar]t.sub.max] + [bar]k [multiplied by [P.sub.max]], such that t = [bar]t - (n - [bar]k) [multiplied by] [P.sub.max]' If t satisfies [Omega]', then [exists](PC, GC) [element of] [Omega]' such that t satisfies both PC and GC. Since t [is greater than] [[bar]t.sub.max] + ([bar]k - 1) [multiplied by] [P.sub.max], and t satisfies GC, then GC is of the form: t' [is less than or equal to] t [is less than or equal to] t", where [[bar]t.sub.max] + ([bar]k - 1) [multiplied by] [P.sub.max] [is less than] t [is less than or equal to] t" [is less than or equal to] [[bar]t.sub.max] + [bar]k [multiplied by] [P.sub.max] and t' [is less than or equal to] [bar][t.sub.max]. Thus Step 3 of the algorithm replaces GC with GC' = t' [is less than or equal to] t. Thus, [bar]t = t + (n - [bar]k) [multiplied by] [P.sub.max] satisfies GC' Moreover, t satisfies PC implies that [bar]t satisfies PC.
   Hence, [exists]<A, [Omega]> [element of] [TAB.sub.EXT] such that [bar]t
   satisfies [Omega]. Let us now suppose max = [bar][t.sub.max] + k
   [multiplied by] [P.sub.max]. In Lemma B.3, we have shown that [MATHEMATICAL
   EXPRESSION NOT REPRODUCIBLE IN ASCII] implies [MATHEMATICAL EXPRESSION NOT
   REPRODUCIBLE IN ASCII], for each j [is greater than] i. Thus, valid([bar]t,
   A) [element of] [C.sub.n] implies valid([bar]t - (n - k) [multiplied by]
   [P.sub.max], A) [element of] [C.sub.k]. Hence, by the same reasoning we
   used for max = [bar][t.sub.max] + [bar]k [multiplied by] [P.sub.max] we can
   conclude the thesis.


We are left to prove that if [exists]<A,[Omega]) [element of] [TAB.sub.EXT] such that [bar]t satisfies [Omega], then [exists](valid(t, A), [Xi])) [element of] [M.sub.P] with [bar]t satisfying [Xi]. Let us first suppose [bar]t [is less than or equal to] max. By Lemma B.7, [exists](valid(t, A), [Xi]) [element of] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], such that [bar]t satisfies [Xi]'. Thus, valid(t, A) [element of] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By Lemma B.2, valid([bar]t, A) [element of] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and by Lemma B.1, valid([bar]t, A) [element of] [G.sub.P]. Therefore, [exists](valid(t, A), [Xi]) [element of] [M.sub.P] such that [bar]t satisfies [Xi].

Let us now suppose [bar]t [is greater than] max. It is easy to show that [bar]t satisfies [Omega] implies that there exists an instant t = [bar]t - n [multiplied by] [P.sub.max], n [element of] [Z.sup.+], max - [P.sub.max] [is less than] t [is less than or equal to] max, such that t satisfies [Omega]. By Lemma B.7, the second step of the algorithm computes [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Hence, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], such that t satisfies [Xi]'. Thus, valid(t, A) [element of] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Let us first suppose that max = [[bar]t.sub.max] + [bar]k [multiplied by] P.sub.max]. Hence, valid(t, A) [element of] [C.sub.[bar]k]. Thus, by Lemma B.3, valid(t, A) [element of] [C.sub.[bar]k+n], and thus valid(t, A) [element of] [G.sub.P](t [is less than or equal to] [[bar]t.sub.max] + ([bar]k + n) [multiplied by] [P.sub.max]). Then, by Lemma B.2 valid([bar]t, A) [element of] [G.sub.P](t [is less than or equal to] [bar][t.sub.max] + ([bar]k+n) [multiplied by] [P.sub.max]). It is sufficient to apply Lemma B.1 to conclude the thesis. Suppose now that max = [bar][t.sub.max] + k [multiplied by] [P.sub.max]. In Lemma B.3, we have shown that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] implies [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], for each j [is greater than] i. Thus, valid(i, A) [element of] [C.sub.k] implies valid([bar]t, A) [element of] [C.sub.k+n], since [bar]t = t + n [multiplied by] [P.sub.max]. Hence, by the same reasoning that we used for max = [[bar]t.sub.max] + [bar]k [multiplied by] [P.sub.max], we can conclude the thesis. []

This article extends the previous work by the authors, which appeared in IEEE Transactions on Knowledge and Data Engineering 8, 1, 67-80, [C]1996, The Institute of Electrical and Electronics Engineers, Inc.

Authors' address: Dipartimento di Scienze dell'Informazione, Universita di Milano, via Comelico 39, 1-20135 Milano, Italy; email: <{bertino,bettini,ferrarie,samarati}@dsi.unimi.it.>. Permission to make digital/hard copy of part or all of this work for personal or classroom use is granted without fee provided that the copies are not made or distributed for profit or commercial advantage, the copyright notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee.

ELISA BERTINO, CLAUDIO BETTINI, ELENA FERRARI and PIERANGELA SAMARATI

University, di Milano
COPYRIGHT 1998 Association for Computing Machinery, Inc.
No portion of this article can be reproduced without the express written permission from the copyright holder.
Copyright 1998 Gale, Cengage Learning. All rights reserved.

Article Details
Printer friendly Cite/link Email Feedback
Author:BERTINO, ELISA; BETTINI, CLAUDIO; FERRARI, ELENA; SAMARATI, PIERANGELA
Publication:ACM Transactions on Database Systems
Date:Sep 1, 1998
Words:31056
Previous Article:Corrigenda.
Next Article:Conceptual Schema Analysis: Techniques and Applications.
Topics:

Terms of use | Privacy policy | Copyright © 2020 Farlex, Inc. | Feedback | For webmasters