TY - JOUR
T1 - Ready to preorder: The case of weak process semantics
AU - Chen, T.
AU - Fokkink, W.J.
AU - van Glabbeek, R.J.
N1 - DBLP:journals/ipl/ChenFG08
PY - 2008
Y1 - 2008
N2 - Recently, Aceto, Fokkink and Ingólfsdóttir proposed an algorithm to turn any sound and ground-complete axiomatisation of any preorder listed in the linear time-branching time spectrum at least as coarse as the ready simulation preorder, into a sound and ground-complete axiomatisation of the corresponding equivalence-its kernel. Moreover, if the former axiomatisation is ω-complete, so is the latter. Subsequently, de Frutos Escrig, Gregorio Rodríguez and Palomino generalised this result, so that the algorithm is applicable to any preorder at least as coarse as the ready simulation preorder, provided it is initials preserving. The current paper shows that the same algorithm applies equally well to weak semantics: the proviso of initials preserving can be replaced by other conditions, such as weak initials preserving and satisfying the second τ-law. This makes it applicable to all 87 preorders surveyed in "the linear time-branching time spectrum II" that are at least as coarse as the ready simulation preorder. We also extend the scope of the algorithm to infinite processes, by adding recursion constants. As an application of both extensions, we provide a ground-complete axiomatisation of the CSP failures equivalence for BCCS processes with divergence. © 2008 Elsevier B.V. All rights reserved.
AB - Recently, Aceto, Fokkink and Ingólfsdóttir proposed an algorithm to turn any sound and ground-complete axiomatisation of any preorder listed in the linear time-branching time spectrum at least as coarse as the ready simulation preorder, into a sound and ground-complete axiomatisation of the corresponding equivalence-its kernel. Moreover, if the former axiomatisation is ω-complete, so is the latter. Subsequently, de Frutos Escrig, Gregorio Rodríguez and Palomino generalised this result, so that the algorithm is applicable to any preorder at least as coarse as the ready simulation preorder, provided it is initials preserving. The current paper shows that the same algorithm applies equally well to weak semantics: the proviso of initials preserving can be replaced by other conditions, such as weak initials preserving and satisfying the second τ-law. This makes it applicable to all 87 preorders surveyed in "the linear time-branching time spectrum II" that are at least as coarse as the ready simulation preorder. We also extend the scope of the algorithm to infinite processes, by adding recursion constants. As an application of both extensions, we provide a ground-complete axiomatisation of the CSP failures equivalence for BCCS processes with divergence. © 2008 Elsevier B.V. All rights reserved.
U2 - 10.1016/j.ipl.2008.09.003
DO - 10.1016/j.ipl.2008.09.003
M3 - Article
SN - 0020-0190
VL - 109
SP - 104
EP - 111
JO - Information Processing Letters
JF - Information Processing Letters
IS - 2
ER -