On the Axiomatizability of Impossible Futures

Select |




Print


van Glabbeek, Robert; Chen, Taolue; Fokkink, Wan

van Glabbeek, Robert; Chen, Taolue; Fokkink, Wan


2015-09-22


Journal Article


Logical Methods in Computer Science


11


3


1-31


A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves omega-completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and omega-complete axiomatizations are derived for weak failures, completed trace and trace semantics. We then present a finite, sound, ground-complete axiomatization for the concrete impossible futures preorder, which implies a finite, sound, ground-complete axiomatization for the weak impossible futures preorder. In contrast, we prove that no finite, sound axiomatization for BCCS modulo concrete and weak impossible futures equivalence is ground-complete. If the alphabet of actions is infinite, then the aforementioned ground-complete axiomatizations are shown to be omega-complete. If the alphabet is finite, we prove that the inequational theories of BCCS modulo the concrete and weak impossible futures preorder lack such a finite basis.


Concurrency, Process Algebra, BCCS, labeled transition systems, complete axiomatizations, impossible futures semantics.


https://doi.org/10.2168/LMCS-11(3:17)2015


http://arxiv.org/abs/1505.04985


© 2015


English


nicta:8502


van Glabbeek, Robert; Chen, Taolue; Fokkink, Wan. On the Axiomatizability of Impossible Futures. Logical Methods in Computer Science. 2015-09-22; 11(3):1-31. https://doi.org/10.2168/LMCS-11(3:17)2015



Loading citation data...

Citation counts
(Requires subscription to view)