Next: Real-time Computations
Up: Partially Ordered Runs
Previous: Partially Ordered Runs
For simplicity, we restrict attention to pure runs and deterministic
agents. A run 
of a distributed ealgebra A can be
defined as a triple 
satisfying the following conditions
1-4.
- 1.
-
M is a partially ordered set, where all sets
are
finite.
Elements of M represent moves made by various agents during the
run. If y < x
then x starts when y is already finished; that explains
why the set is finite.
- 2.
- A is a function on M such that every nonempty
set {x : A(x) = a}
is linearly ordered.
A(x)
is the agent performing move x . The moves of any single agent are
supposed to be linearly ordered.
- 3.
-
assigns a state of A to the empty set and each initial segment
of M ; 
is an initial state.
is the result of performing all moves in X .
- 4.
- The coherence condition: If x is a maximal element in a finite
initial segment X of M and
Y = X - {x},
, then
A(x)
is an agent in
and is obtained from by firing
A(x)
at .
Intuitively, a run can be seen as the common part of histories of the same
computation recorded by various observers. We hope to address this issue
elsewhere.
If agents are not necessarily deterministic, we have to define moves as
state transformers and make the coherence condition more precise:
- 4'
- If x is a maximal element in a finite initial segment X of
M and
Y = X - {x},
then
A(x)
is an
agent in , x is a move of A(x)
and is obtained from by performing x at
.
A run 
is an initial segment of a run if (i) the move
poset of is an initial segment of the move poset of and
(ii) the agent and state functions of are restrictions of those in
. A run is a linearization of if the move
poset of is a linearization of that of , the agent function
of is that of , and the state function of is a
restriction of that of . Linearizations are sequential runs. A
state S of is reachable in a run if it belongs to the
range of the state function of .
Corollary 6.1. All linearizations of the same finite
initial segment of have the
same final state.
Corollary 6.2. A property holds in every reachable state
of a run if any only if it
holds in every reachable state of every linearization of
.
Next: Real-time Computations
Up: Partially Ordered Runs
Previous: Partially Ordered Runs