On the axiomatizability of impossible futures

DOI10.2168/LMCS-11(3:17)2015MaRDI QIDQ3196348zbMATHFDO

Authors Taolue Chen, Wan Fokkink, Rob van Glabbeek

Publication date 29 October 2015

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

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

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)

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.

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

Cited in

(6)

• The equational theory of weak complete simulation semantics over BCCSP
• Non-finite axiomatisability results via reductions: CSP parallel composition and CCS restriction
• A Peculiar Connection Between the Axiom of Choice and Predicting the Future
• Lifting non-finite axiomatizability results to extensions of process algebras
• Axiomatizing weak simulation semantics over BCCSP
• On Finite Bases for Weak Semantics: Failures Versus Impossible Futures

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)