We will use a linear, discrete, modal temporal logic  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: