-
The equational theory of the Weihrauch lattice with multiplication
Authors:
Eike Neumann,
Arno Pauly,
Cécilia Pradic
Abstract:
We study the equational theory of the Weihrauch lattice with multiplication, meaning the collection of equations between terms built from variables, the lattice operations $\sqcup$, $\sqcap$, the product $\times$, and the finite parallelization $(-)^*$ which are true however we substitute Weihrauch degrees for the variables. We provide a combinatorial description of these in terms of a reducibilit…
▽ More
We study the equational theory of the Weihrauch lattice with multiplication, meaning the collection of equations between terms built from variables, the lattice operations $\sqcup$, $\sqcap$, the product $\times$, and the finite parallelization $(-)^*$ which are true however we substitute Weihrauch degrees for the variables. We provide a combinatorial description of these in terms of a reducibility between finite graphs, and moreover, show that deciding which equations are true in this sense is complete for the third level of the polynomial hierarchy.
△ Less
Submitted 20 March, 2024;
originally announced March 2024.
-
On the Complexity of Robust Eventual Inequality Testing for C-Finite Functions
Authors:
Eike Neumann
Abstract:
We study the computational complexity of a robust version of the problem of testing two univariate C-finite functions for eventual inequality at large times. Specifically, working in the bit-model of real computation, we consider the eventual inequality testing problem for real functions that are specified by homogeneous linear Cauchy problems with arbitrary real coefficients and initial values. I…
▽ More
We study the computational complexity of a robust version of the problem of testing two univariate C-finite functions for eventual inequality at large times. Specifically, working in the bit-model of real computation, we consider the eventual inequality testing problem for real functions that are specified by homogeneous linear Cauchy problems with arbitrary real coefficients and initial values. In order to assign to this problem a well-defined computational complexity, we develop a natural notion of polynomial-time decidability of subsets of computable metric spaces which extends our recently introduced notion of maximal partial decidability. We show that eventual inequality of C-finite functions is polynomial-time decidable in this sense.
△ Less
Submitted 1 July, 2023;
originally announced July 2023.
-
Boosting Extra-functional Code Reusability in Cyber-physical Production Systems: The Error Handling Case Study
Authors:
Birgit Vogel-Heuser,
Juliane Fischer,
Dieter Hess,
Eva-Maria Neumann,
Marcus Wuerr
Abstract:
Cyber-Physical Production Systems (CPPS) are long-living and mechatronic systems, which include mechanics, electrics/electronics and software. The interdisciplinary nature combined with challenges and trends in the context of Industry 4.0 such as a high degree of customization, small lot sizes and evolution cause a high amount of variability. Mastering the variability of functional control softwar…
▽ More
Cyber-Physical Production Systems (CPPS) are long-living and mechatronic systems, which include mechanics, electrics/electronics and software. The interdisciplinary nature combined with challenges and trends in the context of Industry 4.0 such as a high degree of customization, small lot sizes and evolution cause a high amount of variability. Mastering the variability of functional control software, e.g., different control variants of an actuator type, is itself a challenge in develo** and reusing CPPS software. This task becomes even more complex when considering extra-functional software such as operating modes, diagnosis and error handling. These software parts have high interdependencies with functional software, often involving the human-machine interface (HMI) to enable the intervention of operators. This paper illustrates the challenges in documenting the dependencies of these software parts including their variability using family models. A procedural and an object-oriented concept for implementing error handling, which represents an extra-functional task with high dependencies to functional software and the HMI, are proposed. The suitability of both concepts to increase the software's reusability and, thus, its flexibility in the context of Industry 4.0 is discussed. Their comparison confirms the high potential of the object-oriented extension of IEC 61131-3 to handle planned reuse of extra-functional CPPS software successfully.
△ Less
Submitted 9 December, 2022;
originally announced December 2022.
-
MICOSE4aPS: Industrially Applicable Maturity Metric to Improve Systematic Reuse of Control Software
Authors:
Birgit Vogel-Heuser,
Eva-Maria Neumann,
Juliane Fischer
Abstract:
automated Production Systems (aPS) are highly complex, mechatronic systems that usually have to operate reliably for many decades. Standardization and reuse of control software modules is a core prerequisite to achieve the required system quality in increasingly shorter development cycles. However, industrial case studies in the field of aPS show that many aPS companies still struggle with strateg…
▽ More
automated Production Systems (aPS) are highly complex, mechatronic systems that usually have to operate reliably for many decades. Standardization and reuse of control software modules is a core prerequisite to achieve the required system quality in increasingly shorter development cycles. However, industrial case studies in the field of aPS show that many aPS companies still struggle with strategically reusing software. This paper proposes a metric-based approach to objectively measure the maturity of industrial IEC 61131-based control software in aPS (MICOSE4aPS) to identify potential weaknesses and quality issues hampering systematic reuse. Module developers in the machine and plant manufacturing industry can directly benefit as the metric calculation is integrated into the software engineering workflow. An in-depth industrial evaluation in a top-ranked machine manufacturing company in food packaging and an expert evaluation with different companies confirmed the benefit to efficiently manage the quality of control software.
△ Less
Submitted 9 December, 2022;
originally announced December 2022.
-
Bounding the Escape Time of a Linear Dynamical System over a Compact Semialgebraic Set
Authors:
Julian D'Costa,
Engel Lefaucheux,
Eike Neumann,
Joël Ouaknine,
James Worrell
Abstract:
We study the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets. We establish a uniform upper bound on the number of iterations it takes for every orbit of a rational matrix to escape a compact semialgebraic set defined over rational data. Our bound is doubly exponential in the ambient dimension, singly exponential in the degrees of the polynomials used to de…
▽ More
We study the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets. We establish a uniform upper bound on the number of iterations it takes for every orbit of a rational matrix to escape a compact semialgebraic set defined over rational data. Our bound is doubly exponential in the ambient dimension, singly exponential in the degrees of the polynomials used to define the semialgebraic set, and singly exponential in the bitsize of the coefficients of these polynomials and the bitsize of the matrix entries. We show that our bound is tight by providing a matching lower bound.
△ Less
Submitted 5 August, 2022; v1 submitted 4 July, 2022;
originally announced July 2022.
-
On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets
Authors:
Julian D'Costa,
Engel Lefaucheux,
Eike Neumann,
Joël Ouaknine,
James Worrell
Abstract:
We study the computational complexity of the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets, or equivalently the Termination Problem for affine loops with compact semialgebraic guard sets. Consider the fragment of the theory of the reals consisting of negation-free $\exists \forall$-sentences without strict inequalities. We derive several equivalent chara…
▽ More
We study the computational complexity of the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets, or equivalently the Termination Problem for affine loops with compact semialgebraic guard sets. Consider the fragment of the theory of the reals consisting of negation-free $\exists \forall$-sentences without strict inequalities. We derive several equivalent characterisations of the associated complexity class which demonstrate its robustness and illustrate its expressive power. We show that the Compact Escape Problem is complete for this class.
△ Less
Submitted 5 July, 2021;
originally announced July 2021.
-
Uniform Envelopes
Authors:
Eike Neumann
Abstract:
In the author's PhD thesis (2019) universal envelopes were introduced as a tool for studying the continuously obtainable information on discontinuous functions.
To any function $f \colon X \to Y$ between $\operatorname{qcb}_0$-spaces one can assign a so-called universal envelope which, in a well-defined sense, encodes all continuously obtainable information on the function. A universal envelope…
▽ More
In the author's PhD thesis (2019) universal envelopes were introduced as a tool for studying the continuously obtainable information on discontinuous functions.
To any function $f \colon X \to Y$ between $\operatorname{qcb}_0$-spaces one can assign a so-called universal envelope which, in a well-defined sense, encodes all continuously obtainable information on the function. A universal envelope consists of two continuous functions $F \colon X \to L$ and $ξ_L \colon Y \to L$ with values in a $Σ$-split injective space $L$. Any continuous function with values in an injective space whose composition with the original function is again continuous factors through the universal envelope. However, it is not possible in general to uniformly compute this factorisation.
In this paper we propose the notion of uniform envelopes. A uniform envelope is additionally endowed with a map $u_L \colon L \to \mathcal{O}^2(Y)$ that is compatible with the multiplication of the double powerspace monad $\mathcal{O}^2$ in a certain sense. This yields for every continuous map with values in an injective space a choice of uniformly computable extension. Under a suitable condition which we call uniform universality, this extension yields a uniformly computable solution for the above factorisation problem.
Uniform envelopes can be endowed with a composition operation. We establish criteria that ensure that the composition of two uniformly universal envelopes is again uniformly universal. These criteria admit a partial converse and we provide evidence that they cannot be easily improved in general.
Not every function admits a uniformly universal uniform envelope. We can however assign to every function a canonical envelope that is in some sense as close as possible to a uniform envelope. We obtain a composition theorem similar to the uniform case.
△ Less
Submitted 27 July, 2022; v1 submitted 30 March, 2021;
originally announced March 2021.
-
Decision problems for linear recurrences involving arbitrary real numbers
Authors:
Eike Neumann
Abstract:
We study the decidability of the Skolem Problem, the Positivity Problem, and the Ultimate Positivity Problem for linear recurrences with real number initial values and real number coefficients in the bit-model of real computation. We show that for each problem there exists a correct partial algorithm which halts for all problem instances for which the answer is locally constant, thus establishing…
▽ More
We study the decidability of the Skolem Problem, the Positivity Problem, and the Ultimate Positivity Problem for linear recurrences with real number initial values and real number coefficients in the bit-model of real computation. We show that for each problem there exists a correct partial algorithm which halts for all problem instances for which the answer is locally constant, thus establishing that all three problems are as close to decidable as one can expect them to be in this setting. We further show that the algorithms for the Positivity Problem and the Ultimate Positivity Problem halt on almost every instance with respect to the usual Lebesgue measure on Euclidean space. In comparison, the analogous problems for exact rational or real algebraic coefficients are known to be decidable only for linear recurrences of fairly low order.
△ Less
Submitted 9 August, 2021; v1 submitted 2 August, 2020;
originally announced August 2020.
-
Implementing evaluation strategies for continuous real functions
Authors:
Michal Konečný,
Eike Neumann
Abstract:
We give a technical overview of our exact-real implementation of various representations of the space of continuous unary real functions over the unit domain and a family of associated (partial) operations, including integration, range computation, as well as pointwise addition, multiplication, division, sine, cosine, square root and maximisation.
We use several representations close to the usua…
▽ More
We give a technical overview of our exact-real implementation of various representations of the space of continuous unary real functions over the unit domain and a family of associated (partial) operations, including integration, range computation, as well as pointwise addition, multiplication, division, sine, cosine, square root and maximisation.
We use several representations close to the usual theoretical model, based on an oracle that evaluates the function at a point or over an interval. We also include several representations based on an oracle that computes a converging sequence of rigorous (piecewise or one-piece) polynomial and rational approximations over the whole unit domain. Finally, we describe "local" representations that combine both approaches, i.e. oracle-like representations that return a rigorous symbolic approximation of the function over a requested interval sub-domain with a requested effort.
See also our paper "Representations and evaluation strategies for feasibly approximable functions" which compares the efficiency of these representations and algorithms and also formally describes and analyses one of the key algorithms, namely a polynomial-time division of functions in a piecewise-polynomial representation. We do not reproduce this division algorithm here.
△ Less
Submitted 10 October, 2019;
originally announced October 2019.
-
Parametrised second-order complexity theory with applications to the study of interval computation
Authors:
Eike Neumann,
Florian Steinberg
Abstract:
We extend the framework for complexity of operators in analysis devised by Kawamura and Cook (2012) to allow for the treatment of a wider class of representations. The main novelty is to endow represented spaces of interest with an additional function on names, called a parameter, which measures the complexity of a given name. This parameter generalises the size function which is usually used in s…
▽ More
We extend the framework for complexity of operators in analysis devised by Kawamura and Cook (2012) to allow for the treatment of a wider class of representations. The main novelty is to endow represented spaces of interest with an additional function on names, called a parameter, which measures the complexity of a given name. This parameter generalises the size function which is usually used in second-order complexity theory and therefore also central to the framework of Kawamura and Cook. The complexity of an algorithm is measured in terms of its running time as a second-order function in the parameter, as well as in terms of how much it increases the complexity of a given name, as measured by the parameters on the input and output side.
As an application we develop a rigorous computational complexity theory for interval computation. In the framework of Kawamura and Cook the representation of real numbers based on nested interval enclosures does not yield a reasonable complexity theory. In our new framework this representation is polytime equivalent to the usual Cauchy representation based on dyadic rational approximation. By contrast, the representation of continuous real functions based on interval enclosures is strictly smaller in the polytime reducibility lattice than the usual representation, which encodes a modulus of continuity. Furthermore, the function space representation based on interval enclosures is optimal in the sense that it contains the minimal amount of information amongst those representations which render evaluation polytime computable.
△ Less
Submitted 12 June, 2019; v1 submitted 28 November, 2017;
originally announced November 2017.
-
On the computability of the Fréchet distance of surfaces in the bit-model of real computation
Authors:
Eike Neumann
Abstract:
We show that the Fréchet distance of two-dimensional parametrised surfaces in a metric space is computable in the bit-model of real computation. An analogous result in the real RAM model for piecewise-linear surfaces has recently been obtained by Nayyeri and Xu (2016).
We show that the Fréchet distance of two-dimensional parametrised surfaces in a metric space is computable in the bit-model of real computation. An analogous result in the real RAM model for piecewise-linear surfaces has recently been obtained by Nayyeri and Xu (2016).
△ Less
Submitted 2 April, 2018; v1 submitted 6 November, 2017;
originally announced November 2017.
-
Representations and evaluation strategies for feasibly approximable functions
Authors:
Michal Konečný,
Eike Neumann
Abstract:
A famous result due to Ko and Friedman (1982) asserts that the problems of integration and maximisation of a univariate real function are computationally hard in a well-defined sense. Yet, both functionals are routinely computed at great speed in practice. We aim to resolve this apparent paradox by studying classes of functions which can be feasibly integrated and maximised, together with represen…
▽ More
A famous result due to Ko and Friedman (1982) asserts that the problems of integration and maximisation of a univariate real function are computationally hard in a well-defined sense. Yet, both functionals are routinely computed at great speed in practice. We aim to resolve this apparent paradox by studying classes of functions which can be feasibly integrated and maximised, together with representations for these classes of functions which encode the information which is necessary to uniformly compute integral and maximum in polynomial time. The theoretical framework for this is the second-order complexity theory for operators in analysis which was introduced by Kawamura and Cook (2012). The representations we study are based on rigorous approximation by polynomials, piecewise polynomials, and rational functions. We compare these representations with respect to polytime reducibility as well as with respect to their ability to quickly evaluate symbolic expressions in a given language. We show that the representation based on rigorous approximation by piecewise polynomials is polytime equivalent to the representation based on rigorous approximation by rational functions. With this representation, all terms in a certain language, which is expressive enough to contain the maximum and integral of most functions of practical interest, can be evaluated in polynomial time. By contrast, both the representation based on polynomial approximation and the standard representation based on function evaluation, which implicitly underlies the Ko-Friedman result, require exponential time to evaluate certain terms in this language. We confirm our theoretical results by an implementation in Haskell, which provides some evidence that second-order polynomial time computability is similarly closely tied with practical feasibility as its first-order counterpart.
△ Less
Submitted 21 October, 2019; v1 submitted 10 October, 2017;
originally announced October 2017.
-
Liveness Verification and Synthesis: New Algorithms for Recursive Programs
Authors:
Roland Meyer,
Sebastian Muskalla,
Elisabeth Neumann
Abstract:
We consider the problems of liveness verification and liveness synthesis for recursive programs. The liveness verification problem (LVP) is to decide whether a given omega-context-free language is contained in a given omega-regular language. The liveness synthesis problem (LSP) is to compute a strategy so that a given omega-context-free game, when played along the strategy, is guaranteed to derive…
▽ More
We consider the problems of liveness verification and liveness synthesis for recursive programs. The liveness verification problem (LVP) is to decide whether a given omega-context-free language is contained in a given omega-regular language. The liveness synthesis problem (LSP) is to compute a strategy so that a given omega-context-free game, when played along the strategy, is guaranteed to derive a word in a given omega-regular language. The problems are known to be EXPTIME-complete and EXPTIME-complete, respectively. Our contributions are new algorithms with optimal time complexity. For LVP, we generalize recent lasso-finding algorithms (also known as Ramsey-based algorithms) from finite to recursive programs. For LSP, we generalize a recent summary-based algorithm from finite to infinite words. Lasso finding and summaries have proven to be efficient in a number of implementations for the finite state and finite word setting.
△ Less
Submitted 11 January, 2017;
originally announced January 2017.
-
Computability in Basic Quantum Mechanics
Authors:
Eike Neumann,
Martin Pape,
Thomas Streicher
Abstract:
The basic notions of quantum mechanics are formulated in terms of separable infinite dimensional Hilbert space $\mathcal{H}$. In terms of the Hilbert lattice $\mathcal{L}$ of closed linear subspaces of $\mathcal{H}$ the notions of state and observable can be formulated as kinds of measures as in [21]. The aim of this paper is to show that there is a good notion of computability for these data stru…
▽ More
The basic notions of quantum mechanics are formulated in terms of separable infinite dimensional Hilbert space $\mathcal{H}$. In terms of the Hilbert lattice $\mathcal{L}$ of closed linear subspaces of $\mathcal{H}$ the notions of state and observable can be formulated as kinds of measures as in [21]. The aim of this paper is to show that there is a good notion of computability for these data structures in the sense of Weihrauch's Type Two Effectivity (TTE) [26].
Instead of explicitly exhibiting admissible representations for the data types under consideration we show that they do live within the category $\mathbf{QCB}_0$ which is equivalent to the category $\mathbf{AdmRep}$ of admissible representations and continuously realizable maps between them. For this purpose in case of observables we have to replace measures by valuations which allows us to prove an effective version of von Neumann's Spectral Theorem.
△ Less
Submitted 18 June, 2018; v1 submitted 27 October, 2016;
originally announced October 2016.
-
Median-of-k Jumplists and Dangling-Min BSTs
Authors:
Markus E. Nebel,
Elisabeth Neumann,
Sebastian Wild
Abstract:
We extend randomized jumplists introduced by Brönnimann et al. (STACS 2003) to choose jump-pointer targets as median of a small sample for better search costs, and present randomized algorithms with expected $O(\log n)$ time complexity that maintain the probability distribution of jump pointers upon insertions and deletions. We analyze the expected costs to search, insert and delete a random eleme…
▽ More
We extend randomized jumplists introduced by Brönnimann et al. (STACS 2003) to choose jump-pointer targets as median of a small sample for better search costs, and present randomized algorithms with expected $O(\log n)$ time complexity that maintain the probability distribution of jump pointers upon insertions and deletions. We analyze the expected costs to search, insert and delete a random element, and we show that omitting jump pointers in small sublists hardly affects search costs, but significantly reduces the memory consumption.
We use a bijection between jumplists and "dangling-min BSTs", a variant of (fringe-balanced) binary search trees for the analysis. Despite their similarities, some standard analysis techniques for search trees fail for dangling-min trees (and hence for jumplists).
△ Less
Submitted 30 October, 2018; v1 submitted 27 September, 2016;
originally announced September 2016.
-
Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
Authors:
Sewon Park,
Franz Brauße,
Pieter Collins,
SunYoung Kim,
Michal Konečný,
Gyesik Lee,
Norbert Müller,
Eike Neumann,
Norbert Preining,
Martin Ziegler
Abstract:
We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language-theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin po…
▽ More
We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language-theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin powerdomain and make our programming language semantics computable and complete: all and only real functions computable in computable analysis can be realized in ERC. The base programming language supports real arithmetic as well as implicit limits; expansions support additional primitive operations (such as a user-defined exponential function). By restricting integers to Presburger arithmetic and real coercion to the `precision' embedding $\mathbb{Z}\ni p\mapsto 2^p\in\mathbb{R}$, we arrive at a first-order theory which we prove to be decidable and model-complete. Based on said logic as specification language for preconditions and postconditions, we extend Hoare logic to a sound (w.r.t. the denotational semantics) and expressive system for deriving correct total correctness specifications. Various examples demonstrate the practicality and convenience of our language and the extended Hoare logic.
△ Less
Submitted 21 June, 2024; v1 submitted 20 August, 2016;
originally announced August 2016.
-
A topological view on algebraic computation models
Authors:
Eike Neumann,
Arno Pauly
Abstract:
We investigate the topological aspects of some algebraic computation models, in particular the BSS-model. Our results can be seen as bounds on how different BSS-computability and computability in the sense of computable analysis can be. The framework for this is Weihrauch reducibility. As a consequence of our characterizations, we establish that the solvability complexity index is (mostly) indepen…
▽ More
We investigate the topological aspects of some algebraic computation models, in particular the BSS-model. Our results can be seen as bounds on how different BSS-computability and computability in the sense of computable analysis can be. The framework for this is Weihrauch reducibility. As a consequence of our characterizations, we establish that the solvability complexity index is (mostly) independent of the computational model, and that there thus is common ground in the study of non-computability between the BSS and TTE setting.
△ Less
Submitted 17 March, 2017; v1 submitted 25 February, 2016;
originally announced February 2016.
-
Computational Problems in Metric Fixed Point Theory and their Weihrauch Degrees
Authors:
Eike Neumann
Abstract:
We study the computational difficulty of the problem of finding fixed points of nonexpansive map**s in uniformly convex Banach spaces. We show that the fixed point sets of computable nonexpansive self-maps of a nonempty, computably weakly closed, convex and bounded subset of a computable real Hilbert space are precisely the nonempty, co-r.e. weakly closed, convex subsets of the domain. A unifor…
▽ More
We study the computational difficulty of the problem of finding fixed points of nonexpansive map**s in uniformly convex Banach spaces. We show that the fixed point sets of computable nonexpansive self-maps of a nonempty, computably weakly closed, convex and bounded subset of a computable real Hilbert space are precisely the nonempty, co-r.e. weakly closed, convex subsets of the domain. A uniform version of this result allows us to determine the Weihrauch degree of the Browder-Goehde-Kirk theorem in computable real Hilbert space: it is equivalent to a closed choice principle, which receives as input a closed, convex and bounded set via negative information in the weak topology and outputs a point in the set, represented in the strong topology. While in finite dimensional uniformly convex Banach spaces, computable nonexpansive map**s always have computable fixed points, on the unit ball in infinite-dimensional separable Hilbert space the Browder-Goehde-Kirk theorem becomes Weihrauch-equivalent to the limit operator, and on the Hilbert cube it is equivalent to Weak Koenig's Lemma. In particular, computable nonexpansive map**s may not have any computable fixed points in infinite dimension. We also study the computational difficulty of the problem of finding rates of convergence for a large class of fixed point iterations, which generalise both Halpern- and Mann-iterations, and prove that the problem of finding rates of convergence already on the unit interval is equivalent to the limit operator.
△ Less
Submitted 27 December, 2015; v1 submitted 16 June, 2015;
originally announced June 2015.
