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 $m = \langle \ldots s_{-2}, s_{-1}, s_0, s_1, s_2, \ldots \rangle$ 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 $\min$ and $\max$ such that for all propositional symbols $x \in P$, and for all states s_i such that $i < \min$ or $i > \max$, s_iattributes 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 ($\max$), 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 $\alpha$, denoted as $m,t \models \alpha$ if the state s_t of the model m, satisfies the formula $\alpha$. 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:

• the symbol ${\bf N}$ refer to the next instant of time. That is $m,t \models {\bf N}\alpha$ if $m , t+1 \models \alpha$.
• the symbol ${\bf B}$ refer to the previous instant of time. That is $m,t \models {\bf B}\alpha$ if $m , t-1 \models \alpha$.
• $\stackrel{\rightarrow}{\Diamond}\!$ refers to some time in the future. $m,t \models \stackrel{\rightarrow}{\Diamond}\! \alpha$ if there is a i > t such that $m, i \models \alpha$
• $\stackrel{\leftarrow}{\Diamond}\!$ refers to some time in the past, that is $m,t \models \stackrel{\leftarrow}{\Diamond}\! \alpha$ if there is a i < t such that $m, i \models \alpha$
• $\Box$ refers to all times (past and future), that is $m,t \models \Box\alpha$ if for all i such that $m, i \models \alpha$

In order to simplify the formulas we will define the abbreviations:

• for each $x \in A$, $x\!\!\uparrow\equiv {\bf B}\neg x \land x$, that is $x\!\!\uparrow$ states that the activity x is starting now.
• for each $x \in A$, $x\!\!\downarrow\equiv {\bf B}x \land \neg x$, that is $x\!\!\downarrow$ states that the activity x has just ended.

• ${\bf N}_n \alpha \equiv {\bf N}{\bf N}\ldots {\bf N}\alpha$, that is that $\alpha$ will be true in n moments in the future.

• $\stackrel{\rightarrow}{\Diamond_{n}}\! \alpha \equiv {\bf N}_{n-1} \stackrel{\rightarrow}{\Diamond}\!\alpha$ that is $\stackrel{\rightarrow}{\Diamond_{n}}\! \alpha$ states that $\alpha$ will be true in at least n moments. Similarly for $\stackrel{\leftarrow}{\Diamond_{n}}\!$.
• extending the notation above, we will define $\stackrel{\rightarrow}{\Diamond_{0}}\! \alpha$ as $\alpha \lor \stackrel{\rightarrow}{\Diamond}\!\alpha$, that is, either $\alpha$ is true now or it will be true in the future. Similarly for $\stackrel{\leftarrow}{\Diamond_{0}}\!$.