Figuring out what to do next

The logic representation proposed above is not strong enough to determine what activity should be performed next. An expression such as

$$b\!\!\downarrow\rightarrow (\stackrel{\rightarrow}{\Diamond}\!d) \land (\stackrel{\rightarrow}{\Diamond}\!c)$$ (19)

does not state that d or c starts just after the end of b; it states that d and c will eventually start after the end of b. In some ways d and c are enabled, in the sense that they could start as soon as bended, but the may start any time in the future.

The logic itself contain operators to represent that d and c must start imediatelly after b ends. This can be expresses as $b\!\!\downarrow\rightarrow {\bf N}( d \land c)$. But this representation does not allow for the flexibility that the expression 19 allow: dand c can start at different times, there can be any (consistent) activity performed between the end of b and the start of d or c, and so on.

In order to figure out from the formulas that express the procedures, constraints and policies, which activities are enabled, without changing the formulas, one need to define a new, stronger logic. That logic is defined below.