In: Baeten, J.C.M.; et al.: Lecture Notes in Computer Science, Vol. 458; CONCUR'90, Theories of Concurrency: Unification and Extension. (Conference, 1990, Amsterdam, The Netherlands), pages 166-181. Berlin, Germany: Springer-Verlag, 1990.
Abstract: It is shown that each live and safe free-choice system without frozen token can be reduced either to a live and safe marked T-graph (marked graph) or to a live and safe marked P-graph (state machine). The four proposed reduction rules are purely local and preserve the behavioural properties in both directions. Hence the method can be used for both, effective analysis and correct design. The class of systems which can be reduced can be characterized without using the reduction rules by their P- and T-components.
Keywords: well-behaved concurrent system; free-choice system (without) frozen token; T-component; P-component.