Graph transitions represent an extension of the DPO approach to graph transformation for
the specification of reactive systems. In this paper, we develop the theory of concurrency for
graph transitions. In particular, we prove a local Church–Rosser theorem and define a
notion of shift-equivalence that allows us to represent both intra-concurrency (within the
specified subsystem) and inter-concurrency (between subsystem and environment). Via an
implementation of transitions in terms of DPO transformations with context rules, a second,
more restrictive notion of equivalence is defined that captures, in addition, the
extra-concurrency (between operations of the environment). As a running example and
motivation, we show how the concepts of this paper provide a formal model for distributed
information systems.
Shift equivalence in the generalized factor order
