摘要：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.
