Showing 1–50 of 59 results for author: Weiß, A

Finite groups with geodetic Cayley graphs

Authors: Murray Elder, Adam Piggott, Florian Stober, Alexander Thumm, Armin Weiß

Abstract: A connected undirected graph is called \emph{geodetic} if for every pair of vertices there is a unique shortest path connecting them. It has been conjectured that for finite groups, the only geodetic Cayley graphs which occur are odd cycles and complete graphs. In this article we present a series of theoretical results which contribute to a computer search verifying this conjecture for all groups… ▽ More A connected undirected graph is called \emph{geodetic} if for every pair of vertices there is a unique shortest path connecting them. It has been conjectured that for finite groups, the only geodetic Cayley graphs which occur are odd cycles and complete graphs. In this article we present a series of theoretical results which contribute to a computer search verifying this conjecture for all groups of size up to 1024. The conjecture is also verified theoretically for several infinite families of groups including dihedral and some families of nilpotent groups. Two key results which enable the computer search to reach as far as it does are: if the center of a group has even order, then the conjecture holds (this eliminates all 2-groups from our computer search); if a Cayley graph is geodetic then there are bounds relating the size of the group, generating set and center (which cuts down the number of generating sets which must be searched significantly). △ Less

Submitted 31 May, 2024; originally announced June 2024.

Comments: 26 pages, 4 tables, 3 figures

MSC Class: 05C12; 05C25; 20F05

An Analysis of the Math Requirements of 199 CS BS/BA Degrees at 158 U.S. Universities

Authors: Carla E. Brodley, McKenna Quam, Mark A. Weiss

