Axiomatizing Team Equivalence for Finite-State Machines

Finite-state machines, a simple class of finite Petri nets, were equipped in [11] with a truly concurrent, bisimulation-based, behavioral equivalence, called team equivalence, which conservatively extends bisimulation equivalence on labeled transition systems and which is checked in a distributed manner, without necessarily building a global model of the overall behavior. The process algebra CFM [10] is expressive enough to represent all and only the finite-state machines, up to net isomorphism. Here we first prove that this equivalence is a congruence for the operators of CFM, then we show some algebraic properties of team equivalence and, finally, we provide a finite, sound and complete, axiomatization for team equivalence over CFM.