Complete and ready simulation semantics are not finitely based over BCCSP, even with a singleton alphabet

This note shows that the complete and the ready simulation preorders do not have a finite inequational basis over the language BCCSP when the set of actions is a singleton. Moreover, the equivalences induced by those preorders do not have a finite (in)equational axiomatization either. These results are in contrast with a claim of finite axiomatizability for those semantics in the literature, which was based on the erroneous assumption that they coincide with complete trace semantics in the presence of a singleton set of actions.     

The equational theory of prebisimilarity over basic CCS with divergence

This paper studies the equational theory of prebisimilarity, a bisimulation-based preorder introduced by Hennessy and Milner in the early 1980s, over basic CCS with the divergent process Ω. It is well known that prebisimilarity affords a finite ground-complete axiomatization over this language; this study proves that this ground-complete axiomatization is also complete in the presence of an infinite set of actions. Moreover, in sharp contrast to this positive result, it is shown that prebisimilarity is not finitely based over basic CCS with the divergent process Ω when the set of actions is finite and nonempty.     

On the axiomatizability of priority II

This paper contributes to the study of the equational theory of the priority operator of Baeten, Bergstra and Klop in the setting of the process algebra BCCSP. It is shown that, in the presence of at least two actions, the collection of process equations over BCCSP with the priority operator that are valid modulo bisimilarity, irrespective of the chosen priority order over actions, is not finitely based. This holds true even if one restricts oneself to the collection of valid process equations that do not contain occurrences of process variables.     

Nested semantics over finite trees are equationally hard

This paper studies nested simulation and nested trace semantics over the language BCCSP, a basic formalism to express finite process behaviour. It is shown that none of these semantics affords finite (in)equational axiomatizations over BCCSP. In particular, for each of the nested semantics studied in this paper, the collection of sound, closed (in)equations over a singleton action set is not finitely based.     

A ground-complete axiomatization of stateless bisimilarity over Linda

This paper offers a finite, ground-complete axiomatization of stateless bisimilarity over the tuple-space-based coordination language Linda. As stepping stones towards that result, axiomatizations of stateless bisimilarity over the sequential fragment of Linda without the nask primitive, and over the full sequential sub-language are given. It is also shown that stateless bisimilarity coincides with standard bisimilarity over the sequential fragment of Linda without the nask primitive.