next up previous
Next: Representing processes, constraints, and Up: Logical Language and Model Previous: Logical Language and Model

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 si. 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 si such that $i < \min$ or $i > \max$, siattributes false to x.

Intuitively, a model is the trace of a possible instance of a process. For each time instant i, the state si 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 st of the model m, satisfies the formula $\alpha$. Sometimes in this paper we will represent the state st of the model m as m|t.

We will now add a set of modal operators to deal with time:

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


next up previous
Next: Representing processes, constraints, and Up: Logical Language and Model Previous: Logical Language and Model
Jacques Wainer
2000-01-06