We investigate Leifer and Milner \emph{RPO approach} for deriving efficient (finitely branching) LTS's and bisimilarities for $\pi$-calculus. To this aim, we work in a category of \emph{second-order term contexts} and we apply a general \emph{pruning technique}, which allows to simplify the set of transitions in the LTS obtained from the original RPO approach. The resulting LTS and bisimilarity provide an alternative presentation of \emph{symbolic LTS} and Sangiorgi's \emph{open bisimilarity}.
Efficient Bisimilarities from Second-order Reaction Semantics for pi-calculus
DI GIANANTONIO, Pietro;LENISA, Marina
2010-01-01
Abstract
We investigate Leifer and Milner \emph{RPO approach} for deriving efficient (finitely branching) LTS's and bisimilarities for $\pi$-calculus. To this aim, we work in a category of \emph{second-order term contexts} and we apply a general \emph{pruning technique}, which allows to simplify the set of transitions in the LTS obtained from the original RPO approach. The resulting LTS and bisimilarity provide an alternative presentation of \emph{symbolic LTS} and Sangiorgi's \emph{open bisimilarity}.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
concur10.pdf
non disponibili
Tipologia:
Altro materiale allegato
Licenza:
Non pubblico
Dimensione
248.03 kB
Formato
Adobe PDF
|
248.03 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
