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.
Roberto Gorrieri (2019). Axiomatizing Team Equivalence for Finite-State Machines. Heidelberg : Springer [10.1007/978-3-030-31175-9_2].
Axiomatizing Team Equivalence for Finite-State Machines
Roberto Gorrieri
2019
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
