An algebra of labelled nondeterministic processes

A new calculus of labelled nondeterministic processes AFLP2 is proposed which is an extension of the known calculus AFP2 by labelling function. The denotational and operational semantics and complete axiomatization of the semantic equivalence are presented. The interrelation of net equivalences from with equivalences of the algebra (semantic and observational) is considered. Analogs of the net equivalences are defined in AFLP2, allowing one to consider the processes specified by formulas of the algebra at different levels of abstraction.