We study general equational characterizations for bisimulation and trace semantics via the respective post-/pre-metaequivalences defined on the ULTraS metamodel. This yields axiomatizations encompassing those appeared in the literature, as well as new ones, for bisimulation and trace equivalences when applied to specific classes of processes. The equational laws are developed incrementally, by starting with some core axioms and then singling out additional axioms for bisimulation post-/pre-metaequivalences on the one hand, and different additional axioms for trace post-/pre-metaequivalences on the other hand. The axiomatizations highlight the fundamental differences in the discriminating power between bisimulation semantics and trace semantics, regardless of specific classes of processes. Moreover, they generalize idempotency laws of bisimilarity and choice-deferring laws of trace semantics, in addition to formalizing shuffling laws for pre-metaequivalences.

Towards General Axiomatizations for Bisimilarity and Trace Semantics

Bernardo, Marco
2021-01-01

Abstract

We study general equational characterizations for bisimulation and trace semantics via the respective post-/pre-metaequivalences defined on the ULTraS metamodel. This yields axiomatizations encompassing those appeared in the literature, as well as new ones, for bisimulation and trace equivalences when applied to specific classes of processes. The equational laws are developed incrementally, by starting with some core axioms and then singling out additional axioms for bisimulation post-/pre-metaequivalences on the one hand, and different additional axioms for trace post-/pre-metaequivalences on the other hand. The axiomatizations highlight the fundamental differences in the discriminating power between bisimulation semantics and trace semantics, regardless of specific classes of processes. Moreover, they generalize idempotency laws of bisimilarity and choice-deferring laws of trace semantics, in addition to formalizing shuffling laws for pre-metaequivalences.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11576/2689576
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact