Extension of the logic

We will define that a model m₁ is a compression of a model m₂after time $\hat{t}$, represented as $m_1 <_{\hat{t}} m_2$ if:

• m₁|i = m₂|i for $i \leq \hat{t}$.
• for all propositional symbols in $x \in A$, $m_2, t_2 \models x\!\!\uparrow$ if and only if $m_1, t_1 \models x\!\!\uparrow$ and if $t_2 > \hat{t}$ then $\hat{t}< t_1 \leq t_2$

Intuitively, a model m₁ is a compression of m₂ after $\hat{t}$ if they agree in everything up to time t, and after time $\hat{t}$ all activities in m₁ start before (or at the same time) as the activities in m₂.

The relation $<_{\hat{t}}$ is reflective, transitive, and antisymmetric. We will say that a model m' is minimal (in relation to $<_{\hat{t}}$) in a set M if there is no other model in M that is a compression of m' and that is not m' itself. Let us call X the set of all minimal models of all continuations of the workcase, after the current time $\hat{t}$, that are consistent with F. The activities that can start immediately after time $\hat{t}$, are the activities $p \in A$ such that:

$$\hbox{for all~} m \in X,\; m, \hat{t}\models {\bf N}p$$ (20)

Intuitively, the models in X are the continuations of the case after $\hat{t}$ that are consistent with F, and for which the start of all activities is anticipated as much as possible. If an activity p is enabled, it means it could start in the next moment, and therefore, in minimal models they will indeed start at the next moment. The method of defining a partial order among models and selecting only the minimal one is the essence of the preferential non-monotonic logics [12].

We will denote the fact that for all $m \in X, m, \hat{t}\models {\bf N}p$ as

$$\Box F, wc, \hat{t}\;\rhd\;p$$ (21)

that is, that given the workcase wc at time $\hat{t}$ and the procedures and policies $\Box F$, p can start in the next moment.