Open Access2-Nested Simulation is not Finitely Equationally Axiomatizable
Author(s) -
Luca Aceto,
Willem Jan Fokkink,
Anna Ingólfsdóttir
Publication year - 2000
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v7i20.20147
Subject(s) - mathematics , concurrency , congruence (geometry) , equivalence (formal languages) , trace (psycholinguistics) , equational logic , process calculus , discrete mathematics , combinatorics , computer science , programming language , rewriting , geometry , linguistics , philosophy
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.