Team equivalences for finite-state machines with silent moves
| Autor: | Roberto Gorrieri |
|---|---|
| Přispěvatelé: | Roberto Gorrieri |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Discrete mathematics
Algebraic properties Finite-state machine Computer science Process calculus Bisimulation equivalence Petri net Congruence relation Computer Science Applications Theoretical Computer Science Decidability Petri nets Finite-state machines truly-concurrent semantics weak bisimulation branching bisimulation axiomatization Computational Theory and Mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Equivalence (formal languages) Information Systems |
| Popis: | Finite-state machines, a simple class of finite Petri nets, were equipped in [16] with an efficiently decidable, truly-concurrent, bisimulation-based, behavioral equivalence, called team equivalence, which conservatively extends classic bisimulation equivalence on labeled transition systems and which is checked in a distributed manner. This paper addresses the problem of defining variants of this equivalence which are insensitive to silent moves. We define (rooted) weak team equivalence and (rooted) branching team equivalence as natural transposition to finite-state machines of Milner's weak bisimilarity [25] and van Glabbeek and Weijland's branching bisimilarity [12] on labeled transition systems. The process algebra CFM [15] is expressive enough to represent all and only the finite-state machines, up to net isomorphism. Here we first prove that the rooted versions of these equivalences are congruences for the operators of CFM, then we show some algebraic properties, and, finally, we provide finite, sound and complete, axiomatizations for them. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|