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.
2019
The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday
14
32
Roberto Gorrieri (2019). Axiomatizing Team Equivalence for Finite-State Machines. Heidelberg : Springer [10.1007/978-3-030-31175-9_2].
Roberto Gorrieri
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/714795
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 2
social impact