Behavioral equivalences of weighted transition systems

We offer sound and complete axiomatizations of both the bisimulation equivalence and the trace equivalence of finite state transition systems, weighted over a semiring. We provide both infinite equational and finite quasi-equational axiomatizations. In the case when the semiring is the boolean semiring, our results specialize to classical axiomatizations of behavioral equivalences of unweighted systems