Abstract: For at least 40 years, there has been debate and disagreement as to the role of mathematics in the computer science curriculum. This paper presents the results of an analysis of the math requirements of 199 Computer Science BS/BA degrees from 158 U.S. universities, looking not only at which math courses are required, but how they are used as prerequisites (and corequisites) for computer science (C… ▽ More For at least 40 years, there has been debate and disagreement as to the role of mathematics in the computer science curriculum. This paper presents the results of an analysis of the math requirements of 199 Computer Science BS/BA degrees from 158 U.S. universities, looking not only at which math courses are required, but how they are used as prerequisites (and corequisites) for computer science (CS) courses. Our analysis shows that while there is consensus that discrete math is critical for a CS degree, and further that calculus is almost always required for the BS in CS, there is little consensus as to when a student should have mastered these subjects. Based on our analysis of how math requirements impact access, retention and on-time degree completion for the BS and the BA in CS, we provide several recommendations for CS departments to consider. △ Less

Submitted 23 April, 2024; originally announced April 2024.

Comments: 13 pages, accepted to Communications of the ACM

ACM Class: K.3.2

Projection-free computation of robust controllable sets with constrained zonotopes

Authors: Abraham P. Vinod, Avishai Weiss, Stefano Di Cairano

Abstract: We study the problem of computing robust controllable sets for discrete-time linear systems with additive uncertainty. We propose a tractable and scalable approach to inner- and outer-approximate robust controllable sets using constrained zonotopes, when the additive uncertainty set is a symmetric, convex, and compact set. Our least-squares-based approach uses novel closed-form approximations of t… ▽ More We study the problem of computing robust controllable sets for discrete-time linear systems with additive uncertainty. We propose a tractable and scalable approach to inner- and outer-approximate robust controllable sets using constrained zonotopes, when the additive uncertainty set is a symmetric, convex, and compact set. Our least-squares-based approach uses novel closed-form approximations of the Pontryagin difference between a constrained zonotopic minuend and a symmetric, convex, and compact subtrahend. Unlike existing approaches, our approach does not rely on convex optimization solvers, and is projection-free for ellipsoidal and zonotopic uncertainty sets. We also propose a least-squares-based approach to compute a convex, polyhedral outer-approximation to constrained zonotopes, and characterize sufficient conditions under which all these approximations are exact. We demonstrate the computational efficiency and scalability of our approach in several case studies, including the design of abort-safe rendezvous trajectories for a spacecraft in near-rectilinear halo orbit under uncertainty. Our approach can inner-approximate a 20-step robust controllable set for a 100-dimensional linear system in under 15 seconds on a standard computer. △ Less

Submitted 20 March, 2024; originally announced March 2024.

Comments: 22 pages, 6 figures

FlashTex: Fast Relightable Mesh Texturing with LightControlNet

Authors: Kangle Deng, Timothy Omernick, Alexander Weiss, Deva Ramanan, Jun-Yan Zhu, Tinghui Zhou, Maneesh Agrawala

Abstract: Manually creating textures for 3D meshes is time-consuming, even for expert visual content creators. We propose a fast approach for automatically texturing an input 3D mesh based on a user-provided text prompt. Importantly, our approach disentangles lighting from surface material/reflectance in the resulting texture so that the mesh can be properly relit and rendered in any lighting environment. W… ▽ More Manually creating textures for 3D meshes is time-consuming, even for expert visual content creators. We propose a fast approach for automatically texturing an input 3D mesh based on a user-provided text prompt. Importantly, our approach disentangles lighting from surface material/reflectance in the resulting texture so that the mesh can be properly relit and rendered in any lighting environment. We introduce LightControlNet, a new text-to-image model based on the ControlNet architecture, which allows the specification of the desired lighting as a conditioning image to the model. Our text-to-texture pipeline then constructs the texture in two stages. The first stage produces a sparse set of visually consistent reference views of the mesh using LightControlNet. The second stage applies a texture optimization based on Score Distillation Sampling (SDS) that works with LightControlNet to increase the texture quality while disentangling surface material from lighting. Our algorithm is significantly faster than previous text-to-texture methods, while producing high-quality and relightable textures. △ Less

Submitted 22 April, 2024; v1 submitted 20 February, 2024; originally announced February 2024.

Comments: Project page: https://flashtex.github.io/

On the Constant-Depth Circuit Complexity of Generating Quasigroups

Authors: Nathaniel A. Collins, Joshua A. Grochow, Michael Levet, Armin Weiß

Abstract: We investigate the constant-depth circuit complexity of the Isomorphism Problem, Minimum Generating Set Problem (MGS), and Sub(quasi)group Membership Problem (Membership) for groups and quasigroups (=Latin squares), given as input in terms of their multiplication (Cayley) tables. Despite decades of research on these problems, lower bounds for these problems even against depth-$2$ AC circuits remai… ▽ More We investigate the constant-depth circuit complexity of the Isomorphism Problem, Minimum Generating Set Problem (MGS), and Sub(quasi)group Membership Problem (Membership) for groups and quasigroups (=Latin squares), given as input in terms of their multiplication (Cayley) tables. Despite decades of research on these problems, lower bounds for these problems even against depth-$2$ AC circuits remain unknown. Perhaps surprisingly, Chattopadhyay, Torán, and Wagner (FSTTCS 2010; ACM Trans. Comput. Theory, 2013) showed that Quasigroup Isomorphism could be solved by AC circuits of depth $O(\log \log n)$ using $O(\log^2 n)$ nondeterministic bits, a class we denote $\exists^{\log^2(n)}FOLL$. We narrow this gap by improving the upper bound for many of these problems to $quasiAC^0$, thus decreasing the depth to constant. In particular, we show: - MGS for quasigroups is in $\exists^{\log^2(n)}\forall^{\log n}NTIME(\mathrm{polylog}(n))\subseteq quasiAC^0$. Papadimitriou and Yannakakis (J. Comput. Syst. Sci., 1996) conjectured that this problem was $\exists^{\log^2(n)}P$-complete; our results refute a version of that conjecture for completeness under $quasiAC^0$ reductions unconditionally, and under polylog-space reductions assuming EXP $\neq$ PSPACE. - MGS for groups is in $AC^{1}(L)$, improving on the previous upper bound of $P$ (Lucchini & Thakkar, J. Algebra, 2024). - Quasigroup Isomorphism belongs to $\exists^{\log^2(n)}AC^0(DTISP(\mathrm{polylog},\log)\subseteq quasiAC^0$, improving on the previous bound of $\exists^{\log^2(n)}L\cap\exists^{\log^2(n)}FOLL\subseteq quasiFOLL$ (Chattopadhyay, Torán, & Wagner, ibid.; Levet, Australas. J. Combin., 2023). Our results suggest that understanding the constant-depth circuit complexity may be key to resolving the complexity of problems concerning (quasi)groups in the multiplication table model. △ Less

Submitted 23 April, 2024; v1 submitted 31 January, 2024; originally announced February 2024.

Comments: Full version of paper to appear in ISSAC 2024

Violating Constant Degree Hypothesis Requires Breaking Symmetry

Authors: Piotr Kawałek, Armin Weiß

Abstract: The Constant Degree Hypothesis was introduced by Barrington et. al. (1990) to study some extensions of $q$-groups by nilpotent groups and the power of these groups in a certain computational model. In its simplest formulation, it establishes exponential lower bounds for $\mathrm{AND}_d \circ \mathrm{MOD}_m \circ \mathrm{MOD}_q$ circuits computing AND of unbounded arity $n$ (for constant integers… ▽ More The Constant Degree Hypothesis was introduced by Barrington et. al. (1990) to study some extensions of $q$-groups by nilpotent groups and the power of these groups in a certain computational model. In its simplest formulation, it establishes exponential lower bounds for $\mathrm{AND}_d \circ \mathrm{MOD}_m \circ \mathrm{MOD}_q$ circuits computing AND of unbounded arity $n$ (for constant integers $d,m$ and a prime $q$). While it has been proved in some special cases (including $d=1$), it remains wide open in its general form for over 30 years. In this paper we prove that the hypothesis holds when we restrict our attention to symmetric circuits with $m$ being a prime. While we build upon techniques by Grolmusz and Tardos (2000), we have to prove a new symmetric version of their Degree Decreasing Lemma and apply it in a highly non-trivial way. Moreover, to establish the result we perform a careful analysis of automorphism groups of $\mathrm{AND} \circ \mathrm{MOD}_m$ subcircuits and study the periodic behaviour of the computed functions. Finally, our methods also yield lower bounds when $d$ is treated as a function of $n$. △ Less

Submitted 29 November, 2023; originally announced November 2023.

MSC Class: 68Q06; 68Q17; 68Q15 ACM Class: F.1.3

Complexity of Spherical Equations in Finite Groups

Authors: Caroline Mattes, Alexander Ushakov, Armin Weiß

Abstract: In this paper we investigate computational properties of the Diophantine problem for spherical equations in some classes of finite groups. We classify the complexity of different variations of the problem, e.g., when $G$ is fixed and when $G$ is a part of the input. When the group $G$ is constant or given as multiplication table, we show that the problem always can be solved in polynomial time.… ▽ More In this paper we investigate computational properties of the Diophantine problem for spherical equations in some classes of finite groups. We classify the complexity of different variations of the problem, e.g., when $G$ is fixed and when $G$ is a part of the input. When the group $G$ is constant or given as multiplication table, we show that the problem always can be solved in polynomial time. On the other hand, for the permutation groups $S_n$ (with $n$ part of the input), the problem is NP-complete. The situation for matrix groups is quite involved: while we exhibit sequences of 2-by-2 matrices where the problem is NP-complete, in the full group $GL(2,p)$ ($p$ prime and part of the input) it can be solved in polynomial time. We also find a similar behaviour with subgroups of matrices of arbitrary dimension over a constant ring. △ Less

Submitted 24 August, 2023; originally announced August 2023.

MSC Class: 20F10; 68W30

Geodetic Graphs: Experiments and New Constructions

Authors: Florian Stober, Armin Weiß

Abstract: In 1962 Ore initiated the study of geodetic graphs. A graph is called geodetic if the shortest path between every pair of vertices is unique. In the subsequent years a wide range of papers appeared investigating their peculiar properties. Yet, a complete classification of geodetic graphs is out of reach. In this work we present a program enumerating all geodetic graphs of a given size. Using our… ▽ More In 1962 Ore initiated the study of geodetic graphs. A graph is called geodetic if the shortest path between every pair of vertices is unique. In the subsequent years a wide range of papers appeared investigating their peculiar properties. Yet, a complete classification of geodetic graphs is out of reach. In this work we present a program enumerating all geodetic graphs of a given size. Using our program, we succeed to find all geodetic graphs with up to 25 vertices and all regular geodetic graphs with up to 32 vertices. This leads to the discovery of two new infinite families of geodetic graphs. △ Less

Submitted 17 August, 2023; originally announced August 2023.

Score-based Source Separation with Applications to Digital Communication Signals

Authors: Tejas Jayashankar, Gary C. F. Lee, Alejandro Lancho, Amir Weiss, Yury Polyanskiy, Gregory W. Wornell

Abstract: We propose a new method for separating superimposed sources using diffusion-based generative models. Our method relies only on separately trained statistical priors of independent sources to establish a new objective function guided by maximum a posteriori estimation with an $α$-posterior, across multiple levels of Gaussian smoothing. Motivated by applications in radio-frequency (RF) systems, we a… ▽ More We propose a new method for separating superimposed sources using diffusion-based generative models. Our method relies only on separately trained statistical priors of independent sources to establish a new objective function guided by maximum a posteriori estimation with an $α$-posterior, across multiple levels of Gaussian smoothing. Motivated by applications in radio-frequency (RF) systems, we are interested in sources with underlying discrete nature and the recovery of encoded bits from a signal of interest, as measured by the bit error rate (BER). Experimental results with RF mixtures demonstrate that our method results in a BER reduction of 95% over classical and existing learning-based methods. Our analysis demonstrates that our proposed method yields solutions that asymptotically approach the modes of an underlying discrete distribution. Furthermore, our method can be viewed as a multi-source extension to the recently proposed score distillation sampling scheme, shedding additional light on its use beyond conditional sampling. The project webpage is available at https://alpha-rgs.github.io △ Less

Submitted 17 January, 2024; v1 submitted 26 June, 2023; originally announced June 2023.

Comments: 34 pages, 18 figures, for associated project webpage see https://alpha-rgs.github.io

A Bilateral Bound on the Mean-Square Error for Estimation in Model Mismatch

Authors: Amir Weiss, Alejandro Lancho, Yuheng Bu, Gregory W. Wornell

Abstract: A bilateral (i.e., upper and lower) bound on the mean-square error under a general model mismatch is developed. The bound, which is derived from the variational representation of the chi-square divergence, is applicable in the Bayesian and nonBayesian frameworks to biased and unbiased estimators. Unlike other classical MSE bounds that depend only on the model, our bound is also estimator-dependent… ▽ More A bilateral (i.e., upper and lower) bound on the mean-square error under a general model mismatch is developed. The bound, which is derived from the variational representation of the chi-square divergence, is applicable in the Bayesian and nonBayesian frameworks to biased and unbiased estimators. Unlike other classical MSE bounds that depend only on the model, our bound is also estimator-dependent. Thus, it is applicable as a tool for characterizing the MSE of a specific estimator. The proposed bounding technique has a variety of applications, one of which is a tool for proving the consistency of estimators for a class of models. Furthermore, it provides insight as to why certain estimators work well under general model mismatch conditions. △ Less

Submitted 14 May, 2023; originally announced May 2023.

Comments: Accepted for publication in Proc. of ISIT 2023

The University of California San Francisco Brain Metastases Stereotactic Radiosurgery (UCSF-BMSR) MRI Dataset

Authors: Jeffrey D. Rudie, Rachit Saluja, David A. Weiss, Pierre Nedelec, Evan Calabrese, John B. Colby, Benjamin Laguna, John Mongan, Steve Braunstein, Christopher P. Hess, Andreas M. Rauschecker, Leo P. Sugrue, Javier E. Villanueva-Meyer

Abstract: The University of California San Francisco Brain Metastases Stereotactic Radiosurgery (UCSF-BMSR) dataset is a public, clinical, multimodal brain MRI dataset consisting of 560 brain MRIs from 412 patients with expert annotations of 5136 brain metastases. Data consists of registered and skull stripped T1 post-contrast, T1 pre-contrast, FLAIR and subtraction (T1 pre-contrast - T1 post-contrast) imag… ▽ More The University of California San Francisco Brain Metastases Stereotactic Radiosurgery (UCSF-BMSR) dataset is a public, clinical, multimodal brain MRI dataset consisting of 560 brain MRIs from 412 patients with expert annotations of 5136 brain metastases. Data consists of registered and skull stripped T1 post-contrast, T1 pre-contrast, FLAIR and subtraction (T1 pre-contrast - T1 post-contrast) images and voxelwise segmentations of enhancing brain metastases in NifTI format. The dataset also includes patient demographics, surgical status and primary cancer types. The UCSF-BSMR has been made publicly available in the hopes that researchers will use these data to push the boundaries of AI applications for brain metastases. The dataset is freely available for non-commercial use at https://imagingdatasets.ucsf.edu/dataset/1 △ Less

Submitted 30 May, 2024; v1 submitted 14 April, 2023; originally announced April 2023.

Comments: 15 pages, 2 tables, 2 figures

Journal ref: Radiology: Artificial Intelligence. 2024;6(2):e230126

On Neural Architectures for Deep Learning-based Source Separation of Co-Channel OFDM Signals

Authors: Gary C. F. Lee, Amir Weiss, Alejandro Lancho, Yury Polyanskiy, Gregory W. Wornell

Abstract: We study the single-channel source separation problem involving orthogonal frequency-division multiplexing (OFDM) signals, which are ubiquitous in many modern-day digital communication systems. Related efforts have been pursued in monaural source separation, where state-of-the-art neural architectures have been adopted to train an end-to-end separator for audio signals (as 1-dimensional time serie… ▽ More We study the single-channel source separation problem involving orthogonal frequency-division multiplexing (OFDM) signals, which are ubiquitous in many modern-day digital communication systems. Related efforts have been pursued in monaural source separation, where state-of-the-art neural architectures have been adopted to train an end-to-end separator for audio signals (as 1-dimensional time series). In this work, through a prototype problem based on the OFDM source model, we assess -- and question -- the efficacy of using audio-oriented neural architectures in separating signals based on features pertinent to communication waveforms. Perhaps surprisingly, we demonstrate that in some configurations, where perfect separation is theoretically attainable, these audio-oriented neural architectures perform poorly in separating co-channel OFDM waveforms. Yet, we propose critical domain-informed modifications to the network parameterization, based on insights from OFDM structures, that can confer about 30 dB improvement in performance. △ Less

Submitted 15 March, 2023; v1 submitted 11 March, 2023; originally announced March 2023.

Can Shadows Reveal Biometric Information?

Authors: Safa C. Medin, Amir Weiss, Frédo Durand, William T. Freeman, Gregory W. Wornell

Abstract: We study the problem of extracting biometric information of individuals by looking at shadows of objects cast on diffuse surfaces. We show that the biometric information leakage from shadows can be sufficient for reliable identity inference under representative scenarios via a maximum likelihood analysis. We then develop a learning-based method that demonstrates this phenomenon in real settings, e… ▽ More We study the problem of extracting biometric information of individuals by looking at shadows of objects cast on diffuse surfaces. We show that the biometric information leakage from shadows can be sufficient for reliable identity inference under representative scenarios via a maximum likelihood analysis. We then develop a learning-based method that demonstrates this phenomenon in real settings, exploiting the subtle cues in the shadows that are the source of the leakage without requiring any labeled real data. In particular, our approach relies on building synthetic scenes composed of 3D face models obtained from a single photograph of each identity. We transfer what we learn from the synthetic data to the real data using domain adaptation in a completely unsupervised way. Our model is able to generalize well to the real domain and is robust to several variations in the scenes. We report high classification accuracies in an identity classification task that takes place in a scene with unknown geometry and occluding objects. △ Less

Submitted 4 October, 2022; v1 submitted 20 September, 2022; originally announced September 2022.

Data-Driven Blind Synchronization and Interference Rejection for Digital Communication Signals

Authors: Alejandro Lancho, Amir Weiss, Gary C. F. Lee, Jennifer Tang, Yuheng Bu, Yury Polyanskiy, Gregory W. Wornell

Abstract: We study the potential of data-driven deep learning methods for separation of two communication signals from an observation of their mixture. In particular, we assume knowledge on the generation process of one of the signals, dubbed signal of interest (SOI), and no knowledge on the generation process of the second signal, referred to as interference. This form of the single-channel source separati… ▽ More We study the potential of data-driven deep learning methods for separation of two communication signals from an observation of their mixture. In particular, we assume knowledge on the generation process of one of the signals, dubbed signal of interest (SOI), and no knowledge on the generation process of the second signal, referred to as interference. This form of the single-channel source separation problem is also referred to as interference rejection. We show that capturing high-resolution temporal structures (nonstationarities), which enables accurate synchronization to both the SOI and the interference, leads to substantial performance gains. With this key insight, we propose a domain-informed neural network (NN) design that is able to improve upon both "off-the-shelf" NNs and classical detection and interference rejection methods, as demonstrated in our simulations. Our findings highlight the key role communication-specific domain knowledge plays in the development of data-driven approaches that hold the promise of unprecedented gains. △ Less

Submitted 11 September, 2022; originally announced September 2022.

Comments: 9 pages, 6 figures, accepted at IEEE GLOBECOM 2022 (this version contains extended proofs)

A Polynomial Decision for 3-SAT

Authors: Angela Weiss

Abstract: We propose a polynomially bounded, in time and space, method to decide whether a given 3-SAT formula is satisfiable or not. The tools we use here are, in fact, very simple. We first decide satisfiability for a particular 3-SAT formula, called pivoted 3-SAT and, after a plain transformation, still kee** the polynomial boundaries, it is shown that 3-SAT formulas can be written as pivoted formulas. We propose a polynomially bounded, in time and space, method to decide whether a given 3-SAT formula is satisfiable or not. The tools we use here are, in fact, very simple. We first decide satisfiability for a particular 3-SAT formula, called pivoted 3-SAT and, after a plain transformation, still kee** the polynomial boundaries, it is shown that 3-SAT formulas can be written as pivoted formulas. △ Less

Submitted 7 June, 2024; v1 submitted 20 August, 2022; originally announced August 2022.

Comments: Revisited version. Short proofs

Exploiting Temporal Structures of Cyclostationary Signals for Data-Driven Single-Channel Source Separation

Authors: Gary C. F. Lee, Amir Weiss, Alejandro Lancho, Jennifer Tang, Yuheng Bu, Yury Polyanskiy, Gregory W. Wornell

Abstract: We study the problem of single-channel source separation (SCSS), and focus on cyclostationary signals, which are particularly suitable in a variety of application domains. Unlike classical SCSS approaches, we consider a setting where only examples of the sources are available rather than their models, inspiring a data-driven approach. For source models with underlying cyclostationary Gaussian cons… ▽ More We study the problem of single-channel source separation (SCSS), and focus on cyclostationary signals, which are particularly suitable in a variety of application domains. Unlike classical SCSS approaches, we consider a setting where only examples of the sources are available rather than their models, inspiring a data-driven approach. For source models with underlying cyclostationary Gaussian constituents, we establish a lower bound on the attainable mean squared error (MSE) for any separation method, model-based or data-driven. Our analysis further reveals the operation for optimal separation and the associated implementation challenges. As a computationally attractive alternative, we propose a deep learning approach using a U-Net architecture, which is competitive with the minimum MSE estimator. We demonstrate in simulation that, with suitable domain-informed architectural choices, our U-Net method can approach the optimal performance with substantially reduced computational burden. △ Less

Submitted 22 August, 2022; originally announced August 2022.

Direct Localization in Underwater Acoustics via Convolutional Neural Networks: A Data-Driven Approach

Authors: Amir Weiss, Toros Arikan, Gregory W. Wornell

Abstract: Direct localization (DLOC) methods, which use the observed data to localize a source at an unknown position in a one-step procedure, generally outperform their indirect two-step counterparts (e.g., using time-difference of arrivals). However, underwater acoustic DLOC methods require prior knowledge of the environment, and are computationally costly, hence slow. We propose, what is to the best of o… ▽ More Direct localization (DLOC) methods, which use the observed data to localize a source at an unknown position in a one-step procedure, generally outperform their indirect two-step counterparts (e.g., using time-difference of arrivals). However, underwater acoustic DLOC methods require prior knowledge of the environment, and are computationally costly, hence slow. We propose, what is to the best of our knowledge, the first data-driven DLOC method. Inspired by classical and contemporary optimal model-based DLOC solutions, and leveraging the capabilities of convolutional neural networks (CNNs), we devise a holistic CNN-based solution. Our method includes a specifically-tailored input structure, architecture, loss function, and a progressive training procedure, which are of independent interest in the broader context of machine learning. We demonstrate that our method outperforms attractive alternatives, and asymptotically matches the performance of an oracle optimal model-based solution. △ Less

Submitted 20 July, 2022; originally announced July 2022.

Lower Bounds for Sorting 16, 17, and 18 Elements

Authors: Florian Stober, Armin Weiß

Abstract: It is a long-standing open question to determine the minimum number of comparisons $S(n)$ that suffice to sort an array of $n$ elements. Indeed, before this work $S(n)$ has been known only for $n\leq 22$ with the exception for $n=16$, $17$, and $18$. In this work, we fill that gap by proving that sorting $n=16$, $17$, and $18$ elements requires $46$, $50$, and $54$ comparisons respectively. This f… ▽ More It is a long-standing open question to determine the minimum number of comparisons $S(n)$ that suffice to sort an array of $n$ elements. Indeed, before this work $S(n)$ has been known only for $n\leq 22$ with the exception for $n=16$, $17$, and $18$. In this work, we fill that gap by proving that sorting $n=16$, $17$, and $18$ elements requires $46$, $50$, and $54$ comparisons respectively. This fully determines $S(n)$ for these values and disproves a conjecture by Knuth that $S(16) = 45$. Moreover, we show that for sorting $28$ elements at least 99 comparisons are needed. We obtain our result via an exhaustive computer search which extends previous work by Wells (1965) and Peczarski (2002, 2004, 2007, 2012). Our progress is both based on advances in hardware and on novel algorithmic ideas such as applying a bidirectional search to this problem. △ Less

Submitted 18 November, 2022; v1 submitted 11 June, 2022; originally announced June 2022.

The Power Word Problem in Graph Products

Authors: Markus Lohrey, Florian Stober, Armin Weiß

Abstract: The power word problem for a group $G$ asks whether an expression $u_1^{x_1} \cdots u_n^{x_n}$, where the $u_i$ are words over a finite set of generators of $G$ and the $x_i$ binary encoded integers, is equal to the identity of $G$. It is a restriction of the compressed word problem, where the input word is represented by a straight-line program (i.e., an algebraic circuit over $G$). We start by s… ▽ More The power word problem for a group $G$ asks whether an expression $u_1^{x_1} \cdots u_n^{x_n}$, where the $u_i$ are words over a finite set of generators of $G$ and the $x_i$ binary encoded integers, is equal to the identity of $G$. It is a restriction of the compressed word problem, where the input word is represented by a straight-line program (i.e., an algebraic circuit over $G$). We start by showing some easy results concerning the power word problem. In particular, the power word problem for a group $G$ is $NC^1$-many-one reducible to the power word problem for a finite-index subgroup of $G$. For our main result, we consider graph products of groups that do not have elements of order two. We show that the power word problem in a fixed such graph product is $AC^0$-Turing-reducible to the word problem for the free group $F_2$ and the power word problems of the base groups. Furthermore, we look into the uniform power word problem in a graph product, where the dependence graph and the base groups are part of the input. Given a class of finitely generated groups $\mathcal{C}$ without order two elements, the uniform power word problem in a graph product can be solved in $\mathsf{AC^0(C_=L^{UPowWP(\mathcal{C})})}$, where $UPowWP(\mathcal{C})$ denotes the uniform power word problem for groups from the class $\mathcal{C}$. As a consequence of our results, the uniform knapsack problem in right-angled Artin groups is NP-complete. The present paper is a combination of the two conference papers. In [StoberW22] and previous iterations of this paper our results on graph products were wrongly stated without the additional assumption that the base groups do not have elements of order two. In the present work we correct this mistake. While we strongly conjecture that the result as stated previously is true, our proof relies on this additional assumption. △ Less

Submitted 12 January, 2023; v1 submitted 17 January, 2022; originally announced January 2022.

Comments: Version 3 fixes a mistake in the previous versions. There our results on graph products were wrongly stated without the additional assumption that the base groups do not have elements of order two. Version 3 also includes some content from arXiv:1904.08343

Blind Modulo Analog-to-Digital Conversion of Vector Processes

Authors: Amir Weiss, Everest Huang, Or Ordentlich, Gregory W. Wornell

Abstract: In a growing number of applications, there is a need to digitize a (possibly high) number of correlated signals whose spectral characteristics are challenging for traditional analog-to-digital converters (ADCs). Examples, among others, include multiple-input multiple-output systems where the ADCs must acquire at once several signals at a very wide but sparsely and dynamically occupied bandwidth su… ▽ More In a growing number of applications, there is a need to digitize a (possibly high) number of correlated signals whose spectral characteristics are challenging for traditional analog-to-digital converters (ADCs). Examples, among others, include multiple-input multiple-output systems where the ADCs must acquire at once several signals at a very wide but sparsely and dynamically occupied bandwidth supporting diverse services. In such scenarios, the resolution requirements can be prohibitively high. As an alternative, the recently proposed modulo-ADC architecture can in principle require dramatically fewer bits in the conversion to obtain the target fidelity, but requires that spatiotemporal information be known and explicitly taken into account by the analog and digital processing in the converter, which is frequently impractical. Building on our recent work, we address this limitation and develop a blind version of the architecture that requires no such knowledge in the converter. In particular, it features an automatic modulo-level adjustment and a fully adaptive modulo-decoding mechanism, allowing it to asymptotically match the characteristics of the unknown input signal. Simulation results demonstrate the successful operation of the proposed algorithm. △ Less

Submitted 12 October, 2021; originally announced October 2021.

Comments: arXiv admin note: substantial text overlap with arXiv:2108.08937

The isomorphism problem for plain groups is in $Σ_3^{\mathsf{P}}$

Authors: Heiko Dietrich, Murray Elder, Adam Piggott, Youming Qiao, Armin Weiß

Abstract: Testing isomorphism of infinite groups is a classical topic, but from the complexity theory viewpoint, few results are known. S{é}nizergues and the fifth author (ICALP2018) proved that the isomorphism problem for virtually free groups is decidable in $\mathsf{PSPACE}$ when the input is given in terms of so-called virtually free presentations. Here we consider the isomorphism problem for the class… ▽ More Testing isomorphism of infinite groups is a classical topic, but from the complexity theory viewpoint, few results are known. S{é}nizergues and the fifth author (ICALP2018) proved that the isomorphism problem for virtually free groups is decidable in $\mathsf{PSPACE}$ when the input is given in terms of so-called virtually free presentations. Here we consider the isomorphism problem for the class of \emph{plain groups}, that is, groups that are isomorphic to a free product of finitely many finite groups and finitely many copies of the infinite cyclic group. Every plain group is naturally and efficiently presented via an inverse-closed finite convergent length-reducing rewriting system. We prove that the isomorphism problem for plain groups given in this form lies in the polynomial time hierarchy, more precisely, in $Σ_3^{\mathsf{P}}$. This result is achieved by combining new geometric and algebraic characterisations of groups presented by inverse-closed finite convergent length-reducing rewriting systems developed in recent work of the second and third authors (2021) with classical finite group isomorphism results of Babai and Szemerédi (1984). △ Less

Submitted 17 January, 2022; v1 submitted 2 October, 2021; originally announced October 2021.

Comments: 11 pages, 0 figures. Accepted in STACS2022

MSC Class: 20E06; 20F65; 68Q15; 68Q42

A Framework for Develo** Algorithms for Estimating Propagation Parameters from Measurements

Authors: Akbar Sayeed, Peter Vouras, Camillo Gentile, Alec Weiss, Jeanne Quimby, Zihang Cheng, Bassel Modad, Yuning Zhang, Chethan An**appa, Fatih Erden, Ozgur Ozdemir, Robert Muller, Diego Dupleich, Han Niu, 6David Michelson, 6Aidan Hughes

Abstract: A framework is proposed for develo** and evaluating algorithms for extracting multipath propagation components (MPCs) from measurements collected by sounders at millimeter-wave (mmW) frequencies. To focus on algorithmic performance, an idealized model is proposed for the spatial frequency response of the propagation environment measured by a sounder. The input to the sounder model is a pre-deter… ▽ More A framework is proposed for develo** and evaluating algorithms for extracting multipath propagation components (MPCs) from measurements collected by sounders at millimeter-wave (mmW) frequencies. To focus on algorithmic performance, an idealized model is proposed for the spatial frequency response of the propagation environment measured by a sounder. The input to the sounder model is a pre-determined set of MPC parameters that serve as the "ground truth." A three-dimensional angle-delay (beamspace) representation of the measured spatial frequency response serves as a natural domain for implementing and analyzing MPC extraction algorithms. Metrics for quantifying the error in estimated MPC parameters are introduced. Initial results are presented for a greedy matching pursuit algorithm that performs a least-squares (LS) reconstruction of the MPC path gains within the iterations. The results indicate that the simple greedy-LS algorithm has the ability to extract MPCs over a large dynamic range, and suggest several avenues for further performance improvement through extensions of the greedy-LS algorithm as well as by incorporating features of other algorithms, such as SAGE and RIMAX. △ Less

Submitted 13 September, 2021; originally announced September 2021.

Journal ref: IEEE Globecom 2020

Parallel algorithms for power circuits and the word problem of the Baumslag group

Authors: Caroline Mattes, Armin Weiß

Abstract: Power circuits have been introduced in 2012 by Myasnikov, Ushakov and Won as a data structure for non-elementarily compressed integers supporting the arithmetic operations addition and $(x,y) \mapsto x\cdot 2^y$. The same authors applied power circuits to give a polynomial-time solution to the word problem of the Baumslag group, which has a non-elementary Dehn function. In this work, we examine… ▽ More Power circuits have been introduced in 2012 by Myasnikov, Ushakov and Won as a data structure for non-elementarily compressed integers supporting the arithmetic operations addition and $(x,y) \mapsto x\cdot 2^y$. The same authors applied power circuits to give a polynomial-time solution to the word problem of the Baumslag group, which has a non-elementary Dehn function. In this work, we examine power circuits and the word problem of the Baumslag group under parallel complexity aspects. In particular, we establish that the word problem of the Baumslag group can be solved in NC - even though one of the essential steps is to compare two integers given by power circuits and this, in general, is shown to be P-complete. The key observation is that the depth of the occurring power circuits is logarithmic and such power circuits can be compared in NC. △ Less

Submitted 15 June, 2022; v1 submitted 19 February, 2021; originally announced February 2021.

ACM Class: F.2.2; G.2.m

Understanding and Fixing Complex Faults in Embedded Cyberphysical Systems

Authors: Alexander Weiss, Smitha Gautham, Athira Varma Jayakumar, Carl Elks, D. Richard Kuhn, Raghu N. Kacker, Thomas B. Preusser

Abstract: Understanding fault types can lead to novel approaches to debugging and runtime verification. Dealing with complex faults, particularly in the challenging area of embedded systems, craves for more powerful tools, which are now becoming available to engineers. Understanding fault types can lead to novel approaches to debugging and runtime verification. Dealing with complex faults, particularly in the challenging area of embedded systems, craves for more powerful tools, which are now becoming available to engineers. △ Less

Submitted 5 February, 2021; originally announced February 2021.

Supporting Musical Practice Sessions Through HMD-Based Augmented Reality

Authors: Karola Marky, Andreas Weiß, Thomas Kosch

Abstract: Learning a musical instrument requires a lot of practice, which ideally, should be done every day. During practice sessions, students are on their own in the overwhelming majority of the time, but access to experts that support students "just-in-time" is limited. Therefore, students commonly do not receive any feedback during their practice sessions. Adequate feedback, especially for beginners, is… ▽ More Learning a musical instrument requires a lot of practice, which ideally, should be done every day. During practice sessions, students are on their own in the overwhelming majority of the time, but access to experts that support students "just-in-time" is limited. Therefore, students commonly do not receive any feedback during their practice sessions. Adequate feedback, especially for beginners, is highly important for three particular reasons: (1) preventing the acquirement of wrong motions, (2) avoiding frustration due to a steep learning curve, and (3) potential health problems that arise from straining muscles or joints harmfully. In this paper, we envision the usage of head-mounted displays as assistance modality to support musical instrument learning. We propose a modular concept for several assistance modes to help students during their practice sessions. Finally, we discuss hardware requirements and implementations to realize the proposed concepts. △ Less

Submitted 4 January, 2021; originally announced January 2021.

Mastering Music Instruments through Technology in Solo Learning Sessions

Authors: Karola Marky, Andreas Weiß, Julien Gedeon, Sebastian Günther

Abstract: Mastering a musical instrument requires time-consuming practice even if students are guided by an expert. In the overwhelming majority of the time, the students practice by themselves and traditional teaching materials, such as videos or textbooks, lack interaction and guidance possibilities. Adequate feedback, however, is highly important to prevent the acquirement of wrong motions and to avoid p… ▽ More Mastering a musical instrument requires time-consuming practice even if students are guided by an expert. In the overwhelming majority of the time, the students practice by themselves and traditional teaching materials, such as videos or textbooks, lack interaction and guidance possibilities. Adequate feedback, however, is highly important to prevent the acquirement of wrong motions and to avoid potential health problems. In this paper, we envision musical instruments as smart objects to enhance solo learning sessions. We give an overview of existing approaches and setups and discuss them. Finally, we conclude with recommendations for designing smart and augmented musical instruments for learning purposes. △ Less

Submitted 27 December, 2020; originally announced December 2020.

Equation satisfiability in solvable groups

Authors: Paweł Idziak, Piotr Kawałek, Jacek Krzaczkowski, Armin Weiß

Abstract: The study of the complexity of the equation satisfiability problem in finite groups had been initiated by Goldmann and Russell (2002) where they showed that this problem is in polynomial time for nilpotent groups while it is NP-complete for non-solvable groups. Since then, several results have appeared showing that the problem can be solved in polynomial time in certain solvable groups $G$ having… ▽ More The study of the complexity of the equation satisfiability problem in finite groups had been initiated by Goldmann and Russell (2002) where they showed that this problem is in polynomial time for nilpotent groups while it is NP-complete for non-solvable groups. Since then, several results have appeared showing that the problem can be solved in polynomial time in certain solvable groups $G$ having a nilpotent normal subgroup $H$ with nilpotent factor $G/H$. This paper shows that such normal subgroup must exist in each finite group with equation satisfiability solvable in polynomial time, unless the Exponential Time Hypothesis fails. △ Less

Submitted 22 October, 2020; originally announced October 2020.

MSC Class: 68Q17 20D10

Using DSP Slices as Content-Addressable Update Queues

Authors: Thomas B. Preußer, Monica Chiosa, Alexander Weiss, Gustavo Alonso

Abstract: Content-Addressable Memory (CAM) is a powerful abstraction for building memory caches, routing tables and hazard detection logic. Without a native CAM structure available on FPGA devices, their functionality must be emulated using the structural primitives at hand. Such an emulation causes significant overhead in the consumption of the underlying resources, typically general-purpose fabric and on-… ▽ More Content-Addressable Memory (CAM) is a powerful abstraction for building memory caches, routing tables and hazard detection logic. Without a native CAM structure available on FPGA devices, their functionality must be emulated using the structural primitives at hand. Such an emulation causes significant overhead in the consumption of the underlying resources, typically general-purpose fabric and on-chip block RAM (BRAM). This often motivates mitigating trade-offs, such as the reduction of the associativity of memory caches. This paper describes a technique to implement the hazard resolution in a memory update queue that hides the off-chip memory readout latency of read-modify-write cycles while guaranteeing the delivery of the full memory bandwidth. The innovative use of DSP slices allows them to assume and combine the functions of (a) the tag and data storage, (b) the tag matching, and (c) the data update in this key-value storage scenario. The proposed approach provides designers with extra flexibility by adding this resource type as another option to implement CAM. △ Less

Submitted 23 April, 2020; originally announced April 2020.

Comments: Submitted to FPL 2020

Efficient Machine Learning Approach for Optimizing the Timing Resolution of a High Purity Germanium Detector

Authors: R. W. Gladen, V. A. Chirayath, A. J. Fairchild, M. T. Manry, A. R. Koymen, A. H. Weiss

Abstract: We describe here an efficient machine-learning based approach for the optimization of parameters used for extracting the arrival time of waveforms, in particular those generated by the detection of 511 keV annihilation gamma-rays by a 60 cm3 coaxial high purity germanium detector (HPGe). The method utilizes a type of artificial neural network (ANN) called a self-organizing map (SOM) to cluster the… ▽ More We describe here an efficient machine-learning based approach for the optimization of parameters used for extracting the arrival time of waveforms, in particular those generated by the detection of 511 keV annihilation gamma-rays by a 60 cm3 coaxial high purity germanium detector (HPGe). The method utilizes a type of artificial neural network (ANN) called a self-organizing map (SOM) to cluster the HPGe waveforms based on the shape of their rising edges. The optimal timing parameters for HPGe waveforms belonging to a particular cluster are found by minimizing the time difference between the HPGe signal and a signal produced by a BaF2 scintillation detector. Applying these variable timing parameters to the HPGe signals achieved a gamma-coincidence timing resolution of ~ 4.3 ns at the 511 keV photo peak (defined as 511 +- 50 keV) and a timing resolution of ~ 6.5 ns for the entire gamma spectrum--without rejecting any valid pulses. This timing resolution approaches the best obtained by analog nuclear electronics, without the corresponding complexities of analog optimization procedures. We further demonstrate the universality and efficacy of the machine learning approach by applying the method to the generation of secondary electron time-of-flight spectra following the implantation of energetic positrons on a sample. △ Less

Submitted 31 March, 2020; originally announced April 2020.

Hardness of equations over finite solvable groups under the exponential time hypothesis

Authors: Armin Weiß

Abstract: Goldmann and Russell (2002) initiated the study of the complexity of the equation satisfiability problem in finite groups by showing that it is in P for nilpotent groups while it is NP-complete for non-solvable groups. Since then, several results have appeared showing that the problem can be solved in polynomial time in certain solvable groups of Fitting length two. In this work, we present the fi… ▽ More Goldmann and Russell (2002) initiated the study of the complexity of the equation satisfiability problem in finite groups by showing that it is in P for nilpotent groups while it is NP-complete for non-solvable groups. Since then, several results have appeared showing that the problem can be solved in polynomial time in certain solvable groups of Fitting length two. In this work, we present the first lower bounds for the equation satisfiability problem in finite solvable groups: under the assumption of the exponential time hypothesis, we show that it cannot be in P for any group of Fitting length at least four and for certain groups of Fitting length three. Moreover, the same hardness result applies to the equation identity problem. △ Less

Submitted 26 October, 2020; v1 submitted 24 February, 2020; originally announced February 2020.

MSC Class: 20D60; 68Q17; 20D10 ACM Class: F.2.2; G.2.m

Groups with ALOGTIME-hard word problems and PSPACE-complete compressed word problems

Authors: Laurent Bartholdi, Michael Figelius, Markus Lohrey, Armin Weiß

Abstract: We give lower bounds on the complexity of the word problem of certain non-solvable groups: for a large class of non-solvable infinite groups, including in particular free groups, Grigorchuk's group and Thompson's groups, we prove that their word problem is $\mathsf{NC}^1$-hard. For some of these groups (including Grigorchuk's group and Thompson's groups) we prove that the compressed word problem (… ▽ More We give lower bounds on the complexity of the word problem of certain non-solvable groups: for a large class of non-solvable infinite groups, including in particular free groups, Grigorchuk's group and Thompson's groups, we prove that their word problem is $\mathsf{NC}^1$-hard. For some of these groups (including Grigorchuk's group and Thompson's groups) we prove that the compressed word problem (which is equivalent to the circuit evaluation problem) is $\mathsf{PSPACE}$-complete. △ Less

Submitted 20 June, 2020; v1 submitted 30 September, 2019; originally announced September 2019.

Comments: A short version of the paper will appear in the Proceedings of the Computational Complexity Conference 2020

An Automaton Group with PSPACE-Complete Word Problem

Authors: Jan Philipp Wächter, Armin Weiß

Abstract: We construct an automaton group with a PSPACE-complete word problem, proving a conjecture due to Steinberg. Additionally, the constructed group has a provably more difficult, namely EXPSPACE-complete, compressed word problem and acts over a binary alphabet. Thus, it is optimal in terms of the alphabet size. Our construction directly simulates the computation of a Turing machine in an automaton gro… ▽ More We construct an automaton group with a PSPACE-complete word problem, proving a conjecture due to Steinberg. Additionally, the constructed group has a provably more difficult, namely EXPSPACE-complete, compressed word problem and acts over a binary alphabet. Thus, it is optimal in terms of the alphabet size. Our construction directly simulates the computation of a Turing machine in an automaton group and, therefore, seems to be quite versatile. It combines two ideas: the first one is a construction used by D'Angeli, Rodaro and the first author to obtain an inverse automaton semigroup with a PSPACE-complete word problem and the second one is to utilize a construction used by Barrington to simulate Boolean circuits of bounded degree and logarithmic depth in the group of even permutations over five elements. △ Less

Submitted 17 July, 2021; v1 submitted 8 June, 2019; originally announced June 2019.

Comments: Extended version submitted to the special issue for STACS 2020; revised according to review comments

MSC Class: 20F10; 68Q17; 68Q45 ACM Class: F.4.m; F.2.2

Journal ref: Conference version: 37th International Symposium on Theoretical Aspects of Computer Science, STACS 2020, March 10-13, 2020, Montpellier, France, pages 6:1-6:17, 2020

On the Average Case of MergeInsertion

Authors: Florian Stober, Armin Weiß

Abstract: MergeInsertion, also known as the Ford-Johnson algorithm, is a sorting algorithm which, up to today, for many input sizes achieves the best known upper bound on the number of comparisons. Indeed, it gets extremely close to the information-theoretic lower bound. While the worst-case behavior is well understood, only little is known about the average case. This work takes a closer look at the aver… ▽ More MergeInsertion, also known as the Ford-Johnson algorithm, is a sorting algorithm which, up to today, for many input sizes achieves the best known upper bound on the number of comparisons. Indeed, it gets extremely close to the information-theoretic lower bound. While the worst-case behavior is well understood, only little is known about the average case. This work takes a closer look at the average case behavior. In particular, we establish an upper bound of $n \log n - 1.4005n + o(n)$ comparisons. We also give an exact description of the probability distribution of the length of the chain a given element is inserted into and use it to approximate the average number of comparisons numerically. Moreover, we compute the exact average number of comparisons for $n$ up to 148. Furthermore, we experimentally explore the impact of different decision trees for binary insertion. To conclude, we conduct experiments showing that a slightly different insertion order leads to a better average case and we compare the algorithm to the recent combination with (1,2)-Insertionsort by Iwama and Teruyama. △ Less

Submitted 23 May, 2019; originally announced May 2019.

The power word problem

Authors: Markus Lohrey, Armin Weiß

Abstract: In this work we introduce a new succinct variant of the word problem in a finitely generated group $G$, which we call the power word problem: the input word may contain powers $p^x$, where $p$ is a finite word over generators of $G$ and $x$ is a binary encoded integer. The power word problem is a restriction of the compressed word problem, where the input word is represented by a straight-line pro… ▽ More In this work we introduce a new succinct variant of the word problem in a finitely generated group $G$, which we call the power word problem: the input word may contain powers $p^x$, where $p$ is a finite word over generators of $G$ and $x$ is a binary encoded integer. The power word problem is a restriction of the compressed word problem, where the input word is represented by a straight-line program (i.e., an algebraic circuit over $G$). The main result of the paper states that the power word problem for a finitely generated free group $F$ is AC$^0$-Turing-reducible to the word problem for $F$. Moreover, the following hardness result is shown: For a wreath product $G \wr \mathbb{Z}$, where $G$ is either free of rank at least two or finite non-solvable, the power word problem is complete for coNP. This contrasts with the situation where $G$ is abelian: then the power word problem is shown to be in TC$^0$. △ Less

Submitted 17 April, 2019; originally announced April 2019.

Oxide: The Essence of Rust

Authors: Aaron Weiss, Olek Gierczak, Daniel Patterson, Amal Ahmed

Abstract: Rust claims to advance industrial programming by bridging the gap between low-level systems programming and high-level application programming. At the heart of the argument that this enables programmers to build more reliable and efficient software is the borrow checker - a novel approach to ownership that aims to balance type system expressivity with usability. And yet, to date there is no core t… ▽ More Rust claims to advance industrial programming by bridging the gap between low-level systems programming and high-level application programming. At the heart of the argument that this enables programmers to build more reliable and efficient software is the borrow checker - a novel approach to ownership that aims to balance type system expressivity with usability. And yet, to date there is no core type system that captures Rust's notion of ownership and borrowing, and hence no foundation for research on Rust to build upon. In this work, we set out to capture the essence of this model of ownership by develo** a type systems account of Rust's borrow checker. We present Oxide, a formalized programming language close to source-level Rust (but with fully-annotated types). This presentation takes a new view of lifetimes as an approximation of the provenances of references, and our type system is able to automatically compute this information through a substructural ty** judgment. We provide the first syntactic proof of type safety for borrow checking using progress and preservation. Oxide is a simpler formulation of borrow checking - including recent features such as non-lexical lifetimes - that we hope researchers will be able to use as the basis for work on Rust. △ Less

Submitted 19 October, 2021; v1 submitted 3 March, 2019; originally announced March 2019.

Comments: Latest draft

A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)

Authors: César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, Ezio Bartocci, Domenico Bianculli, Christian Colombo, Yliés Falcone, Adrian Francalanza, Srđan Krstić, JoHao M. Lourenço, Dejan Nickovic, Gordon J. Pace, Jose Rufino, Julien Signoles, Dmitriy Traytel, Alexander Weiss

Abstract: Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system t… ▽ More Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification. △ Less

Submitted 16 November, 2018; originally announced November 2018.

QuickXsort - A Fast Sorting Scheme in Theory and Practice

Authors: Stefan Edelkamp, Armin Weiß, Sebastian Wild

Abstract: QuickXsort is a highly efficient in-place sequential sorting scheme that mixes Hoare's Quicksort algorithm with X, where X can be chosen from a wider range of other known sorting algorithms, like Heapsort, Insertionsort and Mergesort. Its major advantage is that QuickXsort can be in-place even if X is not. In this work we provide general transfer theorems expressing the number of comparisons of Qu… ▽ More QuickXsort is a highly efficient in-place sequential sorting scheme that mixes Hoare's Quicksort algorithm with X, where X can be chosen from a wider range of other known sorting algorithms, like Heapsort, Insertionsort and Mergesort. Its major advantage is that QuickXsort can be in-place even if X is not. In this work we provide general transfer theorems expressing the number of comparisons of QuickXsort in terms of the number of comparisons of X. More specifically, if pivots are chosen as medians of (not too fast) growing size samples, the average number of comparisons of QuickXsort and X differ only by $o(n)$-terms. For median-of-$k$ pivot selection for some constant $k$, the difference is a linear term whose coefficient we compute precisely. For instance, median-of-three QuickMergesort uses at most $n \lg n - 0.8358n + O(\log n)$ comparisons. Furthermore, we examine the possibility of sorting base cases with some other algorithm using even less comparisons. By doing so the average-case number of comparisons can be reduced down to $n \lg n- 1.4106n + o(n)$ for a remaining gap of only $0.0321n$ comparisons to the known lower bound (while using only $O(\log n)$ additional space and $O(n \log n)$ time overall). Implementations of these sorting strategies show that the algorithms challenge well-established library implementations like Musser's Introsort. △ Less

Submitted 3 November, 2018; originally announced November 2018.

Worst-Case Efficient Sorting with QuickMergesort

Authors: Stefan Edelkamp, Armin Weiß

Abstract: The two most prominent solutions for the sorting problem are Quicksort and Mergesort. While Quicksort is very fast on average, Mergesort additionally gives worst-case guarantees, but needs extra space for a linear number of elements. Worst-case efficient in-place sorting, however, remains a challenge: the standard solution, Heapsort, suffers from a bad cache behavior and is also not overly fast fo… ▽ More The two most prominent solutions for the sorting problem are Quicksort and Mergesort. While Quicksort is very fast on average, Mergesort additionally gives worst-case guarantees, but needs extra space for a linear number of elements. Worst-case efficient in-place sorting, however, remains a challenge: the standard solution, Heapsort, suffers from a bad cache behavior and is also not overly fast for in-cache instances. In this work we present median-of-medians QuickMergesort (MoMQuickMergesort), a new variant of QuickMergesort, which combines Quicksort with Mergesort allowing the latter to be implemented in place. Our new variant applies the median-of-medians algorithm for selecting pivots in order to circumvent the quadratic worst case. Indeed, we show that it uses at most $n \log n + 1.6n$ comparisons for $n$ large enough. We experimentally confirm the theoretical estimates and show that the new algorithm outperforms Heapsort by far and is only around 10% slower than Introsort (std::sort implementation of stdlibc++), which has a rather poor guarantee for the worst case. We also simulate the worst case, which is only around 10% slower than the average case. In particular, the new algorithm is a natural candidate to replace Heapsort as a worst-case stopper in Introsort. △ Less

Submitted 2 November, 2018; originally announced November 2018.

ACM Class: F.2.2

Rust Distilled: An Expressive Tower of Languages

Authors: Aaron Weiss, Daniel Patterson, Amal Ahmed

Abstract: Rust represents a major advancement in production programming languages because of its success in bridging the gap between high-level application programming and low-level systems programming. At the heart of its design lies a novel approach to ownership that remains highly programmable. In this talk, we will describe our ongoing work on designing a formal semantics for Rust that captures owners… ▽ More Rust represents a major advancement in production programming languages because of its success in bridging the gap between high-level application programming and low-level systems programming. At the heart of its design lies a novel approach to ownership that remains highly programmable. In this talk, we will describe our ongoing work on designing a formal semantics for Rust that captures ownership and borrowing without the details of lifetime analysis. This semantics models a high-level understanding of ownership and as a result is close to source-level Rust (but with full type annotations) which differs from the recent RustBelt effort that essentially models MIR, a CPS-style IR used in the Rust compiler. Further, while RustBelt aims to verify the safety of unsafe code in Rust's standard library, we model standard library APIs as primitives, which is sufficient to reason about their behavior. This yields a simpler model of Rust and its type system that we think researchers will find easier to use as a starting point for investigating Rust extensions. Unlike RustBelt, we aim to prove type soundness using progress and preservation instead of a Kripke logical relation. Finally, our semantics is a family of languages of increasing expressive power, where subsequent levels have features that are impossible to define in previous levels. Following Felleisen, expressive power is defined in terms of observational equivalence. Separating the language into different levels of expressive power should provide a framework for future work on Rust verification and compiler optimization. △ Less

Submitted 16 August, 2018; v1 submitted 7 June, 2018; originally announced June 2018.

Comments: ML '18 Final

QuickMergesort: Practically Efficient Constant-Factor Optimal Sorting

Authors: Stefan Edelkamp, Armin Weiß

Abstract: We consider the fundamental problem of internally sorting a sequence of $n$ elements. In its best theoretical setting QuickMergesort, a combination Quicksort with Mergesort with a Median-of-$\sqrt{n}$ pivot selection, requires at most $n \log n - 1.3999n + o(n)$ element comparisons on the average. The questions addressed in this paper is how to make this algorithm practical. As refined pivot selec… ▽ More We consider the fundamental problem of internally sorting a sequence of $n$ elements. In its best theoretical setting QuickMergesort, a combination Quicksort with Mergesort with a Median-of-$\sqrt{n}$ pivot selection, requires at most $n \log n - 1.3999n + o(n)$ element comparisons on the average. The questions addressed in this paper is how to make this algorithm practical. As refined pivot selection usually adds much overhead, we show that the Median-of-3 pivot selection of QuickMergesort leads to at most $n \log n - 0{.}75n + o(n)$ element comparisons on average, while running fast on elementary data. The experiments show that QuickMergesort outperforms state-of-the-art library implementations, including C++'s Introsort and Java's Dual-Pivot Quicksort. Further trade-offs between a low running time and a low number of comparisons are studied. Moreover, we describe a practically efficient version with $n \log n + O(n)$ comparisons in the worst case. △ Less

Submitted 26 April, 2018; originally announced April 2018.

ACM Class: F.2.2

The isomorphism problem for finite extensions of free groups is in PSPACE

Authors: Géraud Sénizergues, Armin Weiß

Abstract: We present an algorithm for the following problem: given a context-free grammar for the word problem of a virtually free group $G$, compute a finite graph of groups $\mathcal{G}$ with finite vertex groups and fundamental group $G$. Our algorithm is non-deterministic and runs in doubly exponential time. It follows that the isomorphism problem of context-free groups can be solved in doubly exponenti… ▽ More We present an algorithm for the following problem: given a context-free grammar for the word problem of a virtually free group $G$, compute a finite graph of groups $\mathcal{G}$ with finite vertex groups and fundamental group $G$. Our algorithm is non-deterministic and runs in doubly exponential time. It follows that the isomorphism problem of context-free groups can be solved in doubly exponential space. Moreover, if, instead of a grammar, a finite extension of a free group is given as input, the construction of the graph of groups is in NP and, consequently, the isomorphism problem in PSPACE. △ Less

Submitted 20 February, 2018; originally announced February 2018.

MSC Class: 68Q45; 68Q25; 05C25; 20E08; 20F10; 20F65 ACM Class: F.4.3; F.2.2; G.2.2

First-Order Perturbation Analysis of the SECSI Framework for the Approximate CP Decomposition of 3-D Noise-Corrupted Low-Rank Tensors

Authors: Sher Ali Cheema, Emilio Rafael Balda, Yao Cheng, Martin Haardt, Amir Weiss, Arie Yeredor

Abstract: The Semi-Algebraic framework for the approximate Canonical Polyadic (CP) decomposition via SImultaneaous matrix diagonalization (SECSI) is an efficient tool for the computation of the CP decomposition. The SECSI framework reformulates the CP decomposition into a set of joint eigenvalue decomposition (JEVD) problems. Solving all JEVDs, we obtain multiple estimates of the factor matrices and the bes… ▽ More The Semi-Algebraic framework for the approximate Canonical Polyadic (CP) decomposition via SImultaneaous matrix diagonalization (SECSI) is an efficient tool for the computation of the CP decomposition. The SECSI framework reformulates the CP decomposition into a set of joint eigenvalue decomposition (JEVD) problems. Solving all JEVDs, we obtain multiple estimates of the factor matrices and the best estimate is chosen in a subsequent step by using an exhaustive search or some heuristic strategy that reduces the computational complexity. Moreover, the SECSI framework retains the option of choosing the number of JEVDs to be solved, thus providing an adjustable complexity-accuracy trade-off. In this work, we provide an analytical performance analysis of the SECSI framework for the computation of the approximate CP decomposition of a noise corrupted low-rank tensor, where we derive closed-form expressions of the relative mean square error for each of the estimated factor matrices. These expressions are obtained using a first-order perturbation analysis and are formulated in terms of the second-order moments of the noise, such that apart from a zero mean, no assumptions on the noise statistics are required. Simulation results exhibit an excellent match between the obtained closed-form expressions and the empirical results. Moreover, we propose a new Performance Analysis based Selection (PAS) scheme to choose the final factor matrix estimate. The results show that the proposed PAS scheme outperforms the existing heuristics, especially in the high SNR regime. △ Less

Submitted 18 October, 2017; originally announced October 2017.

Tortoise: Interactive System Configuration Repair

Authors: Aaron Weiss, Arjun Guha, Yuriy Brun

Abstract: System configuration languages provide powerful abstractions that simplify managing large-scale, networked systems. Thousands of organizations now use configuration languages, such as Puppet. However, specifications written in configuration languages can have bugs and the shell remains the simplest way to debug a misconfigured system. Unfortunately, it is unsafe to use the shell to fix problems wh… ▽ More System configuration languages provide powerful abstractions that simplify managing large-scale, networked systems. Thousands of organizations now use configuration languages, such as Puppet. However, specifications written in configuration languages can have bugs and the shell remains the simplest way to debug a misconfigured system. Unfortunately, it is unsafe to use the shell to fix problems when a system configuration language is in use: a fix applied from the shell may cause the system to drift from the state specified by the configuration language. Thus, despite their advantages, configuration languages force system administrators to give up the simplicity and familiarity of the shell. This paper presents a synthesis-based technique that allows administrators to use configuration languages and the shell in harmony. Administrators can fix errors using the shell and the technique automatically repairs the higher-level specification written in the configuration language. The approach (1) produces repairs that are consistent with the fix made using the shell; (2) produces repairs that are maintainable by minimizing edits made to the original specification; (3) ranks and presents multiple repairs when relevant; and (4) supports all shells the administrator may wish to use. We implement our technique for Puppet, a widely used system configuration language, and evaluate it on a suite of benchmarks under 42 repair scenarios. The top-ranked repair is selected by humans 76% of the time and the human-equivalent repair is ranked 1.31 on average. △ Less

Submitted 15 September, 2017; originally announced September 2017.

Comments: Published version in proceedings of IEEE/ACM International Conference on Automated Software Engineering (ASE) 2017

Journal ref: in Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2017, pp. 625-636

TC^0 circuits for algorithmic problems in nilpotent groups

Authors: Alexei Myasnikov, Armin Weiß

Abstract: Recently, Macdonald et. al. showed that many algorithmic problems for finitely generated nilpotent groups including computation of normal forms, the subgroup membership problem, the conjugacy problem, and computation of subgroup presentations can be done in Logspace. Here we follow their approach and show that all these problems are complete for the uniform circuit class TC^0 - uniformly for all r… ▽ More Recently, Macdonald et. al. showed that many algorithmic problems for finitely generated nilpotent groups including computation of normal forms, the subgroup membership problem, the conjugacy problem, and computation of subgroup presentations can be done in Logspace. Here we follow their approach and show that all these problems are complete for the uniform circuit class TC^0 - uniformly for all r-generated nilpotent groups of class at most c for fixed r and c. In order to solve these problems in TC^0, we show that the unary version of the extended gcd problem (compute greatest common divisors and express them as linear combinations) is in TC^0. Moreover, if we allow a certain binary representation of the inputs, then the word problem and computation of normal forms is still in uniform TC^0, while all the other problems we examine are shown to be TC^0-Turing reducible to the binary extended gcd problem. △ Less

Submitted 26 July, 2017; v1 submitted 21 February, 2017; originally announced February 2017.

ACM Class: F.2.2; G.2.0

The conjugacy problem in free solvable groups and wreath product of abelian groups is in TC$^0$

Authors: Alexei Miasnikov, Svetla Vassileva, Armin Weiß

Abstract: We show that the conjugacy problem in a wreath product $A \wr B$ is uniform-$\mathsf{TC}^0$-Turing-reducible to the conjugacy problem in the factors $A$ and $B$ and the power problem in $B$. If $B$ is torsion free, the power problem for $B$ can be replaced by the slightly weaker cyclic submonoid membership problem for $B$. Moreover, if $A$ is abelian, the cyclic subgroup membership problem suffice… ▽ More We show that the conjugacy problem in a wreath product $A \wr B$ is uniform-$\mathsf{TC}^0$-Turing-reducible to the conjugacy problem in the factors $A$ and $B$ and the power problem in $B$. If $B$ is torsion free, the power problem for $B$ can be replaced by the slightly weaker cyclic submonoid membership problem for $B$. Moreover, if $A$ is abelian, the cyclic subgroup membership problem suffices, which itself is uniform-$\mathsf{AC}^0$-many-one-reducible to the conjugacy problem in $A \wr B$. Furthermore, under certain natural conditions, we give a uniform $\mathsf{TC}^0$ Turing reduction from the power problem in $A \wr B$ to the power problems of $A$ and $B$. Together with our first result, this yields a uniform $\mathsf{TC}^0$ solution to the conjugacy problem in iterated wreath products of abelian groups - and, by the Magnus embedding, also in free solvable groups. △ Less

Submitted 11 September, 2017; v1 submitted 18 December, 2016; originally announced December 2016.

MSC Class: 20F10; 68Q25 ACM Class: F.2.2; G.2.m

User Experience of a Smart Factory Robot: Assembly Line Workers Demand Adaptive Robots

Authors: Astrid Weiss, Andreas Huber

Abstract: This paper reports a case study on the User Experience (UX)of an industrial robotic prototype in the context of human-robot cooperation in an automotive assembly line. The goal was to find out what kinds of suggestions the assembly line workers, who actually use the new robotic system, propose in order to improve the human-robot interaction (HRI). The operators working with the robotic prototype w… ▽ More This paper reports a case study on the User Experience (UX)of an industrial robotic prototype in the context of human-robot cooperation in an automotive assembly line. The goal was to find out what kinds of suggestions the assembly line workers, who actually use the new robotic system, propose in order to improve the human-robot interaction (HRI). The operators working with the robotic prototype were interviewed three weeks after the deployment using established UX narrative interview guidelines. Our results show that the cooperation with a robot that executes predefined working steps actually impedes the user in terms of flexibility and individual speed. This results in a change of working routine for the operators, impacts the UX, and potentially leads to a decrease in productivity. We present the results of the interviews as well as first thoughts on technical solutions in order to enhance the adaptivity and subsequently the UX of the human-robot cooperation. △ Less

Submitted 13 June, 2016; originally announced June 2016.

Comments: 5th International Symposium on New Frontiers in Human-Robot Interaction 2016 (arXiv:1602.05456)

Report number: AISB-NFHRI/2016/02

Help, Anyone? A User Study For Modeling Robotic Behavior To Mitigate Malfunctions With The Help Of The User

Authors: Markus Bajones, Astrid Weiss, Markus Vincze

Abstract: Service robots for the domestic environment are intended to autonomously provide support for their users. However, state-of-the-art robots still often get stuck in failure situations leading to breakdowns in the interaction flow from which the robot cannot recover alone. We performed a multi-user Wizard-of-Oz experiment in which we manipulated the robot's behavior in such a way that it appeared un… ▽ More Service robots for the domestic environment are intended to autonomously provide support for their users. However, state-of-the-art robots still often get stuck in failure situations leading to breakdowns in the interaction flow from which the robot cannot recover alone. We performed a multi-user Wizard-of-Oz experiment in which we manipulated the robot's behavior in such a way that it appeared unexpected and malfunctioning, and asked participants to help the robot in order to restore the interaction flow. We examined how participants reacted to the robot's error, its subsequent request for help and how it changed their perception of the robot with respect to perceived intelligence, likability, and task contribution. As interaction scenario we used a game of building Lego models performed by user dyads. In total 38 participants interacted with the robot and helped in malfunctioning situations. We report two major findings: (1) in user dyads, the user who gave the last command followed by the user who is closer is more likely to help (2) malfunctions that can be actively fixed by the user seem not to negatively impact perceived intelligence and likability ratings. This work offers insights in how far user support can be a strategy for domestic service robots to recover from repeating malfunctions. △ Less

Submitted 8 June, 2016; originally announced June 2016.

Comments: 5th International Symposium on New Frontiers in Human-Robot Interaction 2016 (arXiv:1602.05456)

Report number: AISB-NFHRI/2016/02

BlockQuicksort: How Branch Mispredictions don't affect Quicksort

Authors: Stefan Edelkamp, Armin Weiß

Abstract: Since the work of Kaligosi and Sanders (2006), it is well-known that Quicksort -- which is commonly considered as one of the fastest in-place sorting algorithms -- suffers in an essential way from branch mispredictions. We present a novel approach to address this problem by partially decoupling control from data flow: in order to perform the partitioning, we split the input in blocks of constant s… ▽ More Since the work of Kaligosi and Sanders (2006), it is well-known that Quicksort -- which is commonly considered as one of the fastest in-place sorting algorithms -- suffers in an essential way from branch mispredictions. We present a novel approach to address this problem by partially decoupling control from data flow: in order to perform the partitioning, we split the input in blocks of constant size (we propose 128 data elements); then, all elements in one block are compared with the pivot and the outcomes of the comparisons are stored in a buffer. In a second pass, the respective elements are rearranged. By doing so, we avoid conditional branches based on outcomes of comparisons at all (except for the final Insertionsort). Moreover, we prove that for a static branch predictor the average total number of branch mispredictions is at most $εn \log n + O(n)$ for some small $ε$ depending on the block size when sorting $n$ elements. Our experimental results are promising: when sorting random integer data, we achieve an increase in speed of 80% over the GCC implementation of C++ std::sort. Also for many other types of data and non-random inputs, there is still a significant speedup over std::sort. Only in few special cases like sorted or almost sorted inputs, std::sort can beat out implementation. Moreover, even on random input permutations, our implementation is even slightly faster than an implementation of the highly tuned Super Scalar Sample Sort, which uses a linear amount of additional space. △ Less

Submitted 23 June, 2016; v1 submitted 22 April, 2016; originally announced April 2016.

ACM Class: F.2.2

5th International Symposium on New Frontiers in Human-Robot Interaction 2016 (NF-HRI 2016)

Authors: Maha Salem, Astrid Weiss, Paul Baxter, Kerstin Dautenhahn

Abstract: This volume is the proceedings of the 5th International Symposium on New Frontiers in Human-Robot Interaction, held at the AISB Convention 2016, which took place on the 5th and 6th of April 2016, in Sheffield, U.K. Organised by Maha Salem (Google U.K.), Astrid Weiss (Vienna University of Technology, Austria), Paul Baxter (Lincoln University, U.K.), and Kerstin Dautenhahn (University of Hertfords… ▽ More This volume is the proceedings of the 5th International Symposium on New Frontiers in Human-Robot Interaction, held at the AISB Convention 2016, which took place on the 5th and 6th of April 2016, in Sheffield, U.K. Organised by Maha Salem (Google U.K.), Astrid Weiss (Vienna University of Technology, Austria), Paul Baxter (Lincoln University, U.K.), and Kerstin Dautenhahn (University of Hertfordshire, U.K.). △ Less

Submitted 8 June, 2016; v1 submitted 17 February, 2016; originally announced February 2016.

Comments: Index for conference proceedings NF-HRI 2016

MSC Class: 68T40

A Logspace Solution to the Word and Conjugacy problem of Generalized Baumslag-Solitar Groups

Authors: Armin Weiß

Abstract: Baumslag-Solitar groups were introduced in 1962 by Baumslag and Solitar as examples for finitely presented non-Hopfian two-generator groups. Since then, they served as examples for a wide range of purposes. As Baumslag-Solitar groups are HNN extensions, there is a natural generalization in terms of graph of groups. Concerning algorithmic aspects of generalized Baumslag-Solitar groups, several de… ▽ More Baumslag-Solitar groups were introduced in 1962 by Baumslag and Solitar as examples for finitely presented non-Hopfian two-generator groups. Since then, they served as examples for a wide range of purposes. As Baumslag-Solitar groups are HNN extensions, there is a natural generalization in terms of graph of groups. Concerning algorithmic aspects of generalized Baumslag-Solitar groups, several decidability results are known. Indeed, a straightforward application of standard algorithms leads to a polynomial time solution of the word problem (the question whether some word over the generators represents the identity of the group). The conjugacy problem (the question whether two given words represent conjugate group elements) is more complicated; still decidability has been established by Anshel and Stebe for ordinary Baumslag-Solitar groups and for generalized Baumslag-Solitar groups independently by Lockhart and Beeker. However, up to now no precise complexity estimates have been given. In this work, we give a LOGSPACE algorithm for both problems. More precisely, we describe a uniform TC^0 many-one reduction of the word problem to the word problem of the free group. Then we refine the known techniques for the conjugacy problem and show that it can be solved in LOGSPACE. Moreover, for ordinary Baumslag-Solitar groups also conjugacy is AC^0-Turing-reducible to the word problem of the free group. Finally, we consider uniform versions (where also the graph of groups is part of the input) of both word and conjugacy problem: while the word problem still is solvable in LOGSPACE, the conjugacy problem becomes EXPSPACE-complete. △ Less

Submitted 28 February, 2016; v1 submitted 7 February, 2016; originally announced February 2016.

MSC Class: 20F10; 68Q25 ACM Class: F.2.1; G.2.1