Università di Pisa, Dipartimento di Informatica, PhD Thesis TD--4/90, 146 pp. pages, 1990.
Abstract: The author analyzes concurrency models from a logical standpoint and shows that the behavioural equivalences in the models can be completely characterized by the equivalences induced by the logics --- Petri nets can be viewed as graphs with algebraic structure: they are simply graphs equipped with a commutative monoidal operation, expressing parallel composition of states and transitions. The free category generated by the graph is a symmetric monoidal category. This framework is used to show that an elementary transition involving the use of several resources may be decomposed into a sequence of more elementary steps involving just one resource. This decompositon is proved conservative with respect to successful computations.
Keywords: behavioural equivalence; symmetric monoidal category; decomposition (of) resources; concurrency models, (unifying).