2-Nested Simulation is not Finitely Equationally Axiomatizable

Abstract

2-nested simulation was introduced by Groote and Vaandrager
[10] as the coarsest equivalence included in completed trace equivalence
for which the tyft/tyxt format is a congruence format. In the linear
time-branching time spectrum of van Glabbeek [8], 2-nested simulation
is one of the few equivalences for which no finite equational axiomatization
is presented. In this paper we prove that such an axiomatization
does not exist for 2-nested simulation.

Keywords: Concurrency, process algebra, basic CCS, 2-nested simulation,
equational logic, complete axiomatizations.