A new thesis concerning synchronised parallel computing -- simplified parallel ASM thesis

DOI10.1016/J.TCS.2016.08.013zbMATH Open1355.68087arXiv1504.06203OpenAlexW2100307158MaRDI QIDQ313981FDOQ313981

Loredana Tec, Flavio Ferrarotti, Qing Wang, Klaus-Dieter Schewe

Publication date: 12 September 2016

Published in: Theoretical Computer Science (Search for Journal in Brave)

Abstract: A behavioural theory consists of machine-independent postulates characterizing a particular class of algorithms or systems, an abstract machine model that provably satisfies these postulates, and a rigorous proof that any algorithm or system stipulated by the postulates is captured by the abstract machine model. The class of interest in this article is that of synchronous parallel algorithms. For this class a behavioural theory has already been developed by Blass and Gurevich, which unfortunately, though mathematically correct, fails to be convincing, as it is not intuitively clear that the postulates really capture the essence of (synchronous) parallel algorithms. In this article we present a much simpler (and presumably more convincing) set of four postulates for (synchronous) parallel algorithms, which are rather close to those used in Gurevich's celebrated sequential ASM thesis, i.e. the behavioural theory of sequential algorithms. The key difference is made by an extension of the bounded exploration postulate using multiset comprehension terms instead of ground terms formulated over the signature of the states. In addition, all implicit assumptions are made explicit, which amounts to considering states of a parallel algorithm to be represented by meta-finite first-order structures. The article first provides the necessary evidence that the axiomatization presented in this article characterizes indeed the whole class of deterministic, synchronous, parallel algorithms, then formally proves that parallel algorithms are captured by Abstract State Machines (ASMs). The proof requires some recourse to methods from finite model theory, by means of which it can be shown that if a critical tuple defines an update in some update set, then also every other tuple that is logically indistinguishable defines an update in that update set.

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

Recommendations

• Abstract state machines capture parallel algorithms: correction and extension
• Abstract state machines capture parallel algorithms
• scientific article; zbMATH DE number 1860674
• scientific article; zbMATH DE number 1343482
• A behavioural theory of recursive algorithms

zbMATH Keywords

parallel algorithmabstract state machineASM thesisbehavioural theory

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Parallel algorithms in computer science (68W10)

Cites Work

• Abstract State Machines
• Evolving Algebras 1993: Lipari Guide
• Title not available (Why is that?)
• Concurrent abstract state machines
• Title not available (Why is that?)
• Title not available (Why is that?)
• A new thesis concerning synchronised parallel computing -- simplified parallel ASM thesis
• Abstract state machines capture parallel algorithms
• Abstract state machines capture parallel algorithms
• Interactive Small-Step Algorithms I: Axiomatization
• Sequential abstract-state machines capture sequential algorithms
• On elementary equivalence for equality-free logic
• Metafinite model theory
• Title not available (Why is that?)
• Foundational Analyses of Computation
• Foundations of information and knowledge systems. 7th international symposium, FoIKS 2012, Kiel, Germany, March 5--9, 2012. Proceedings

Cited In (11)

• ASM specification and refinement of a quantum algorithm
• Computation on structures. Behavioural theory, logic, complexity
• Axiomatization and characterization of BSP algorithms
• Capturing Membrane Computing by ASMs
• Distributed Adaptive Systems
• Concurrent abstract state machines
• A new thesis concerning synchronised parallel computing -- simplified parallel ASM thesis
• Systematic Refinement of Abstract State Machines with Higher-Order Logic
• A unifying logic for non-deterministic, parallel and concurrent abstract state machines
• A Behavioural Theory of Recursive Algorithms
• A Logic for Reflective ASMs

This page was built for publication: A new thesis concerning synchronised parallel computing -- simplified parallel ASM thesis

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