Axiomatizing weighted synchronization trees and weighted bisimilarity

We consider regular synchronization trees weighted over a semiring and provide sound and complete axiomatizations of these trees and their weighted bisimulation equivalence classes. We prove that they can be both axiomatized by a finite number of identities relatively to the general axioms of the fixed point operation captured by the notion of iteration theories. We present infinite equational and finite quasi-equational axiomatizations.