Next: Representing processes, constraints, and Up: Logical Language and Model Previous: Logical Language and Model

## Logic

We will use a linear, discrete, modal temporal logic [5] as representation tool. In this logic time is discrete, but the value of the unit of time is unimportant. We will define a set of propositional symbols P; an important subset of P is the set Aof propositional symbols that represent the activities. The symbols in P - A will, for the purpose of this paper, be used only as auxiliary propositions for a particular representational problem. In the future, propositions in P- A may represent external events, conditions on the data, and so on.

A model is a sequence of states si. Each state attributes true or false to each propositional symbol in P. We will also demand that for each model, there should exist two integers and such that for all propositional symbols , and for all states si such that or , siattributes false to x.

Intuitively, a model is the trace of a possible instance of a process. For each time instant i, the state si expresses the activities that are being executed (those that are true in the state). And after some long enough time (), all activities would have been executed. Activities can be executed in parallel (that is there may be more than one activity true in the state) and activities can be repeated (that is, a propositional symbol can be true in a state, falsein a later state, and then true again in a latter state).

We say that a model m and a time t satisfy a propositional formula , denoted as if the state st of the model m, satisfies the formula . Sometimes in this paper we will represent the state st of the model m as m|t.

We will now add a set of modal operators to deal with time:

• the symbol refer to the next instant of time. That is if .
• the symbol refer to the previous instant of time. That is if .
• refers to some time in the future. if there is a i > t such that
• refers to some time in the past, that is if there is a i < t such that
• refers to all times (past and future), that is if for all i such that
In order to simplify the formulas we will define the abbreviations:
• for each , , that is states that the activity x is starting now.
• for each , , that is states that the activity x has just ended.

• , that is that will be true in n moments in the future.

• that is states that will be true in at least n moments. Similarly for .
• extending the notation above, we will define as , that is, either is true now or it will be true in the future. Similarly for .

Next: Representing processes, constraints, and Up: Logical Language and Model Previous: Logical Language and Model
Jacques Wainer
2000-01-06