Abstract:
Van Glabbeek (1990) presented the linear time-branching time
spectrum of behavioral equivalences for finitely branching, concrete,
sequential processes. He studied these semantics in the setting of the basic
process algebra BCCSP, and tried to give finite complete and
-complete axiomatizations for them. (An axiomatization 
is
-complete when an equation can be derived from if, and only if,
all its closed instantiations can be derived from .) Obtaining such
axiomatizations in concurrency theory often turns out to be difficult, even
in the setting of simple languages like BCCSP. This has raised a host of open
questions that have been the subject of intensive research in recent years.
Most of these questions have been settled over BCCSP, either positively by
giving a finite complete or -complete axiomatization, or negatively
by proving that such an axiomatization does not exist. Still some open
questions remain. This paper reports on these results, and on the
state-of-the-art on axiomatizations for richer process algebras, containing
constructs like sequential and parallel composition
-complete axiomatizations for them. (An axiomatization is
-complete when an equation can be derived from if, and only if,
all its closed instantiations can be derived from .) Obtaining such
axiomatizations in concurrency theory often turns out to be difficult, even
in the setting of simple languages like BCCSP. This has raised a host of open
questions that have been the subject of intensive research in recent years.
Most of these questions have been settled over BCCSP, either positively by
giving a finite complete or -complete axiomatization, or negatively
by proving that such an axiomatization does not exist. Still some open
questions remain. This paper reports on these results, and on the
state-of-the-art on axiomatizations for richer process algebras, containing
constructs like sequential and parallel compositionAvailable as PostScript, PDF.