Partially ordered computations are well known in the literature [L, Mz, KP, etc.] but we need to define our own version of that notion for our purposes here. We restrict attention to the case where moves are atomic and we use global states. Non-atomic moves have been explored in [BGR]. A simple notion of runs in [GM] does not use global states.
Let us recall some well known notions. A poset is a partially
ordered set. An initial segment of a poset P is a substructure
X of P such that if
x X
and
y < x
in
P then
y
X.
Since X is a substructure,
y < x
in
X if and only if
y < x
in
P whenever
x,y
X.
A linearization of a poset P is a linearly ordered
set P'
with the
same elements such that if
x < y
in
P then
x < y
in
P'
.