On the axiomatizability of impossible futures

DOI10.2168/LMCS-11(3:17)2015zbMATH Open1448.68335arXiv1505.04985MaRDI QIDQ3196348FDOQ3196348

Taolue Chen, Wan Fokkink, Rob van Glabbeek

Publication date: 29 October 2015

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1505.04985

Recommendations

• On Finite Bases for Weak Semantics: Failures Versus Impossible Futures
• Automata, Languages and Programming
• scientific article; zbMATH DE number 2038703
• Ready to preorder: the case of weak process semantics
• The equational theory of weak complete simulation semantics over BCCSP

zbMATH Keywords

process algebraconcurrency theoryequational logicimpossible futures

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (5)

• On Finite Bases for Weak Semantics: Failures Versus Impossible Futures
• The Equational Theory of Weak Complete Simulation Semantics over BCCSP
• A Peculiar Connection Between the Axiom of Choice and Predicting the Future
• Non-finite axiomatisability results via reductions: CSP parallel composition and CCS restriction
• Axiomatizing weak simulation semantics over BCCSP

This page was built for publication: On the axiomatizability of impossible futures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3196348)