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 s_{i}. 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 s_{i} such that or , s_{i}attributes false to x.
Intuitively, a model is the trace of a possible instance of a process. For each time instant i, the state s_{i} 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 s_{t} of the model m, satisfies the formula . Sometimes in this paper we will represent the state s_{t} of the model m as m|t.
We will now add a set of modal operators to deal with time: