TY - JOUR
T1 - Congruence from the operator’s point of view
T2 - Syntactic requirements on modal characterizations
AU - Gazda, Maciej
AU - Fokkink, Wan
AU - Massaro, Vittorio
PY - 2020/10/1
Y1 - 2020/10/1
N2 - A basic sanity property of a process semantics is that it constitutes a congruence with respect to standard process operators. This issue has been traditionally addressed by developing, for a specific process semantics, a syntactic format for operational semantics specifications. We suggest a novel, orthogonal approach, which focuses on a specific process operator and determines a class of congruence relations for this operator. To this end, we impose syntactic restrictions on Hennessy–Milner logic, so that a process semantics whose modal characterization satisfies those criteria is guaranteed to be a congruence with respect to the operator in question. We investigate alternative composition, action prefix, projection, encapsulation, renaming, and parallel composition with communication, in the context of both concrete and weak process semantics.
AB - A basic sanity property of a process semantics is that it constitutes a congruence with respect to standard process operators. This issue has been traditionally addressed by developing, for a specific process semantics, a syntactic format for operational semantics specifications. We suggest a novel, orthogonal approach, which focuses on a specific process operator and determines a class of congruence relations for this operator. To this end, we impose syntactic restrictions on Hennessy–Milner logic, so that a process semantics whose modal characterization satisfies those criteria is guaranteed to be a congruence with respect to the operator in question. We investigate alternative composition, action prefix, projection, encapsulation, renaming, and parallel composition with communication, in the context of both concrete and weak process semantics.
UR - http://www.scopus.com/inward/record.url?scp=85075932473&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85075932473&partnerID=8YFLogxK
U2 - 10.1007/s00236-019-00355-5
DO - 10.1007/s00236-019-00355-5
M3 - Article
AN - SCOPUS:85075932473
SN - 0001-5903
VL - 57
SP - 329
EP - 351
JO - Acta Informatica
JF - Acta Informatica
IS - 3-5
ER -