2-Nested Simulation is not Finitely Equationally Axiomatizable

Luca Aceto
Willem Jan Fokkink
Anna Ingólfsdóttir

August 2000


2-nested simulation was introduced by Groote and Vaandrager 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, 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

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.