Temporal aspects of logical procedure definiton

hfon Systems Vol. 5. pp. 167-187 @ Pergamon Press Ltd., IBO. Printed in Great Britain

TEMPORAL ASPECTS OF LOGICAL PROCEDURE DEFINITION AMILCARSERNADAS London Schoolof Economics,Room S.110, Houghton Street, London WCZA 2AE, England (Received10May 1979;in revised

form10 December

1979)

Abstract-This paper discusses the inclusion of time in a message-oriented relational model of information systems order to achieve memory independent specifications. The concept of memory independence is reviewed and several systems languages are analysed from this point of view and also in other aspects of their temporal properties. The concept of temporal database is formally introduced and a special modal tense logic is developed to deal with it. This logic is extended with a transition imperative logic to allow the specification of processes within the information system at a very high level. The information system is seen as composed of these concurrent autonomous processes that communicate through the temporal database divided in event and state assertions. in

NOTATION

a before (exclusive) 4 before (inclusive) A within

Classical logic symbols

V 3 A v j (j =

for all (universal quantifier symbol) exists at least one (existential quantifier symbol) and (conjunction) or (disjunction) no (negation) implies (implication) is equivalent (equivalence) is equal (identify predicate)

I at FIRST (a) first period of a truth LAST (a) nth(a)

last period of a truth nth period of a truth

Messagelprocess diagram symbols 0 process

V 0 + * CI -

Usual symbols for arithmetic operations (functions in the logic): + ,- ,x ,I, etc.

event relation state relation trigger transitions reference

Usual symbols for order predicates:

Extensions E belongs (membership predicate) C is included (inclusion predicate) x summation i integration convolution operators # cardinal

max min U n \ {x:a) [Xl7x21

1. INTRODUCTION

and 2

maximum minimum i union intersection complementation set of x satisfying a = {x:x, 5 x I x2}

Transition logic symbols B for all in paralleldo (parallelquantifiersymbol)

Y for all in sequence do (sequential quantifier symbol) E false/true transition predicate 3 true/false transition predicate 9 delay operator Tense logic symbols d always (in the past and now)

dp always in the past ‘rp ever (in the past or now) P ever in the past dt always during t %I ever during 1 [a]t a true at t [a]tAGO a true at t ago D after (exclusive) @ after (inclusive)

A good introduction to the problem of representing time in a database system is found in Bubenko[l]. Deeper problems arise in the field of systems specifications related to the concept of memory independence. A model of an information system is said to achieve memory independence if it allows the specification of all processes in the system without any assumption concerning which messages are stored in the current state of the system that refer to the past. This is a desirable feature of any systems language or model because it allows the delaying of the decision concerning what to store in files until the later stage of physical implementation design. Only at that stage is a cost/benefit analysis possible to compare the different solutions. This concept of memory independence (not to be confused with the weaker concept of data independence) was introduced by Teichroew[2] and Grindleyl31, both authors working on systems languages, respectively PSL and SYSTEMATICS. The former puts clearly that some piece of information must be stored only if it may be used at a time different of the instant of its production; another solution is to derive it when necessary. Between these two options the choice should come from physical design criteria, not applicable at the stage of the logical statement of systems requirements or systems specification. 167

168

A. SERNADAS

Several solutions to this problem will be analysed, including the simplest (but worst) known as the current view model. The results of this analysis show the need for a temporal model of the information system database (defined informally as the set of messages in thesystem). This model will be based on a specially developed modal tense logic. For this purpose the work made by the modal logicians in the area of time modelling is reviewed and extended in Section 3 below. A message-oriented model of the information system is assumed which allows the use of relational languages. Several timeless relational models are analysed in order to justify the multitype interpretation approach chosen herein. A predicate-oriented process specification language is introduced in Section 4 below. This language is a temporal version of the transition logic introduced by the author[4] to define DMTL2. (Dynamic MultiType Logic with higher-order capabilities). The information system is modelled by a network of concurrent autonomous processes that exchange messages amongst themselves and with the environment through the information system temporal database. These processes may only change the current state of the system and are aware of the previous states which they may refer to for decision making (but not change). The reference to these past versions of the temporal database is made with the tense logic defined in Section 3. This specification language is memory independent in the sense that nothing is assumed concerning how and what information from the past is actually stored in the current database. This temporal model of the information system database allows the useful distinction between events and state assertions. However, it will be shown that Grindley’s event triggered specification of procedures is not complete and the full process view introduced by the author[4] for DMTLZ is retained in DMTLT (Dynamic MultiType Logic with Time). The specification of a process corresponds to the specification of a set of event generation rules. Some events exist by themselves (such as the issuing of output messages) and others correspond to state transitions (such as the update of a stock level). The specification of the information system at the level of messages and processes is close to the approach taken by Grindley in SYSTEMATICS; another solution would be the direct specification of the object system (substantive level), as proposed by Stamper [5] for LEGOLZ. From the point of view of time modelling these two solutions have their counterparts in tense logic, as will be shown in 3.2 below. The message/process level was chosen as a matter of the author’s preferences; no doubt systems languages are needed at both levels and another field of research would be to link specifications at different levels. This choice has little influence on the syntax of a predicate oriented systems language because it affects mainly the semantics of such a language. Although the objective of this paper is to develop a memory independent model for the information system, leading to a suitable process specification language, the

modal tense logic chosen herein might also be used for database querying at a higher level than that achieved by current database languages. Indeed, this higher level would allow the user to consult an historical database without being concerned with the way the historical facts are represented in the current database. This seems to imply that the concepts of memory independence and tense logic deserve the attention of those interested in relational databases and their predicate-oriented languages. As an illustration to this argument see Mason[6], although in a relational algebra framework. 2. TIMELESS MODELS

2.1 The relational database and logic The definition of a “non-procedural” language for systems specification presupposes the introduction of a suitable model for the memory component of the information system (the database). A rather successful model that achieves a high degree of data independence is the relational model introduced by Codd[7]. This model has been extensively studied from several points of view. Herein its main interest comes from tb possibility of using a predicate calculus to refer to the database composed of relations: each relation is assigned to a predicate in the logic. For implementing this idea two main approaches are possible: (a) the axiomatic approach that corresponds to the inclusion of the database contents as axioms in the logic; (b) the interpretation approach that corresponds to using the database contents as an interpretation structure of the logic. For a comparative study of these two solutions see Nicolas[8]. There it is argued that the latter approach is more adequate. Both solutions allow the introduction of a virtual database (besides the object or extensional database discussed so far) composed of relations defined through general laws that take the form of axioms and may involve recursion. Integrity constraints may also take this form. Taking either of the two approaches, the chosen set of axioms and derivation rules should define a set of theses that is precisely the set of valid well formed formulae. Theses are axioms or formulae derived from them (using the derivation rules). Valid formulae are formulae true for every interpretation. In the second approach this means that valid formulae are true for every database state. In either case a sound and complete logic should be defined in order to avoid deriving false theses (for some interpretation) or being unable to derive formulae true for every interpretation. Moreover the chosen logic should contain the standard predicate calculus (in the sense that all standard theses are theses of the applied logic). This would ensure the validity of standard results that might be useful. This objective is achieved by including in the axiomatic definition of the applied logic a basis for the standard predicate calculus and avoiding any inconsistencies (which means that each new thesis should not be provable as false in that basis). These considerations seem to have been disregarded as such in the literature, except in what concerns the problem of the closed world assump-

Temporalaspects of logicalproceduredefinition tion (see for example Nicholas~8J and Reiterb]). It is beyond the scope of this paper to follow this problem any further. However, it is important to stress that it is possible to avoid it completely by taking the interpretation approach and defining the virtual relations not through-axioms but through expressions that are evaluated in terms of the object predicates. It seems that nothing is lost with this simple solution since even recursion is possible. Taking into consideration this argument and those presented by Nicolas (see supra cila), the interpretation approach will be chosen in this paper which completely avoids any deductive method in the interpretation of formulae. The chosen axioms and derivation rules will describe only universally~ valid propositions (true for every interpretation or database state). Their only interest is to derive general rules that may be used for example to simplify queries. So, a standard axiomatic basis may be used for the predicate calculus to access the database. Following this solution, a choice must be made between two models: B. I Codd’s model (Codd [7, lo]) corresponding to the introduction of a special uni-sorted first order logic with range predicates representing the database relations; B.2 ~mffj~-o~e#ted model (Lacroix[ll], Sernadas (121)corresponding to the use of a standard many-sorted first order logic (Enderton [ 131)where sorts are assigned to domains and predicates to relations. In order to avoid meaningless formulae, the former model has complex rules for defining the allowed well formed formulae. The latter approach is simpler from this point of view and has several advantages (see supru cita and Sernadas[4]) over the relational calculus proposed by Codd. From a theoretical point of view the multitype model (using Computing Science terminology, since the concept of sort corresponds to the concept of type) has the important advantage of leading to a predicate calculus for which the relational database constitutes an interpretation structure in the sense of Mathematical Logic. The same desideratum might be achieved with a unisorted approach although that is not the case of the special Codd’s relational calculus. However, the multitype model allows a closer description of the database domains and is easily extended to include higher order capabilities that are needed to deal, for example, with repeating groups. In conclusion, the adoption of an interpretation multitype model for the relational database is justified by the des~bility of using sanded logical statures as much as possible. Then well known axiomatics can be exploited to prove the equivalence of queries, or any other applications, where universally valid formulae are useful. The relevance of logical models of the relational database for the problem of systems specification follows and Section 3 below discusses the inclusion of time in the chosen logic. 2.2 Timeless systems specification Using a message-oriented model of information sys-

169

terns (as that intr~uced by the author~4]), it is possibte to develop a predi~ate~~ent~ language for systems specification. This language allows the specification of concurrent, autonomous processes at a very high level. Processes exchange messages amongst themselves and with the environment through a relational database. To each message type corresponds, in general, a relation in the database. These relations are not necessarily normalized because they may contain input/output messages which in many cases contain repeating groups. The database at the current time contains all valid messages at that instant. The past messages are forgotten unless explicitly stored in the current database. This approach corresponds to a current view of the time problem that leads to a high degree of memory dependence in the sense that the systems analyst cannot avoid specifying how and what is to be stored in the current database from the past. The great advantage of this approach is its relative simplicity. The dynamic evolution of the database imposed by the activity of the processes in the system (and the environment) is specified using an extension to the multitype logic. This extension constitutes a transition logic whose executional semantics may be defined formally (see Sernadas[4,141). Therein a process specification language (DMTLZ) based on this current view is intr~uced. For an illustration of the capabilities of DMTL2, consider an order entry process that receives incoming orders. For each product (in parallel) it sequentially selects each order of that product; if the respective stock is sufficient it fulfills the order by issuing a delivery inst~ction and updating the stock level and if the stock is not sufficient it creates a backorder; in either case the process deletes the processed order from its input file. Note that the only sequencing assumed is implied by the logic of the problem itself and not on the grounds of implementation criteria. DMTL2 achieves a high degree of non-procedurality from this and other points of view (see supru cita). 9prod, q, S&I ORDER(n, prod, q) ST~K(prod,

s)

* 01, prod, q) 3 ORDER (s 2 qj(n, prod, q) GDELIVERY (prod, s - q) E STOCK(prod) ELSE (n, prod, q) ~BACKORDER) The semantics of the dynamic logic symbols (9, Y: E, 3 ) are described below in Section 4. For the moment it is sufficient to recognize respectively the parallel universal quant~er (4p), the sequentiai universal quantifier (3, the insertion transition predicate (E) and the deletion transition predicate ( 3 ). This language represented an improvement over all earlier attempts from the non-procedurality point of

A. SERNADAS

170

view. The main purpose of Section 4 below is to develop a temporal version of this language retaining its nonprocedural properties and achieving a high level of memory independence. Note that the current view is pragmati~~ly complete in what concerns references to historical information. As Bubenko [ I] shows, it is possible to include in the current database a finite number of messages that are sufficient to describe the complete behaviour of the system in the past. Several solutions are always possible to achieve such a representation. The choice between them should be left to the implementation designer and not arbitrarily made by the systems analyst. With this serious disadvantage, the current view offers on the other hand simplicity. This is probably the main reason why so many systems languages were proposed taking the current view approach. Examples of these are Information Algebra (CODASYL[lS]), BDL (Leavenworthll61, Hammer [ 171)and STREMA (Clark [ 18,191). This type of systems specification could be referred to as ~~~e~e~~~pecj~cu~i~~since time is not dealt with directly in the underlying model of the information system. Against this solution see Grindley [3] and Teichroew [2]; lately Stamper [20] joins the group, although at the substantive level. Both Grindley and Stamper attempt to find a better model including time. These two attempts are briefly reviewed at the beginning of the next section. The experience gained from them will be used later on to choose a logic model for time. 3. TEMPORALMODELS

3.1 Early attempts Several related aspects are important in the treatment of time for systems languages, concerning what is recalled from the past, when procedures are executed and how their synchronization is achieved: (a) begot independence: as already intr~uced, this desirable feature corresponds to the possibility of recalling the past without being involved in its actual representation in the current state of the system; (b) Non-update: avoiding update specifications (and using instead integrity rules over a temporal database for the same purpose) is a sufficient condition to achieve memory independence; however it wig be shown below that it is possible to use update s~~ifi~ations and still achieve memory independence; (c) Priuileged present time: as opposed to the substantive temporal rule approach; the former corresponds to the specification of the system by transitions executed at the current time (with eventual references to the past but not changing it) and it is well suited to the message/process level of the specification; the latter corresponds to the specification of the system by integrity constraints to be satisfied trout all time; (d) Temporal database: in opposition to the current view introduced in the previous section; the temporal database is the family of database states through time; without it, memory independence is impossible; (e) Events and triggers: events are messages instantaneously true and triggers are events used to specify run

times of procedures; events are useful to specify when certain transitions should happen and are the only way to communicate with the environment; naturally, the use of events implies the temporal database approach, unless the concept of event is accepted as a primitive one and, for this reason, left undefined. The logical relationships between these approaches to time modelling are summarized in the two following networks of implications:

No-update

-

Events 8r triggers

Current database

Memory indepen~n~e -

1 Temporal database

-

Memory dependence

\ 4

Privileged present time

The arrows in this diagram indicate implications. For example, the use of a strictly current database implies the use of updates to specify changes, the implicit reference to a privileged current instant and a high level of memory dependence. The current model discussed in the previous section is characterized by: -current database: -update; -privileged present time; -memory dependence. Much more sophisticated models were proposed related to the two following systems languages: SYS~~~A~ZC~ (Grindley [3,21,22]) This language is based on a behavioural model of the information system (with input signals, action answers and feedback) that corresponds loosely to the message process level of specification. Processes (subsystems in Grindley’s terminolo~) are triggered off by certain input events (triggers). An important part of any s~cifi~ation with SYSTEMATICS is the statement of the triggering conditions for the production of each set of outputs. Grindley claims that the concept of updating is at the level of the implementation strategy and should be avoided at the specification stage in order to achieve memory independence. So SYSTEMATICS is based on a strict view of the system specified through inpu~output rules. The update of state assertions (such as the stock Ievel) is “avoided“ as follows: STOCK = X REPLENISHMENTS - Z DISPATCHES which corresponds to an integrity constraint on the underlying temporal database, although this concept is not explicitly used by Grindley. This integrity constraint is

Temporalaspects of logicalproceduredefinition better specified by: STOCK, = I: REPLINISHMENT,,I’ f*l is another time set term interpreted as the interval between tl and t2. Similar expressions may be used to build open intervals. In the expressions above t is a variable, and t, and t2 are terms all of type time.

A. SERNADAS

178

Useful constants to be included in the language might be: -THISYEAR; -THISWEEK; -1980; -LASTMONTH;

etc.

Note that in the examples above some are moving time constants (e.g. THISWEEK) whose interpretation varies with the Z, E Z considered. Others are fixed time constants (e.g. 1980) whose interpretation is the same through all I, E I. No attempt is made here to define the micro-syntax rules governing the writing of constants, variables and names in general. However the macro-syntax is completely defined by the rules specifying the building of wlfs in the logic. Another way to obtain time set terms is to use any of the following operators: -After (inclusive) ------------. p, -After (exclusive) ------------ D -Before (inclusive) ----------. ,a -Before (exclusive) ---------- 4 -Within _______ _____ _____________. A -At ________ ______ ____ _____________ ( If a is a wtI and 13is any of the time operators above then

is a time set term. Also if 1 is any time term, then

are time set terms of straightforward interpretation. Assuming that a is a wtI then: -la is interpreted in L, as the time set A such that for everytEA:tst,andaistrueinZ,. -~a is interpreted in Z,, as the time set A such that for every t E A: t s t, and 8(a) is true in I,. -da is interpreted in I,, as the time set A such that for every t E A: t I t, and Sa(- (a)) is true in I,. Assuming the operator A defined, then by definition,

Formally, Aa in I,, is interpreted as the time set A such that for all t E A: -t5t,; -8(a) is true in I,; -and there is a t’ such that t 5 t’ 5 t, and a is true in Z1’. The existence of time set terms allows the introduction of restricted temporal quantifications. If t is a time set term and a is a wtI, then both: &(a)-always during t, a is true; It(a)-ever during t, a is true; are well formed formulae. Naturally,

and it is necessary to interpret only one of them. For example,

will be true in a Z, E Z iff for every Z,.E Z such that t’ E t (note that t is interpreted in C) a is true in I,,. Note also that t’ E 1 means that I,, is seen by It where 1 is evaluated. These restricted quantifications do not behave so well as the unrestricted ones as can easily be verified. No attempt is made here to extend the axiomatic introduced in 3.3.1 above to describe the properties of these operators. However some universally valid formulae may be informally indicated: -&(a A~)&&(a) A5&(P); --JBtr U t2(a@&(a) h &J&(a); --8t(a v p)&Yl(a) v st(& --%t, U t2(a)tStl(a) v 8&(a). Another form of restricted time quantification is obtained by introducing: SQ”and 8’ interpreted as always and ever in the past respectively. The past is the time set including all elements of T except the current instant. Other interesting time set generation operators might be found useful, such as:

and

FIRST

(a);

LAST(a); and in general: The within operator A is informally interpreted as follows:

is the time interval that goes from the“‘first” instant in which a is true until the “last” instant in which Q is still true. Note that such instants may not exist at all.

nth (a) where n is any term of type positive integer. For example, the interpretation of FIRST(a) would be as follows: -FIRST(a) in I,, is the time set A such that, for all SEA, t