next up previous
Next: Modes of use of Up: Figuring out what to Previous: Figuring out what to

Extension of the logic

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

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

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:

\begin{displaymath}\hbox{for all~} m \in X,\; m, \hat{t}\models {\bf N}p
\end{displaymath} (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

\begin{displaymath}\Box F, wc, \hat{t}\;\rhd\;p
\end{displaymath} (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.


next up previous
Next: Modes of use of Up: Figuring out what to Previous: Figuring out what to
Jacques Wainer
2000-01-06