arXiv subjects

Klaus-Dieter Schewe

Publications and source records attributed to Klaus-Dieter Schewe.

At least 19 recordsLinked to original sources

arXiv2026

A Behavioural Theory of Probabilistic Algorithms Using Probabilistic Abstract State Machines

We motivate an axiomatic definition of probabilistic algorithms (PAs) by four postulates covering random branching time, abstract states, background, and random bounded exploration. Then, we introduce probabilistic Abstract State Machines (pASMs) and show that they specify PAs. Finally, we prove that every PA satisfying these postulates can be simulated step-by-step by a behaviourally equivalent pASM with the same signature and background.

cs.LO↗

arXiv2026

TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory

The verification of liveness conditions is an important aspect of state-based rigorous methods. This article addresses the extension of the logic of Event-B to a powerful logic, in which properties of traces of an Event-B machine can be expressed. However, all formulae of this logic are still interpreted over states of an Event-B machine rather than traces. The logic exploits that for an Event-B machine $M$ a state $S$ determines all traces of $M$ starting in $S$. We identify a fragment called TREBL of this logic, in which all liveness conditions of interest can be expressed, and define a set of sound derivation rules for the fragment. We further show relative completeness of these derivation rules in the sense that for every valid entailment of a formula $φ$ one can find a derivation, provided the machine $M$ is sufficiently refined. The decisive property is that certain variant terms must be definable in the refined machine. We show that such refinements always exist. Throughout the article several examples from the field of security are used to illustrate the theory.

cs.LO↗

arXiv2025

Behavioural Theory of Reflective Algorithms II: Reflective Parallel Algorithms

We develop a behavioural theory of reflective parallel algorithms (RAs), i.e. synchronous parallel algorithms that can modify their own behaviour. The theory comprises a set of postulates defining the class of RAs, an abstract machine model, and the proof that all RAs are captured by this machine model. RAs are sequential-time, parallel algorithms, where every state includes a representation of the algorithm in that state, thus enabling linguistic reflection. Bounded exploration is preserved using multiset comprehension terms as values. The abstract machine model is defined by reflective Abstract State Machines (rASMs), which extend ASMs using extended states that include an updatable representation of the main ASM rule to be executed by the machine in that state.

cs.LO↗

arXiv2025

Insignificant Choice Polynomial Time: A Logic Capturing PTIME

In this article choiceless polynomial time (CPT) is extended using non-determini\-stic Abstract State Machines (ASMs), which are restricted by three conditions: (1) choice is restricted to choice among atoms; (2) update sets in a state must be isomorphic; (3) for any two isomorphic update sets on states $S$ and $S^\prime$, respectively, the sets of update sets of the corresponding successor states are isomorphic. The restrictions can be incorporated into the semantics of ASM rules such that update sets are only yielded, if the conditions are satisfied. Furthermore, the conditions can be checked in polynomial time on a simulating Turing machine. Finally, the conditions imply global insignificance, i.e. the final result is independent from the choices. These properties suffice to show that the ASMs restricted this way define a logic capturing PTIME, which we call insignificant choice polynomial time (ICPT)

cs.CC↗

arXiv2024

A Complete Fragment of LTL(EB)

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.

cs.LO↗

arXiv2024

Choiceless Polynomial Space

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.

cs.LO↗

arXiv2022

Asynchronous Control-State Choreographies

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.

cs.LO↗

arXiv2021

Exploiting Spline Models for the Training of Fully Connected Layers in Neural Network

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.

cs.LG↗

arXiv2020

Completeness in Polylogarithmic Time and Space

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.

cs.LO↗

arXiv2020

A Behavioural Theory of Recursive Algorithms

"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.

cs.LO↗

arXiv2020

Behavioural Theory of Reflective Algorithms I: Reflective Sequential Algorithms

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.

cs.LO↗

arXiv2019

Proper Hierarchies in Polylogarithmic Time and Absence of Complete Problems

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.

cs.CC↗

arXiv2019

A Restricted Second-Order Logic for Non-deterministic Poly-Logarithmic Time

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.

cs.LO↗

arXiv2019

Concurrent Computing with Shared Replicated Memory

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.

cs.DC↗

arXiv2018

The Polylog-Time Hierarchy Captured by Restricted Second-Order Logic

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.

cs.LO↗

arXiv2017

Accurate and Efficient Profile Matching in Knowledge Bases

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.

cs.LO↗

arXiv2017

Serialisable Multi-Level Transaction Control: A Specification and Verification

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.

cs.DB↗

arXiv2017

Specifying Transaction Control to Serialize Concurrent Program Executions

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.

cs.DB↗