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
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.