TY - JOUR

T1 - On finite alphabets and infinite bases

AU - Chen, T.

AU - Fokkink, W.J.

AU - Luttik, B.

AU - Nain, S.

N1 - DBLP:journals/iandc/ChenFLN08

PY - 2008

Y1 - 2008

N2 - Van Glabbeek presented the linear time-branching time spectrum of behavioral semantics. He studied these semantics in the setting of the basic process algebra BCCSP, and gave finite, sound and ground-complete, axiomatizations for most of these semantics. Groote proved for some of van Glabbeek's axiomatizations that they are ω-complete, meaning that an equation can be derived if (and only if) all of its closed instantiations can be derived. In this paper, we settle the remaining open questions for all the semantics in the linear time-branching time spectrum, either positively by giving a finite sound and ground-complete axiomatization that is ω-complete, or negatively by proving that such a finite basis for the equational theory does not exist. We prove that in case of a finite alphabet with at least two actions, failure semantics affords a finite basis, while for ready simulation, completed simulation, simulation, possible worlds, ready trace, failure trace and ready semantics, such a finite basis does not exist. Completed simulation semantics also lacks a finite basis in case of an infinite alphabet of actions. © 2007 Elsevier Inc. All rights reserved.

AB - Van Glabbeek presented the linear time-branching time spectrum of behavioral semantics. He studied these semantics in the setting of the basic process algebra BCCSP, and gave finite, sound and ground-complete, axiomatizations for most of these semantics. Groote proved for some of van Glabbeek's axiomatizations that they are ω-complete, meaning that an equation can be derived if (and only if) all of its closed instantiations can be derived. In this paper, we settle the remaining open questions for all the semantics in the linear time-branching time spectrum, either positively by giving a finite sound and ground-complete axiomatization that is ω-complete, or negatively by proving that such a finite basis for the equational theory does not exist. We prove that in case of a finite alphabet with at least two actions, failure semantics affords a finite basis, while for ready simulation, completed simulation, simulation, possible worlds, ready trace, failure trace and ready semantics, such a finite basis does not exist. Completed simulation semantics also lacks a finite basis in case of an infinite alphabet of actions. © 2007 Elsevier Inc. All rights reserved.

U2 - 10.1016/j.ic.2007.09.003

DO - 10.1016/j.ic.2007.09.003

M3 - Article

VL - 206

SP - 492

EP - 519

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 5

ER -