-
A Complete Fragment of LTL(EB)
Authors:
Flavio Ferrarotti,
Peter Rivière,
Klaus-Dieter Schewe,
Neeraj Kumar Singh,
Yamine Aït Ameur
Abstract:
The verification of liveness conditions is an important aspect of state-based rigorous methods. This article investigates this problem in a fragment $\square$LTL of the logic LTL(EB), the integration of the UNTIL-fragment of Pnueli's linear time temporal logic (LTL) and the logic of Event-B, in which the most commonly used liveness conditions can be expressed. For this fragment a sound set of deri…
▽ More
The verification of liveness conditions is an important aspect of state-based rigorous methods. This article investigates this problem in a fragment $\square$LTL of the logic LTL(EB), the integration of the UNTIL-fragment of Pnueli's linear time temporal logic (LTL) and the logic of Event-B, in which the most commonly used liveness conditions can be expressed. For this fragment a sound set of derivation rules is developed, which is also complete under mild restrictions for Event-B machines.
△ Less
Submitted 30 January, 2024;
originally announced January 2024.
-
Choiceless Polynomial Space
Authors:
Flavio Ferrarotti,
Klaus-Dieter Schewe
Abstract:
Abstract State Machines (ASMs) provide a model of computations on structures rather than strings. Blass, Gurevich and Shelah showed that deterministic PTIME-bounded ASMs define the choiceless fragment of PTIME, but cannot capture PTIME. In this article deterministic PSPACE-bounded ASMs are introduced, and it is proven that they cannot capture PSPACE. The key for the proof is a characterisation by…
▽ More
Abstract State Machines (ASMs) provide a model of computations on structures rather than strings. Blass, Gurevich and Shelah showed that deterministic PTIME-bounded ASMs define the choiceless fragment of PTIME, but cannot capture PTIME. In this article deterministic PSPACE-bounded ASMs are introduced, and it is proven that they cannot capture PSPACE. The key for the proof is a characterisation by partial fixed-point formulae over the Stärk/Nanchen logic for deterministic ASMs and a construction of transitive structures, in which such formulae must hold. This construction exploits that the decisive support theorem for choiceless polynomial time holds under slightly weaker assumptions.
△ Less
Submitted 29 January, 2024;
originally announced January 2024.
-
Exploiting Spline Models for the Training of Fully Connected Layers in Neural Network
Authors:
Kanya Mo,
Shen Zheng,
Xiwei Wang,
**ghua Wang,
Klaus-Dieter Schewe
Abstract:
The fully connected (FC) layer, one of the most fundamental modules in artificial neural networks (ANN), is often considered difficult and inefficient to train due to issues including the risk of overfitting caused by its large amount of parameters. Based on previous work studying ANN from linear spline perspectives, we propose a spline-based approach that eases the difficulty of training FC layer…
▽ More
The fully connected (FC) layer, one of the most fundamental modules in artificial neural networks (ANN), is often considered difficult and inefficient to train due to issues including the risk of overfitting caused by its large amount of parameters. Based on previous work studying ANN from linear spline perspectives, we propose a spline-based approach that eases the difficulty of training FC layers. Given some dataset, we first obtain a continuous piece-wise linear (CPWL) fit through spline methods such as multivariate adaptive regression spline (MARS). Next, we construct an ANN model from the linear spline model and continue to train the ANN model on the dataset using gradient descent optimization algorithms. Our experimental results and theoretical analysis show that our approach reduces the computational cost, accelerates the convergence of FC layers, and significantly increases the interpretability of the resulting model (FC layers) compared with standard ANN training with random parameter initialization followed by gradient descent optimizations.
△ Less
Submitted 12 February, 2021;
originally announced February 2021.
-
Completeness in Polylogarithmic Time and Space
Authors:
Flavio Ferrarotti,
Senen Gonzalez,
Klaus-Dieter Schewe,
Jose Maria Turull-Torres
Abstract:
Complexity theory can be viewed as the study of the relationship between computation and applications, understood the former as complexity classes and the latter as problems. Completeness results are clearly central to that view. Many natural algorithms resulting from current applications have polylogarithmic time (PolylogTime) or space complexity (PolylogSpace). The classical Karp notion of compl…
▽ More
Complexity theory can be viewed as the study of the relationship between computation and applications, understood the former as complexity classes and the latter as problems. Completeness results are clearly central to that view. Many natural algorithms resulting from current applications have polylogarithmic time (PolylogTime) or space complexity (PolylogSpace). The classical Karp notion of complete problem however does not plays well with these complexity classes. It is well known that PolylogSpace does not have complete problems under logarithmic space many-one reductions. In this paper we show similar results for deterministic and non-deterministic PolylogTime as well as for every other level of the polylogarithmic time hierarchy. We achieve that by following a different strategy based on proving the existence of proper hierarchies of problems inside each class. We then develop an alternative notion of completeness inspired by the concept of uniformity from circuit complexity and prove the existence of a (uniformly) complete problem for PolylogSpace under this new notion. As a consequence of this result we get that complete problems can still play an important role in the study of the interrelationship between polylogarithmic and other classical complexity classes.
△ Less
Submitted 8 September, 2020;
originally announced September 2020.
-
Asynchronous Control-State Choreographies
Authors:
Klaus-Dieter Schewe,
Yamine Ait-Ameur,
Sarah Benyagoub
Abstract:
Choreographies prescribe the rendez-vous synchronisation of messages in a system of communicating finite state machines. Such a system is called realisable, if the traces of the prescribed communication coincide with those of the asynchronous system of peers, where the communication channels either use FIFO queues or multiset mailboxes. In a recent article realisability was characterised by two ne…
▽ More
Choreographies prescribe the rendez-vous synchronisation of messages in a system of communicating finite state machines. Such a system is called realisable, if the traces of the prescribed communication coincide with those of the asynchronous system of peers, where the communication channels either use FIFO queues or multiset mailboxes. In a recent article realisability was characterised by two necessary conditions that together are sufficient. A simple consequence is that realisability in the presence of a choreography becomes decidable. In this article we extend this work by generalising choreographies to control-state choreographies, which enable parallelism. We redefine P2P systems on grounds of control-state machines and show that a control-state choreography is equivalent to the rendez-vous compositions of its peers and that language-synchronisability coincides with synchronisability. These results are used to characterise realisability of control-state choreographies. As for the case of FSM-based choreographies we prove two necessary conditions: a sequence condition and a choice condition. Then we also show that these two conditions together are sufficient for the realisability of control-state choreographies.
△ Less
Submitted 2 December, 2022; v1 submitted 8 September, 2020;
originally announced September 2020.
-
Insignificant Choice Polynomial Time
Authors:
Klaus-Dieter Schewe
Abstract:
In the late 1980s Gurevich conjectured that there is no logic capturing PTIME, where logic has to be understood in a very general way comprising computation models over structures. In this article we first refute Gurevich's conjecture. For this we extend the seminal research of Blass, Gurevich and Shelah on {\em choiceless polynomial time} (CPT), which exploits deterministic Abstract State Machine…
▽ More
In the late 1980s Gurevich conjectured that there is no logic capturing PTIME, where logic has to be understood in a very general way comprising computation models over structures. In this article we first refute Gurevich's conjecture. For this we extend the seminal research of Blass, Gurevich and Shelah on {\em choiceless polynomial time} (CPT), which exploits deterministic Abstract State Machines (ASMs) supporting unbounded parallelism to capture the choiceless fragment of PTIME. CPT is strictly included in PTIME. We observe that choice is unavoidable, but that a restricted version suffices, which guarantees that the final result is independent from the choice. Such a version of polynomially bounded ASMs, which we call {\em insignificant choice polynomial time} (ICPT) will indeed capture PTIME. Even more, insignificant choice can be captured by ASMs with choice restricted to atoms such that a {\em local insignificance condition} is satisfied. As this condition can be expressed in the logic of non-deterministic ASMs, we obtain a logic capturing PTIME. Furthermore, using inflationary fixed-points we can capture problems in PTIME by fixed-point formulae in a fragment of the logic of non-deterministic ASMs plus inflationary fixed-points. We use this result for our second contribution showing that PTIME differs from NP. For the proof we build again on the research on CPT first establishing a limitation on permutation classes of the sets that can be activated by an ICPT computation. We then prove an inseparability theorem, which characterises classes of structures that cannot be separated by the logic. In particular, this implies that SAT cannot be decided by an ICPT computation.
△ Less
Submitted 1 February, 2021; v1 submitted 10 May, 2020;
originally announced May 2020.
-
Behavioural Theory of Reflective Algorithms I: Reflective Sequential Algorithms
Authors:
Klaus-Dieter Schewe,
Flavio Ferrarotti
Abstract:
We develop a behavioural theory of reflective sequential algorithms (RSAs), i.e. sequential algorithms that can modify their own behaviour. The theory comprises a set of language-independent postulates defining the class of RSAs, an abstract machine model, and the proof that all RSAs are captured by this machine model. As in Gurevich's behavioural theory for sequential algorithms RSAs are sequenti…
▽ More
We develop a behavioural theory of reflective sequential algorithms (RSAs), i.e. sequential algorithms that can modify their own behaviour. The theory comprises a set of language-independent postulates defining the class of RSAs, an abstract machine model, and the proof that all RSAs are captured by this machine model. As in Gurevich's behavioural theory for sequential algorithms RSAs are sequential-time, bounded parallel algorithms, where the bound depends on the algorithm only and not on the input. Different from the class of sequential algorithms every state of an RSA includes a representation of the algorithm in that state, thus enabling linguistic reflection. Bounded exploration is preserved using terms as values. The model of reflective sequential abstract state machines (rsASMs) extends sequential ASMs using extended states that include an updatable representation of the main ASM rule to be executed by the machine in that state. Updates to the representation of ASM signatures and rules are realised by means of a sophisticated tree algebra.
△ Less
Submitted 6 January, 2020;
originally announced January 2020.
-
A Behavioural Theory of Recursive Algorithms
Authors:
Egon Börger,
Klaus-Dieter Schewe
Abstract:
"What is an algorithm?" is a fundamental question of computer science. Gurevich's behavioural theory of sequential algorithms (aka the sequential ASM thesis) gives a partial answer by defining (non-deterministic) sequential algorithms axiomatically, without referring to a particular machine model or programming language, and showing that they are captured by (non-deterministic) sequential Abstract…
▽ More
"What is an algorithm?" is a fundamental question of computer science. Gurevich's behavioural theory of sequential algorithms (aka the sequential ASM thesis) gives a partial answer by defining (non-deterministic) sequential algorithms axiomatically, without referring to a particular machine model or programming language, and showing that they are captured by (non-deterministic) sequential Abstract State Machines (nd-seq ASMs). Moschovakis pointed out that recursive algorithms such as mergesort are not covered by this theory. In this article we propose an axiomatic definition of the notion of sequential recursive algorithm which extends Gurevich's axioms for sequential algorithms by a Recursion Postulate and allows us to prove that sequential recursive algorithms are captured by recursive Abstract State Machines, an extension of nd-seq ASMs by a CALL rule. Applying this recursive ASM thesis yields a characterization of sequential recursive algorithms as finitely composed concurrent algorithms all of whose concurrent runs are partial-order runs.
△ Less
Submitted 24 March, 2020; v1 submitted 6 January, 2020;
originally announced January 2020.
-
A Restricted Second-Order Logic for Non-deterministic Poly-Logarithmic Time
Authors:
Flavio Ferrarotti,
Senen Gonzáles,
Klaus-Dieter Schewe,
José María Turull-Torres
Abstract:
We introduce a restricted second-order logic $\mathrm{SO}^{\mathit{plog}}$ for finite structures where second-order quantification ranges over relations of size at most poly-logarithmic in the size of the structure. We demonstrate the relevance of this logic and complexity class by several problems in database theory. We then prove a Fagin's style theorem showing that the Boolean queries which can…
▽ More
We introduce a restricted second-order logic $\mathrm{SO}^{\mathit{plog}}$ for finite structures where second-order quantification ranges over relations of size at most poly-logarithmic in the size of the structure. We demonstrate the relevance of this logic and complexity class by several problems in database theory. We then prove a Fagin's style theorem showing that the Boolean queries which can be expressed in the existential fragment of $\mathrm{SO}^{\mathit{plog}}$ corresponds exactly to the class of decision problems that can be computed by a non-deterministic Turing machine with random access to the input in time $O((\log n)^k)$ for some $k \ge 0$, i.e., to the class of problems computable in non-deterministic poly-logarithmic time. It should be noted that unlike Fagin's theorem which proves that the existential fragment of second-order logic captures NP over arbitrary finite structures, our result only holds over ordered finite structures, since $\mathrm{SO}^{\mathit{plog}}$ is too weak as to define a total order of the domain. Nevertheless $\mathrm{SO}^{\mathit{plog}}$ provides natural levels of expressibility within poly-logarithmic space in a way which is closely related to how second-order logic provides natural levels of expressibility within polynomial space. Indeed, we show an exact correspondence between the quantifier prefix classes of $\mathrm{SO}^{\mathit{plog}}$ and the levels of the non-deterministic poly-logarithmic time hierarchy, analogous to the correspondence between the quantifier prefix classes of second-order logic and the polynomial-time hierarchy. Our work closely relates to the constant depth quasipolynomial size AND/OR circuits and corresponding restricted second-order logic defined by David A. Mix Barrington in 1992. We explore this relationship in detail.
△ Less
Submitted 29 November, 2019;
originally announced December 2019.
-
Proper Hierarchies in Polylogarithmic Time and Absence of Complete Problems
Authors:
Flavio Ferrarotti,
Senén González,
Klaus-Dieter Schewe,
José María Turull-Torres
Abstract:
The polylogarithmic time hierarchy structures sub-linear time complexity. In recent work it was shown that all classes $\tildeΣ_{m}^{\mathit{plog}}$ or $\tildeΠ_{m}^{\mathit{plog}}$ ($m \in \mathbb{N}$) in this hierarchy can be captured by semantically restricted fragments of second-order logic. In this paper the descriptive complexity theory of polylogarithmic time is taken further showing that t…
▽ More
The polylogarithmic time hierarchy structures sub-linear time complexity. In recent work it was shown that all classes $\tildeΣ_{m}^{\mathit{plog}}$ or $\tildeΠ_{m}^{\mathit{plog}}$ ($m \in \mathbb{N}$) in this hierarchy can be captured by semantically restricted fragments of second-order logic. In this paper the descriptive complexity theory of polylogarithmic time is taken further showing that there are strict hierarchies inside each of the classes of the hierarchy. A straightforward consequence of this result is that there are no complete problems for these complexity classes, not even under polynomial time reductions. As another consequence we show that the polylogarithmic time hierarchy itself is strict.
△ Less
Submitted 29 November, 2019;
originally announced November 2019.
-
Concurrent Computing with Shared Replicated Memory
Authors:
Klaus-Dieter Schewe,
Andreas Prinz,
Egon Börger
Abstract:
The behavioural theory of concurrent systems states that any concurrent system can be captured by a behaviourally equivalent concurrent Abstract State Machine (cASM). While the theory in general assumes shared locations, it remains valid, if different agents can only interact via messages, i.e. sharing is restricted to mailboxes. There may even be a strict separation between memory managing agents…
▽ More
The behavioural theory of concurrent systems states that any concurrent system can be captured by a behaviourally equivalent concurrent Abstract State Machine (cASM). While the theory in general assumes shared locations, it remains valid, if different agents can only interact via messages, i.e. sharing is restricted to mailboxes. There may even be a strict separation between memory managing agents and other agents that can only access the shared memory by sending query and update requests to the memory agents. This article is dedicated to an investigation of replicated data that is maintained by a memory management subsystem, whereas the replication neither appears in the requests nor in the corresponding answers. We show how the behaviour of a concurrent system with such a memory management can be specified using concurrent communicating ASMs. We provide several refinements of a high-level ground model addressing different replication policies and internal messaging between data centres. For all these refinements we analyse their effects on the runs such that decisions concerning the degree of consistency can be consciously made.
△ Less
Submitted 13 February, 2019;
originally announced February 2019.
-
The Polylog-Time Hierarchy Captured by Restricted Second-Order Logic
Authors:
Flavio Ferrarotti,
Senén González,
Klaus-Dieter Schewe,
José María Turull-Torres
Abstract:
Let $\mathrm{SO}^{\mathit{plog}}$ denote the restriction of second-order logic, where second-order quantification ranges over relations of size at most poly-logarithmic in the size of the structure. In this article we investigate the problem, which Turing machine complexity class is captured by Boolean queries over ordered relational structures that can be expressed in this logic. For this we defi…
▽ More
Let $\mathrm{SO}^{\mathit{plog}}$ denote the restriction of second-order logic, where second-order quantification ranges over relations of size at most poly-logarithmic in the size of the structure. In this article we investigate the problem, which Turing machine complexity class is captured by Boolean queries over ordered relational structures that can be expressed in this logic. For this we define a hierarchy of fragments $Σ^{\mathit{plog}}_m$ (and $Π^{\mathit{plog}}_m$) defined by formulae with alternating blocks of existential and universal second-order quantifiers in quantifier-prenex normal form. We first show that the existential fragment $Σ^{\mathit{plog}}_1$ captures NPolyLogTime, i.e. the class of Boolean queries that can be accepted by a non-deterministic Turing machine with random access to the input in time $O((\log n)^k)$ for some $k \ge 0$. Using alternating Turing machines with random access input allows us to characterise also the fragments $Σ^{\mathit{plog}}_m$ (and $Π^{\mathit{plog}}_m$) as those Boolean queries with at most $m$ alternating blocks of second-order quantifiers that are accepted by an alternating Turing machine. Consequently, $\mathrm{SO}^{\mathit{plog}}$ captures the whole poly-logarithmic time hierarchy. We demonstrate the relevance of this logic and complexity class by several problems in database theory.
△ Less
Submitted 19 June, 2018;
originally announced June 2018.
-
Accurate and Efficient Profile Matching in Knowledge Bases
Authors:
Jorge Martinez-Gil,
Alejandra Lorena Paoletti,
Gábor Rácz,
Attila Sali,
Klaus-Dieter Schewe
Abstract:
A profile describes a set of properties, e.g. a set of skills a person may have, a set of skills required for a particular job, or a set of abilities a football player may have with respect to a particular team strategy. Profile matching aims to determine how well a given profile fits to a requested profile. The approach taken in this article is grounded in a matching theory that uses filters in l…
▽ More
A profile describes a set of properties, e.g. a set of skills a person may have, a set of skills required for a particular job, or a set of abilities a football player may have with respect to a particular team strategy. Profile matching aims to determine how well a given profile fits to a requested profile. The approach taken in this article is grounded in a matching theory that uses filters in lattices to represent profiles, and matching values in the interval [0,1]: the higher the matching value the better is the fit. Such lattices can be derived from knowledge bases exploiting description logics to represent the knowledge about profiles. An interesting first question is, how human expertise concerning the matching can be exploited to obtain most accurate matchings. It will be shown that if a set of filters together with matching values by some human expert is given, then under some mild plausibility assumptions a matching measure can be determined such that the computed matching values preserve the rankings given by the expert. A second question concerns the efficient querying of databases of profile instances. For matching queries that result in a ranked list of profile instances matching a given one it will be shown how corresponding top-k queries can be evaluated on grounds of pre-computed matching values, which in turn allows the maintenance of the knowledge base to be decoupled from the maintenance of profile instances. In addition, it will be shown how the matching queries can be exploited for gap queries that determine how profile instances need to be extended in order to improve in the rankings. Finally, the theory of matching will be extended beyond the filters, which lead to a matching theory that exploits fuzzy sets or probabilistic logic with maximum entropy semantics. It will be shown that added fuzzy links can be captured by extending the underlying lattice.
△ Less
Submitted 17 November, 2017; v1 submitted 21 June, 2017;
originally announced June 2017.
-
Serialisable Multi-Level Transaction Control: A Specification and Verification
Authors:
Egon Börger,
Klaus-Dieter Schewe,
Qing Wang
Abstract:
We define a programming language independent controller TaCtl for multi-level transactions and an operator $TA$, which when applied to concurrent programs with multi-level shared locations containing hierarchically structured complex values, turns their behavior with respect to some abstract termination criterion into a transactional behavior. We prove the correctness property that concurrent runs…
▽ More
We define a programming language independent controller TaCtl for multi-level transactions and an operator $TA$, which when applied to concurrent programs with multi-level shared locations containing hierarchically structured complex values, turns their behavior with respect to some abstract termination criterion into a transactional behavior. We prove the correctness property that concurrent runs under the transaction controller are serialisable, assuming an Inverse Operation Postulate to guarantee recoverability. For its applicability to a wide range of programs we specify the transaction controller TaCtl and the operator $TA$ in terms of Abstract State Machines (ASMs). This allows us to model concurrent updates at different levels of nested locations in a precise yet simple manner, namely in terms of partial ASM updates. It also provides the possibility to use the controller TaCtl and the operator $TA$ as a plug-in when specifying concurrent system components in terms of sequential ASMs.
△ Less
Submitted 12 June, 2017;
originally announced June 2017.
-
Specifying Transaction Control to Serialize Concurrent Program Executions
Authors:
Egon Börger,
Klaus-Dieter Schewe
Abstract:
We define a programming language independent transaction controller and an operator which when applied to concurrent programs with shared locations turns their behavior with respect to some abstract termination criterion into a transactional behavior. We prove the correctness property that concurrent runs under the transaction controller are serialisable. We specify the transaction controller TaCt…
▽ More
We define a programming language independent transaction controller and an operator which when applied to concurrent programs with shared locations turns their behavior with respect to some abstract termination criterion into a transactional behavior. We prove the correctness property that concurrent runs under the transaction controller are serialisable. We specify the transaction controller TaCtl and the operator TA in terms of Abstract State Machines. This makes TaCtl applicable to a wide range of programs and in particular provides the possibility to use it as a plug-in when specifying concurrent system components in terms of Abstract State Machines.
△ Less
Submitted 6 June, 2017;
originally announced June 2017.
-
A Logic for Non-Deterministic Parallel Abstract State Machines
Authors:
Flavio Ferrarotti,
Klaus-Dieter Schewe,
Loredana Tec,
Qing Wang
Abstract:
We develop a logic which enables reasoning about single steps of non-deterministic parallel Abstract State Machines (ASMs). Our logic builds upon the unifying logic introduced by Nanchen and Stärk for reasoning about hierarchical (parallel) ASMs. Our main contribution to this regard is the handling of non-determinism (both bounded and unbounded) within the logical formalism. Moreover, we do this w…
▽ More
We develop a logic which enables reasoning about single steps of non-deterministic parallel Abstract State Machines (ASMs). Our logic builds upon the unifying logic introduced by Nanchen and Stärk for reasoning about hierarchical (parallel) ASMs. Our main contribution to this regard is the handling of non-determinism (both bounded and unbounded) within the logical formalism. Moreover, we do this without sacrificing the completeness of the logic for statements about single steps of non-deterministic parallel ASMs, such as invariants of rules, consistency conditions for rules, or step-by-step equivalence of rules.
△ Less
Submitted 30 May, 2017;
originally announced May 2017.
-
A Complete Logic for Database Abstract State Machines
Authors:
Flavio Ferrarotti,
Klaus-Dieter Schewe,
Loredana Tec,
Qing Wang
Abstract:
In database theory, the term $\textit{database transformation}$ was used to refer to a unifying treatment for computable queries and updates. Recently, it was shown that non-deterministic database transformations can be captured exactly by a variant of ASMs, the so-called Database Abstract State Machines (DB-ASMs). In this article we present a logic for DB-ASMs, extending the logic of Nanchen and…
▽ More
In database theory, the term $\textit{database transformation}$ was used to refer to a unifying treatment for computable queries and updates. Recently, it was shown that non-deterministic database transformations can be captured exactly by a variant of ASMs, the so-called Database Abstract State Machines (DB-ASMs). In this article we present a logic for DB-ASMs, extending the logic of Nanchen and Stärk for ASMs. In particular, we develop a rigorous proof system for the logic for DB-ASMs, which is proven to be sound and complete. The most difficult challenge to be handled by the extension is a proper formalisation capturing non-determinism of database transformations and all its related features such as consistency, update sets or multisets associated with DB-ASM rules. As the database part of a state of database transformations is a finite structure and DB-ASMs are restricted by allowing quantifiers only over the database part of a state, we resolve this problem by taking update sets explicitly into the logic, i.e. by using an additional modal operator $[X]$, where $X$ is interpreted as an update set $Δ$ generated by a DB-ASM rule. The DB-ASM logic provides a powerful verification tool to study properties of database transformations.
△ Less
Submitted 30 May, 2017; v1 submitted 24 February, 2016;
originally announced February 2016.
-
A New Thesis concerning Synchronised Parallel Computing - Simplified Parallel ASM Thesis
Authors:
Flavio Ferrarotti,
Klaus-Dieter Schewe,
Loredana Tec,
Qing Wang
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…
▽ More
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.
△ Less
Submitted 23 April, 2015;
originally announced April 2015.
