TY - GEN
T1 - On the axiomatisability of parallel composition
T2 - 31st International Conference on Concurrency Theory, CONCUR 2020
AU - Aceto, Luca
AU - Castiglioni, Valentina
AU - Ingólfsdóttir, Anna
AU - Luttik, Bas
AU - Pedersen, Mathias Ruggaard
PY - 2020/8/1
Y1 - 2020/8/1
N2 - This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek's linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. On the other hand, we show that no congruence over that language that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation. This negative result applies to all the nested trace and nested simulation semantics.
AB - This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek's linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. On the other hand, we show that no congruence over that language that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation. This negative result applies to all the nested trace and nested simulation semantics.
KW - Axiomatisation
KW - Linear time-branching time spectrum
KW - Parallel composition
UR - http://www.scopus.com/inward/record.url?scp=85091560477&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CONCUR.2020.18
DO - 10.4230/LIPIcs.CONCUR.2020.18
M3 - Conference contribution
AN - SCOPUS:85091560477
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 181
EP - 1822
BT - 31st International Conference on Concurrency Theory, CONCUR 2020
A2 - Konnov, Igor
A2 - Kovacs, Laura
PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Y2 - 1 September 2020 through 4 September 2020
ER -