Consistency between model and case

Once the process specifications, constraints, and policies are coded as logic expressions, we must determine when a case is in agreement with these process specifications, constraints, and policies. A workcase can be seen as a subsequence of a model. If the current time is $\hat{t}$, then the workcase wc is a sequence $\langle \ldots s_{-1}, s_0, s_1, \ldots s_{\hat{t}} \rangle$. We will denote the state s_i of the workcase wc as wc|i.

We will call a model m a continuation of a workcase wc, after time $\hat{t}$, if for all $i \leq \hat{t}$, m|i = wc|i. A continuation is a model that agrees with the workcase up to time $\hat{t}$.

We will collect the logical formulas that state the policies, constraints, and processes in a single formula F, which can be thought as the conjunction of all the individual formulas.

A workcase wc is consistent with the set of procedures and policies F, up to time $\hat{t}$, if there exists at least one model m that is a continuation of wc after time $\hat{t}$, such that $m, \hat{t}\models \Box F$. That is the workcase is consistent with the set of policies and procedures if there is at least one possible continuation of that workcase that satisfy the formulas in F for all times.

We denote that a workcase wc is consistent up to time $\hat{t}$ with the set F as

$$wc, \hat{t}\;\sim\;F$$ (18)

For example, let us suppose that the case developed as below, where the top row refer to states and the bottom row lists the propositions that are true in each state.

$$\begin{array}{ccccccccccccc} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & ... ... & a & a & & b & n_1,b & b & & & m_1 & & c & c,d \end{array}$$

The workcase, up to time t=12 is consistent with the set of formulas 1-17.