Showing 1–36 of 36 results for author: Walter, T

Proving Calculational Proofs Correct

Authors: Andrew T. Walter, Ankit Kumar, Panagiotis Manolios

Abstract: Teaching proofs is a crucial component of any undergraduate-level program that covers formal reasoning. We have developed a calculational reasoning format and refined it over several years of teaching a freshman-level course, "Logic and Computation", to thousands of undergraduate students. In our companion paper, we presented our calculational proof format, gave an overview of the calculational pr… ▽ More Teaching proofs is a crucial component of any undergraduate-level program that covers formal reasoning. We have developed a calculational reasoning format and refined it over several years of teaching a freshman-level course, "Logic and Computation", to thousands of undergraduate students. In our companion paper, we presented our calculational proof format, gave an overview of the calculational proof checker (CPC) tool that we developed to help users write and validate proofs, described some of the technical and implementation details of CPC and provided several publicly available proofs written using our format. In this paper, we dive deeper into the implementation details of CPC, highlighting how proof validation works, which helps us argue that our proof checking process is sound. △ Less

Submitted 15 November, 2023; originally announced November 2023.

Comments: In Proceedings ACL2-2023, arXiv:2311.08373

ACM Class: D.2.4

Journal ref: EPTCS 393, 2023, pp. 133-150

Calculational Proofs in ACL2s

Authors: Andrew T. Walter, Ankit Kumar, Panagiotis Manolios

Abstract: Teaching college students how to write rigorous proofs is a critical objective in courses that introduce formal reasoning. Over the course of several years, we have developed a mechanically-checkable style of calculational reasoning that we used to teach over a thousand freshman-level undergraduate students how to reason about computation in our "Logic and Computation" class at Northeastern Univer… ▽ More Teaching college students how to write rigorous proofs is a critical objective in courses that introduce formal reasoning. Over the course of several years, we have developed a mechanically-checkable style of calculational reasoning that we used to teach over a thousand freshman-level undergraduate students how to reason about computation in our "Logic and Computation" class at Northeastern University. We were inspired by Dijkstra, who advocated the use of calculational proofs, writing "calculational proofs are almost always more effective than all informal alternatives, ..., the design of calculational proofs seems much more teachable than the elusive art of discovering an informal proof." Our calculational proof checker is integrated into ACL2s and is available as an Eclipse IDE plugin, via a Web interface, and as a stand-alone tool. It automatically checks proofs for correctness and provides useful feedback. We describe the architecture of the checker, its proof format, its underlying algorithms, its correctness and provide examples using proofs from our undergraduate class and from Dijkstra. We also describe our experiences using the proof checker to teach undergraduates how to formally reason about computation. △ Less

Submitted 23 July, 2023; originally announced July 2023.

NeRSemble: Multi-view Radiance Field Reconstruction of Human Heads

Authors: Tobias Kirschstein, Shenhan Qian, Simon Giebenhain, Tim Walter, Matthias Nießner

Abstract: We focus on reconstructing high-fidelity radiance fields of human heads, capturing their animations over time, and synthesizing re-renderings from novel viewpoints at arbitrary time steps. To this end, we propose a new multi-view capture setup composed of 16 calibrated machine vision cameras that record time-synchronized images at 7.1 MP resolution and 73 frames per second. With our setup, we coll… ▽ More We focus on reconstructing high-fidelity radiance fields of human heads, capturing their animations over time, and synthesizing re-renderings from novel viewpoints at arbitrary time steps. To this end, we propose a new multi-view capture setup composed of 16 calibrated machine vision cameras that record time-synchronized images at 7.1 MP resolution and 73 frames per second. With our setup, we collect a new dataset of over 4700 high-resolution, high-framerate sequences of more than 220 human heads, from which we introduce a new human head reconstruction benchmark. The recorded sequences cover a wide range of facial dynamics, including head motions, natural expressions, emotions, and spoken language. In order to reconstruct high-fidelity human heads, we propose Dynamic Neural Radiance Fields using Hash Ensembles (NeRSemble). We represent scene dynamics by combining a deformation field and an ensemble of 3D multi-resolution hash encodings. The deformation field allows for precise modeling of simple scene movements, while the ensemble of hash encodings helps to represent complex dynamics. As a result, we obtain radiance field representations of human heads that capture motion over time and facilitate re-rendering of arbitrary novel viewpoints. In a series of experiments, we explore the design choices of our method and demonstrate that our approach outperforms state-of-the-art dynamic radiance field approaches by a significant margin. △ Less

Submitted 4 May, 2023; originally announced May 2023.

Comments: Siggraph 2023, Project Page: https://tobias-kirschstein.github.io/nersemble/ , Video: https://youtu.be/a-OAWqBzldU

Journal ref: ACM Transactions on Graphics, Volume 42, Issue 4, Article No. 161 (2023) 1-14

A barrier for further approximating Sorting By Transpositions

Authors: Luiz Augusto G. da Silva, Luis Antonio B. Kowada, Maria Emília M. T. Walter

Abstract: The Transposition Distance Problem (TDP) is a classical problem in genome rearrangements which seeks to determine the minimum number of transpositions needed to transform a linear chromosome into another represented by the permutations $π$ and $σ$, respectively. This paper focuses on the equivalent problem of Sorting By Transpositions (SBT), where $σ$ is the identity permutation $ι$. Specifically,… ▽ More The Transposition Distance Problem (TDP) is a classical problem in genome rearrangements which seeks to determine the minimum number of transpositions needed to transform a linear chromosome into another represented by the permutations $π$ and $σ$, respectively. This paper focuses on the equivalent problem of Sorting By Transpositions (SBT), where $σ$ is the identity permutation $ι$. Specifically, we investigate palisades, a family of permutations that are "hard" to sort, as they require numerous transpositions above the celebrated lower bound devised by Bafna and Pevzner. By determining the transposition distance of palisades, we were able to provide the exact transposition diameter for $3$-permutations (TD3), a special subset of the Symmetric Group $S_n$, essential for the study of approximate solutions for SBT using the simplification technique. The exact value for TD3 has remained unknown since Elias and Hartman showed an upper bound for it. Another consequence of determining the transposition distance of palisades is that, using as lower bound the one by Bafna and Pevzner, it is impossible to guarantee approximation ratios lower than $1.375$ when approximating SBT. This finding has significant implications for the study of SBT, as this problem has been subject of intense research efforts for the past 25 years. △ Less

Submitted 8 July, 2023; v1 submitted 27 April, 2023; originally announced April 2023.

Simple and Efficient Confidence Score for Grading Whole Slide Images

Authors: Mélanie Lubrano, Yaëlle Bellahsen-Harrar, Rutger Fick, Cécile Badoual, Thomas Walter

Abstract: Grading precancerous lesions on whole slide images is a challenging task: the continuous space of morphological phenotypes makes clear-cut decisions between different grades often difficult, leading to low inter- and intra-rater agreements. More and more Artificial Intelligence (AI) algorithms are developed to help pathologists perform and standardize their diagnosis. However, those models can ren… ▽ More Grading precancerous lesions on whole slide images is a challenging task: the continuous space of morphological phenotypes makes clear-cut decisions between different grades often difficult, leading to low inter- and intra-rater agreements. More and more Artificial Intelligence (AI) algorithms are developed to help pathologists perform and standardize their diagnosis. However, those models can render their prediction without consideration of the ambiguity of the classes and can fail without notice which prevent their wider acceptance in a clinical context. In this paper, we propose a new score to measure the confidence of AI models in grading tasks. Our confidence score is specifically adapted to ordinal output variables, is versatile and does not require extra training or additional inferences nor particular architecture changes. Comparison to other popular techniques such as Monte Carlo Dropout and deep ensembles shows that our method provides state-of-the art results, while being simpler, more versatile and less computationally intensive. The score is also easily interpretable and consistent with real life hesitations of pathologists. We show that the score is capable of accurately identifying mispredicted slides and that accuracy for high confidence decisions is significantly higher than for low-confidence decisions (gap in AUC of 17.1% on the test set). We believe that the proposed confidence score could be leveraged by pathologists directly in their workflow and assist them on difficult tasks such as grading precancerous lesions. △ Less

Submitted 8 March, 2023; originally announced March 2023.

PointFISH -- learning point cloud representations for RNA localization patterns

Authors: Arthur Imbert, Florian Mueller, Thomas Walter

Abstract: Subcellular RNA localization is a critical mechanism for the spatial control of gene expression. Its mechanism and precise functional role is not yet very well understood. Single Molecule Fluorescence in Situ Hybridization (smFISH) images allow for the detection of individual RNA molecules with subcellular accuracy. In return, smFISH requires robust methods to quantify and classify RNA spatial dis… ▽ More Subcellular RNA localization is a critical mechanism for the spatial control of gene expression. Its mechanism and precise functional role is not yet very well understood. Single Molecule Fluorescence in Situ Hybridization (smFISH) images allow for the detection of individual RNA molecules with subcellular accuracy. In return, smFISH requires robust methods to quantify and classify RNA spatial distribution. Here, we present PointFISH, a novel computational approach for the recognition of RNA localization patterns. PointFISH is an attention-based network for computing continuous vector representations of RNA point clouds. Trained on simulations only, it can directly process extracted coordinates from experimental smFISH images. The resulting embedding allows scalable and flexible spatial transcriptomics analysis and matches performance of hand-crafted pipelines. △ Less

Submitted 21 February, 2023; originally announced February 2023.

Learning with minimal effort: leveraging in silico labeling for cell and nucleus segmentation

Authors: Thomas Bonte, Maxence Philbert, Emeline Coleno, Edouard Bertrand, Arthur Imbert, Thomas Walter

Abstract: Deep learning provides us with powerful methods to perform nucleus or cell segmentation with unprecedented quality. However, these methods usually require large training sets of manually annotated images, which are tedious and expensive to generate. In this paper we propose to use In Silico Labeling (ISL) as a pretraining scheme for segmentation tasks. The strategy is to acquire label-free microsc… ▽ More Deep learning provides us with powerful methods to perform nucleus or cell segmentation with unprecedented quality. However, these methods usually require large training sets of manually annotated images, which are tedious and expensive to generate. In this paper we propose to use In Silico Labeling (ISL) as a pretraining scheme for segmentation tasks. The strategy is to acquire label-free microscopy images (such as bright-field or phase contrast) along fluorescently labeled images (such as DAPI or CellMask). We then train a model to predict the fluorescently labeled images from the label-free microscopy images. By comparing segmentation performance across several training set sizes, we show that such a scheme can dramatically reduce the number of required annotations. △ Less

Submitted 10 January, 2023; originally announced January 2023.

Giga-SSL: Self-Supervised Learning for Gigapixel Images

Authors: Tristan Lazard, Marvin Lerousseau, Etienne Decencière, Thomas Walter

Abstract: Whole slide images (WSI) are microscopy images of stained tissue slides routinely prepared for diagnosis and treatment selection in medical practice. WSI are very large (gigapixel size) and complex (made of up to millions of cells). The current state-of-the-art (SoTA) approach to classify WSI subdivides them into tiles, encodes them by pre-trained networks and applies Multiple Instance Learning (M… ▽ More Whole slide images (WSI) are microscopy images of stained tissue slides routinely prepared for diagnosis and treatment selection in medical practice. WSI are very large (gigapixel size) and complex (made of up to millions of cells). The current state-of-the-art (SoTA) approach to classify WSI subdivides them into tiles, encodes them by pre-trained networks and applies Multiple Instance Learning (MIL) to train for specific downstream tasks. However, annotated datasets are often small, typically a few hundred to a few thousand WSI, which may cause overfitting and underperforming models. Conversely, the number of unannotated WSI is ever increasing, with datasets of tens of thousands (soon to be millions) of images available. While it has been previously proposed to use these unannotated data to identify suitable tile representations by self-supervised learning (SSL), downstream classification tasks still require full supervision because parts of the MIL architecture is not trained during tile level SSL pre-training. Here, we propose a strategy of slide level SSL to leverage the large number of WSI without annotations to infer powerful slide representations. Applying our method to The Cancer-Genome Atlas, one of the most widely used data resources in cancer research (16 TB image data), we are able to downsize the dataset to 23 MB without any loss in predictive power: we show that a linear classifier trained on top of these embeddings maintains or improves previous SoTA performances on various benchmark WSI classification tasks. Finally, we observe that training a classifier on these representations with tiny datasets (e.g. 50 slides) improved performances over SoTA by an average of +6.3 AUC points over all downstream tasks. △ Less

Submitted 6 December, 2022; originally announced December 2022.

ACL2s Systems Programming

Authors: Andrew T. Walter, Panagiotis Manolios

Abstract: ACL2 provides a systems programming capability that allows one to write code that uses and extends ACL2 inside of ACL2. However, for soundness reasons, ACL2 bars the unrestricted use of certain kinds of programming constructs, like destructive updates, higher-order functions, eval, and arbitrary macros. We devised a methodology for writing code in Common Lisp that allows one to access ACL2, ACL2s… ▽ More ACL2 provides a systems programming capability that allows one to write code that uses and extends ACL2 inside of ACL2. However, for soundness reasons, ACL2 bars the unrestricted use of certain kinds of programming constructs, like destructive updates, higher-order functions, eval, and arbitrary macros. We devised a methodology for writing code in Common Lisp that allows one to access ACL2, ACL2s, and Common Lisp functionality in a unified way. We arrived at this methodology in the process of develo** the ACL2 Sedan (ACL2s) and using it as a key component in formal-methods-enabled projects relating to gamified verification, education, proof checking, interfacing with external theorem provers and security. The methodology includes a library for performing ACL2 queries from Common Lisp, as well as guidelines and utilities that help address common needs. We call this methodology "ACL2s systems programming," to distinguish it from ACL2 systems programming. We show how our methodology makes it possible to easily develop tools that interface with ACL2 and ACL2s, and describe our experience using it in our research. △ Less

Submitted 23 May, 2022; originally announced May 2022.

Comments: In Proceedings ACL2 2022, arXiv:2205.11103

ACM Class: D.2.4

Journal ref: EPTCS 359, 2022, pp. 134-150

Accelerating Inhibitor Discovery With A Deep Generative Foundation Model: Validation for SARS-CoV-2 Drug Targets

Authors: Vijil Chenthamarakshan, Samuel C. Hoffman, C. David Owen, Petra Lukacik, Claire Strain-Damerell, Daren Fearon, Tika R. Malla, Anthony Tumber, Christopher J. Schofield, Helen M. E. Duyvesteyn, Wanwisa Dejnirattisai, Loic Carrique, Thomas S. Walter, Gavin R. Screaton, Tetiana Matviiuk, Aleksandra Mojsilovic, Jason Crain, Martin A. Walsh, David I. Stuart, Payel Das

Abstract: The discovery of novel inhibitor molecules for emerging drug-target proteins is widely acknowledged as a challenging inverse design problem: Exhaustive exploration of the vast chemical search space is impractical, especially when the target structure or active molecules are unknown. Here we validate experimentally the broad utility of a deep generative framework trained at-scale on protein sequenc… ▽ More The discovery of novel inhibitor molecules for emerging drug-target proteins is widely acknowledged as a challenging inverse design problem: Exhaustive exploration of the vast chemical search space is impractical, especially when the target structure or active molecules are unknown. Here we validate experimentally the broad utility of a deep generative framework trained at-scale on protein sequences, small molecules, and their mutual interactions -- that is unbiased toward any specific target. As demonstrators, we consider two dissimilar and relevant SARS-CoV-2 targets: the main protease and the spike protein (receptor binding domain, RBD). To perform target-aware design of novel inhibitor molecules, a protein sequence-conditioned sampling on the generative foundation model is performed. Despite using only the target sequence information, and without performing any target-specific adaptation of the generative model, micromolar-level inhibition was observed in in vitro experiments for two candidates out of only four synthesized for each target. The most potent spike RBD inhibitor also exhibited activity against several variants in live virus neutralization assays. These results therefore establish that a single, broadly deployable generative foundation model for accelerated hit discovery is effective and efficient, even in the most general case where neither target structure nor binder information is available. △ Less

Submitted 14 October, 2022; v1 submitted 19 April, 2022; originally announced April 2022.

Comments: Revised title, abstract, and text; additional figures

Diachronic Analysis of German Parliamentary Proceedings: Ideological Shifts through the Lens of Political Biases

Authors: Tobias Walter, Celina Kirschner, Steffen Eger, Goran Glavaš, Anne Lauscher, Simone Paolo Ponzetto

Abstract: We analyze bias in historical corpora as encoded in diachronic distributional semantic models by focusing on two specific forms of bias, namely a political (i.e., anti-communism) and racist (i.e., antisemitism) one. For this, we use a new corpus of German parliamentary proceedings, DeuPARL, spanning the period 1867--2020. We complement this analysis of historical biases in diachronic word embeddin… ▽ More We analyze bias in historical corpora as encoded in diachronic distributional semantic models by focusing on two specific forms of bias, namely a political (i.e., anti-communism) and racist (i.e., antisemitism) one. For this, we use a new corpus of German parliamentary proceedings, DeuPARL, spanning the period 1867--2020. We complement this analysis of historical biases in diachronic word embeddings with a novel measure of bias on the basis of term co-occurrences and graph-based label propagation. The results of our bias measurements align with commonly perceived historical trends of antisemitic and anti-communist biases in German politics in different time periods, thus indicating the viability of analyzing historical bias trends using semantic spaces induced from historical corpora. △ Less

Submitted 13 August, 2021; originally announced August 2021.

Comments: Accepted for JCDL2021

Prototy** and Evaluation of Infrastructure-Assisted Transition of Control for Cooperative Automated Vehicles

Authors: Baldomero Coll-Perales, Joschua Schulte-Tigges, Michele Rondinone, Javier Gozalvez, Michael Reke, Dominik Matheis, Thomas Walter

Abstract: Automated driving is now possible in diverse road and traffic conditions. However, there are still situations that automated vehicles cannot handle safely and efficiently. In this case, a Transition of Control (ToC) is necessary so that the driver takes control of the driving. Executing a ToC requires the driver to get full situation awareness of the driving environment. If the driver fails to get… ▽ More Automated driving is now possible in diverse road and traffic conditions. However, there are still situations that automated vehicles cannot handle safely and efficiently. In this case, a Transition of Control (ToC) is necessary so that the driver takes control of the driving. Executing a ToC requires the driver to get full situation awareness of the driving environment. If the driver fails to get back the control in a limited time, a Minimum Risk Maneuver (MRM) is executed to bring the vehicle into a safe state (e.g., decelerating to full stop). The execution of ToCs requires some time and can cause traffic disruption and safety risks that increase if several vehicles execute ToCs/MRMs at similar times and in the same area. This study proposes to use novel C-ITS traffic management measures where the infrastructure exploits V2X communications to assist Connected and Automated Vehicles (CAVs) in the execution of ToCs. The infrastructure can suggest a spatial distribution of ToCs, and inform vehicles of the locations where they could execute a safe stop in case of MRM. This paper reports the first field operational tests that validate the feasibility and quantify the benefits of the proposed infrastructure-assisted ToC and MRM management. The paper also presents the CAV and roadside infrastructure prototypes implemented and used in the trials. The conducted field trials demonstrate that infrastructure-assisted traffic management solutions can reduce safety risks and traffic disruptions. △ Less

Submitted 24 March, 2021; originally announced March 2021.

Comments: 16 pages, 15 figures, 3 tables. in IEEE Transactions on Intelligent Transportation Systems, 04 March 2021 (Early Access)

Neural network fast-classifies biological images using features selected after their random-forests-importance to power smart microscopy

Authors: Maël Balluet, Florian Sizaire, Youssef El Habouz, Thomas Walter, Jérémy Pont, Baptiste Giroux, Otmane Bouchareb, Marc Tramier, Jacques Pécréaux

Abstract: Artificial intelligence is nowadays used for cell detection and classification in optical microscopy, during post-acquisition analysis. The microscopes are now fully automated and next expected to be smart, to make acquisition decisions based on the images. It calls for analysing them on the fly. Biology further imposes training on a reduced dataset due to cost and time to prepare the samples and… ▽ More Artificial intelligence is nowadays used for cell detection and classification in optical microscopy, during post-acquisition analysis. The microscopes are now fully automated and next expected to be smart, to make acquisition decisions based on the images. It calls for analysing them on the fly. Biology further imposes training on a reduced dataset due to cost and time to prepare the samples and have the datasets annotated by experts. We propose here a real-time image processing, compliant with these specifications by balancing accurate detection and execution performance. We characterised the images using a generic, high-dimensional feature extractor. We then classified the images using machine learning for the sake of understanding the contribution of each feature in decision and execution time. We found that the non-linear-classifier random forests outperformed Fisher's linear discriminant. More importantly, the most discriminant and time-consuming features could be excluded without any significant loss in accuracy, offering a substantial gain in execution time. It suggests a feature-group redundancy likely related to the biology of the observed cells. We offer a method to select fast and discriminant features. In our assay, a 79.6 $\pm$ 2.4 % accurate classification of a cell took 68.7 $\pm$ 3.5 ms (mean $\pm$ SD, 5-fold cross-validation nested in 10 bootstrap repeats), corresponding to 14 cells per second, dispatched into 8 phases of the cell cycle using 12 feature-groups and operating a consumer market ARM-based embedded system. Interestingly, a simple neural network offered similar performances paving the way to faster training and classification, using parallel execution on a general-purpose graphic processing unit. Finally, this strategy is also usable for deep neural networks paving the way to optimising these algorithms for smart microscopy. △ Less

Submitted 18 December, 2020; originally announced December 2020.

MSC Class: 68T45; 92C37; 68U10 ACM Class: I.4.8; J.3; C.3

Implementation of Conditional-Phase Gates based on tunable ZZ-Interactions

Authors: Michele C. Collodo, Johannes Herrmann, Nathan Lacroix, Christian Kraglund Andersen, Ants Remm, Stefania Lazar, Jean-Claude Besse, Theo Walter, Andreas Wallraff, Christopher Eichler

Abstract: High fidelity two-qubit gates exhibiting low crosstalk are essential building blocks for gate-based quantum information processing. In superconducting circuits two-qubit gates are typically based either on RF-controlled interactions or on the in-situ tunability of qubit frequencies. Here, we present an alternative approach using a tunable cross-Kerr-type ZZ-interaction between two qubits, which we… ▽ More High fidelity two-qubit gates exhibiting low crosstalk are essential building blocks for gate-based quantum information processing. In superconducting circuits two-qubit gates are typically based either on RF-controlled interactions or on the in-situ tunability of qubit frequencies. Here, we present an alternative approach using a tunable cross-Kerr-type ZZ-interaction between two qubits, which we realize by a flux-tunable coupler element. We control the ZZ-coupling rate over three orders of magnitude to perform a rapid (38 ns), high-contrast, low leakage (0.14 %) conditional-phase CZ gate with a fidelity of 97.9 % without relying on the resonant interaction with a non-computational state. Furthermore, by exploiting the direct nature of the ZZ-coupling, we easily access the entire conditional-phase gate family by adjusting only a single control parameter. △ Less

Submitted 18 May, 2020; originally announced May 2020.

Journal ref: Phys. Rev. Lett. 125, 240502 (2020)

Building hierarchical martensite

Authors: Stefan Schwabe, Robert Niemann, Anja Backen, Daniel Wolf, Christine Damm, Tina Walter, Hanus Seiner, Oleg Heczko, Kornelius Nielsch, Sebastian Fähler

Abstract: Martensitic materials show a complex, hierarchical microstructure containing structural domains separated by various types of twin boundaries. Several concepts exist to describe this microstructure on each length scale, however, there is no comprehensive approach bridging the whole range from the nano- up to the macroscopic scale. Here, we describe for a Ni-Mn-based Heusler alloy how this hierarch… ▽ More Martensitic materials show a complex, hierarchical microstructure containing structural domains separated by various types of twin boundaries. Several concepts exist to describe this microstructure on each length scale, however, there is no comprehensive approach bridging the whole range from the nano- up to the macroscopic scale. Here, we describe for a Ni-Mn-based Heusler alloy how this hierarchical microstructure is built from scratch with just one key parameter: the tetragonal distortion of the basic building block at the atomic level. Based on this initial block, we introduce five successive levels of nested building blocks. At each level, a larger building block is formed by twinning the preceding one to minimise the relevant energy contributions locally. This naturally explains the occurrence of different types of twin boundaries. We compare this scale-bridging approach of nested building blocks with experiments in real and reciprocal space. Our approach of nested building blocks is versatile as it can be applied to the broad class of functional materials exhibiting diffusionless transformations. △ Less

Submitted 21 April, 2020; originally announced April 2020.

Comments: 25 pages, including supplementary

Journal ref: Advanced Functional Materials (2020) 2005715

A new 1.375-approximation algorithm for Sorting By Transpositions

Authors: L. A. G. Silva, L. A. B. Kowada, N. R. Rocco, M. E. M. T. Walter

Abstract: In genome rearrangements, the mutational event transposition swaps two adjacent blocks of genes in one chromosome. The Transposition Distance Problem (TDP) aims to find the minimum number of transpositions required to transform one chromosome into another, both represented as permutations. The TDP can be reduced to the problem of Sorting by Transpositions (SBT). SBT is $\mathcal{NP}$-hard and th… ▽ More In genome rearrangements, the mutational event transposition swaps two adjacent blocks of genes in one chromosome. The Transposition Distance Problem (TDP) aims to find the minimum number of transpositions required to transform one chromosome into another, both represented as permutations. The TDP can be reduced to the problem of Sorting by Transpositions (SBT). SBT is $\mathcal{NP}$-hard and the best approximation algorithm with a $1.375$ ratio was proposed by Elias and Hartman. Their algorithm employs simplification, a technique used to transform an input permutation $π$ into a simple permutation $\hatπ$, presumably easier to handle with. The permutation $\hatπ$ is obtained by inserting new symbols into $π$ in a way that the lower bound of the transposition distance of $π$ is kept on $\hatπ$. The simplification is guaranteed to keep the lower bound, not the transposition distance. In this paper, we first show that the algorithm of Elias and Hartman (EH algorithm) may require one extra transposition above the approximation ratio of $1.375$, depending on how the input permutation is simplified. Next, using an algebraic approach, we propose a new upper bound for the transposition distance and a new $1.375$-approximation algorithm to solve SBT skip** simplification and ensuring the approximation ratio of $1.375$ for all $S_n$. We implemented our algorithm and EH's. Regarding the implementation of the EH algorithm, two issues needed to be fixed. We tested both algorithms against all permutations of size $n$, $2\leq n \leq 12$. The results show that the EH algorithm exceeds the approximation ratio of $1.375$ for permutations with a size greater than $7$. Finally, we investigate the performance of both implementations on longer permutations of maximum length $500$. △ Less

Submitted 4 November, 2021; v1 submitted 30 January, 2020; originally announced January 2020.

Parity Detection of Propagating Microwave Fields

Authors: Jean-Claude Besse, Simone Gasparinetti, Michele C. Collodo, Theo Walter, Ants Remm, Jonas Krause, Christopher Eichler, Andreas Wallraff

Abstract: The parity of the number of elementary excitations present in a quantum system provides important insights into its physical properties. Parity measurements are used, for example, to tomographically reconstruct quantum states or to determine if a decay of an excitation has occurred, information which can be used for quantum error correction in computation or communication protocols. Here we demons… ▽ More The parity of the number of elementary excitations present in a quantum system provides important insights into its physical properties. Parity measurements are used, for example, to tomographically reconstruct quantum states or to determine if a decay of an excitation has occurred, information which can be used for quantum error correction in computation or communication protocols. Here we demonstrate a versatile parity detector for propagating microwaves, which distinguishes between radiation fields containing an even or odd number n of photons, both in a single-shot measurement and without perturbing the parity of the detected field. We showcase applications of the detector for direct Wigner tomography of propagating microwaves and heralded generation of Schrödinger cat states. This parity detection scheme is applicable over a broad frequency range and may prove useful, for example, for heralded or fault-tolerant quantum communication protocols. △ Less

Submitted 20 December, 2019; originally announced December 2019.

Journal ref: Phys. Rev. X 10, 011046 (2020)

Quantum communication with time-bin encoded microwave photons

Authors: Philipp Kurpiers, Marek Pechal, Baptiste Royer, Paul Magnard, Theo Walter, Johannes Heinsoo, Yves Salathé, Abdulkadir Akin, Simon Storz, Jean-Claude Besse, Simone Gasparinetti, Alexandre Blais, Andreas Wallraff

Abstract: Heralding techniques are useful in quantum communication to circumvent losses without resorting to error correction schemes or quantum repeaters. Such techniques are realized, for example, by monitoring for photon loss at the receiving end of the quantum link while not disturbing the transmitted quantum state. We describe and experimentally benchmark a scheme that incorporates error detection in a… ▽ More Heralding techniques are useful in quantum communication to circumvent losses without resorting to error correction schemes or quantum repeaters. Such techniques are realized, for example, by monitoring for photon loss at the receiving end of the quantum link while not disturbing the transmitted quantum state. We describe and experimentally benchmark a scheme that incorporates error detection in a quantum channel connecting two transmon qubits using traveling microwave photons. This is achieved by encoding the quantum information as a time-bin superposition of a single photon, which simultaneously realizes high communication rates and high fidelities. The presented scheme is straightforward to implement in circuit QED and is fully microwave-controlled, making it an interesting candidate for future modular quantum computing architectures. △ Less

Submitted 19 November, 2018; originally announced November 2018.

Journal ref: Phys. Rev. Applied 12, 044067 (2019)

Challenging local realism with human choices

Authors: The BIG Bell Test Collaboration, C. Abellán, A. Acín, A. Alarcón, O. Alibart, C. K. Andersen, F. Andreoli, A. Beckert, F. A. Beduini, A. Bendersky, M. Bentivegna, P. Bierhorst, D. Burchardt, A. Cabello, J. Cariñe, S. Carrasco, G. Carvacho, D. Cavalcanti, R. Chaves, J. Cortés-Vega, A. Cuevas, A. Delgado, H. de Riedmatten, C. Eichler, P. Farrera , et al. (83 additional authors not shown)

Abstract: A Bell test is a randomized trial that compares experimental observations against the philosophical worldview of local realism. A Bell test requires spatially distributed entanglement, fast and high-efficiency detection and unpredictable measurement settings. Although technology can satisfy the first two of these requirements, the use of physical devices to choose settings in a Bell test involves… ▽ More A Bell test is a randomized trial that compares experimental observations against the philosophical worldview of local realism. A Bell test requires spatially distributed entanglement, fast and high-efficiency detection and unpredictable measurement settings. Although technology can satisfy the first two of these requirements, the use of physical devices to choose settings in a Bell test involves making assumptions about the physics that one aims to test. Bell himself noted this weakness in using physical setting choices and argued that human `free will' could be used rigorously to ensure unpredictability in Bell tests. Here we report a set of local-realism tests using human choices, which avoids assumptions about predictability in physics. We recruited about 100,000 human participants to play an online video game that incentivizes fast, sustained input of unpredictable selections and illustrates Bell-test methodology. The participants generated 97,347,490 binary choices, which were directed via a scalable web platform to 12 laboratories on five continents, where 13 experiments tested local realism using photons, single atoms, atomic ensembles, and superconducting devices. Over a 12-hour period on 30 November 2016, participants worldwide provided a sustained data flow of over 1,000 bits per second to the experiments, which used different human-generated data to choose each measurement setting. The observed correlations strongly contradict local realism and other realistic positions in bipartite and tripartite scenarios. Project outcomes include closing the `freedom-of-choice loophole' (the possibility that the setting choices are influenced by `hidden variables' to correlate with the particle properties), the utilization of video-game methods for rapid collection of human generated randomness, and the use of networking techniques for global participation in experimental science. △ Less

Submitted 9 November, 2018; v1 submitted 11 May, 2018; originally announced May 2018.

Comments: This version includes minor changes resulting from reviewer and editorial input. Abstract shortened to fit within arXiv limits

Journal ref: Nature, volume 557, pages 212-216 (2018)

Rapid high-fidelity multiplexed readout of superconducting qubits

Authors: Johannes Heinsoo, Christian Kraglund Andersen, Ants Remm, Sebastian Krinner, Theodore Walter, Yves Salathé, Simone Gasparinetti, Jean-Claude Besse, Anton Potočnik, Christopher Eichler, Andreas Wallraff

Abstract: The duration and fidelity of qubit readout is a critical factor for applications in quantum information processing as it limits the fidelity of algorithms which reuse qubits after measurement or apply feedback based on the measurement result. Here we present fast multiplexed readout of five qubits in a single 1.2 GHz wide readout channel. Using a readout pulse length of 80 ns and populating readou… ▽ More The duration and fidelity of qubit readout is a critical factor for applications in quantum information processing as it limits the fidelity of algorithms which reuse qubits after measurement or apply feedback based on the measurement result. Here we present fast multiplexed readout of five qubits in a single 1.2 GHz wide readout channel. Using a readout pulse length of 80 ns and populating readout resonators for less than 250 ns we find an average correct assignment probability for the five measured qubits to be $97\%$. The differences between the individual readout errors and those found when measuring the qubits simultaneously are within $1\%$. We employ individual Purcell filters for each readout resonator to suppress off-resonant driving, which we characterize by the dephasing imposed on unintentionally measured qubits. We expect the here presented readout scheme to become particularly useful for the selective readout of individual qubits in multi-qubit quantum processors. △ Less

Submitted 24 January, 2018; originally announced January 2018.

Comments: 13 pages, 10 figures

Journal ref: Phys. Rev. Applied 10, 034040 (2018)

Fast and Unconditional All-Microwave Reset of a Superconducting Qubit

Authors: Paul Magnard, Philipp Kurpiers, Baptiste Royer, Theo Walter, Jean-Claude Besse, Simone Gasparinetti, Marek Pechal, Johannes Heinsoo, Simon Storz, Alexandre Blais, Andreas Wallraff

Abstract: Active qubit reset is a key operation in many quantum algorithms, and particularly in error correction codes. Here, we experimentally demonstrate a reset scheme of a three level transmon artificial atom coupled to a large bandwidth resonator. The reset protocol uses a microwave-induced interaction between the $|f,0\rangle$ and $|g,1\rangle$ states of the coupled transmon-resonator system, with… ▽ More Active qubit reset is a key operation in many quantum algorithms, and particularly in error correction codes. Here, we experimentally demonstrate a reset scheme of a three level transmon artificial atom coupled to a large bandwidth resonator. The reset protocol uses a microwave-induced interaction between the $|f,0\rangle$ and $|g,1\rangle$ states of the coupled transmon-resonator system, with $|g\rangle$ and $|f\rangle$ denoting the ground and second excited states of the transmon, and $|0\rangle$ and $|1\rangle$ the photon Fock states of the resonator. We characterize the reset process and demonstrate reinitialization of the transmon-resonator system to its ground state with $0.2\%$ residual excitation in less than $500 \, \rm{ns}$. Our protocol is of practical interest as it has no requirements on the architecture, beyond those for fast and efficient single-shot readout of the transmon, and does not require feedback. △ Less

Submitted 23 January, 2018; originally announced January 2018.

Journal ref: Phys. Rev. Lett. 121, 060502 (2018)

Deterministic Quantum State Transfer and Generation of Remote Entanglement using Microwave Photons

Authors: Philipp Kurpiers, Paul Magnard, Theo Walter, Baptiste Royer, Marek Pechal, Johannes Heinsoo, Yves Salathé, Abdulkadir Akin, Simon Storz, Jean-Claude Besse, Simone Gasparinetti, Alexandre Blais, Andreas Wallraff

Abstract: Sharing information coherently between nodes of a quantum network is at the foundation of distributed quantum information processing. In this scheme, the computation is divided into subroutines and performed on several smaller quantum registers connected by classical and quantum channels. A direct quantum channel, which connects nodes deterministically, rather than probabilistically, is advantageo… ▽ More Sharing information coherently between nodes of a quantum network is at the foundation of distributed quantum information processing. In this scheme, the computation is divided into subroutines and performed on several smaller quantum registers connected by classical and quantum channels. A direct quantum channel, which connects nodes deterministically, rather than probabilistically, is advantageous for fault-tolerant quantum computation because it reduces the threshold requirements and can achieve larger entanglement rates. Here, we implement deterministic state transfer and entanglement protocols between two superconducting qubits fabricated on separate chips. Superconducting circuits constitute a universal quantum node capable of sending, receiving, storing, and processing quantum information. Our implementation is based on an all-microwave cavity-assisted Raman process which entangles or transfers the qubit state of a transmon-type artificial atom to a time-symmetric itinerant single photon. We transfer qubit states at a rate of $50 \, \rm{kHz}$ using the emitted photons which are absorbed at the receiving node with a probability of $98.1 \pm 0.1 \%$ achieving a transfer process fidelity of $80.02 \pm 0.07 \%$. We also prepare on demand remote entanglement with a fidelity as high as $78.9 \pm 0.1 \%$. Our results are in excellent agreement with numerical simulations based on a master equation description of the system. This deterministic quantum protocol has the potential to be used as a backbone of surface code quantum error correction across different nodes of a cryogenic network to realize large-scale fault-tolerant quantum computation in the circuit quantum electrodynamic architecture. △ Less

Submitted 22 December, 2017; originally announced December 2017.

Comments: 11 pages 8 Figures

Journal ref: Nature 558, 264-267 (2018)

Single-Shot Quantum Non-Demolition Detection of Itinerant Microwave Photons

Authors: Jean-Claude Besse, Simone Gasparinetti, Michele C. Collodo, Theo Walter, Philipp Kurpiers, Marek Pechal, Christopher Eichler, Andreas Wallraff

Abstract: Single-photon detection is an essential component in many experiments in quantum optics, but remains challenging in the microwave domain. We realize a quantum non-demolition detector for propagating microwave photons and characterize its performance using a single-photon source. To this aim we implement a cavity-assisted conditional phase gate between the incoming photon and a superconducting arti… ▽ More Single-photon detection is an essential component in many experiments in quantum optics, but remains challenging in the microwave domain. We realize a quantum non-demolition detector for propagating microwave photons and characterize its performance using a single-photon source. To this aim we implement a cavity-assisted conditional phase gate between the incoming photon and a superconducting artificial atom. By reading out the state of this atom in single shot, we reach an internal photon detection fidelity of 71%, limited by the coherence properties of the qubit. By characterizing the coherence and average number of photons in the field reflected off the detector, we demonstrate its quantum non-demolition nature. We envisage applications in generating heralded remote entanglement between qubits and for realizing logic gates between propagating microwave photons. △ Less

Submitted 30 November, 2017; originally announced November 2017.

Journal ref: Phys. Rev. X 8, 021003 (2018)

Parikh-reducing Church-Rosser representations for some classes of regular languages

Authors: Tobias Walter

Abstract: In this paper the concept of Parikh-reducing Church-Rosser systems is studied. It is shown that for two classes of regular languages there exist such systems which describe the languages using finitely many equivalence classes of the rewriting system. The two classes are: 1.) the class of all regular languages such that the syntactic monoid contains only abelian groups and 2.) the class of all gro… ▽ More In this paper the concept of Parikh-reducing Church-Rosser systems is studied. It is shown that for two classes of regular languages there exist such systems which describe the languages using finitely many equivalence classes of the rewriting system. The two classes are: 1.) the class of all regular languages such that the syntactic monoid contains only abelian groups and 2.) the class of all group languages over a two-letter alphabet. The construction of the systems yield a monoid representation such that all subgroups are abelian. Additionally, the complexity of those representations is studied. △ Less

Submitted 29 March, 2017; originally announced March 2017.

Realizing Rapid, High-Fidelity, Single-Shot Dispersive Readout of Superconducting Qubits

Authors: T. Walter, P. Kurpiers, S. Gasparinetti, P. Magnard, A. Potocnik, Y. Salathe, M. Pechal, M. Mondal, M. Oppliger, C. Eichler, A. Wallraff

Abstract: The speed of quantum gates and measurements is a decisive factor for the overall fidelity of quantum protocols when performed on physical qubits with finite coherence time. Reducing the time required to distinguish qubit states with high fidelity is therefore a critical goal in quantum information science. The state-of-the-art readout of superconducting qubits is based on the dispersive interactio… ▽ More The speed of quantum gates and measurements is a decisive factor for the overall fidelity of quantum protocols when performed on physical qubits with finite coherence time. Reducing the time required to distinguish qubit states with high fidelity is therefore a critical goal in quantum information science. The state-of-the-art readout of superconducting qubits is based on the dispersive interaction with a readout resonator. Here, we bring this technique to its current limit and demonstrate how the careful design of system parameters leads to fast and high-fidelity measurements without affecting qubit coherence. We achieve this result by increasing the dispersive interaction strength, by choosing an optimal linewidth of the readout resonator, by employing a Purcell filter, and by utilizing phase-sensitive parametric amplification. In our experiment, we measure 98.25% readout fidelity in only 48 ns, when minimizing read-out time, and 99.2% in 88 ns, when maximizing the fidelity, limited predominantly by the qubit lifetime of 7.6 us. The presented scheme is also expected to be suitable for integration into a multiplexed readout architecture. △ Less

Submitted 25 January, 2017; v1 submitted 24 January, 2017; originally announced January 2017.

Comments: 10 pages, 7 figures; fixed pdf compile bug with the e' in Y. Salathe

Journal ref: Phys. Rev. Applied 7, 054020 (2017)

Characterizing the attenuation of coaxial and rectangular microwave-frequency waveguides at cryogenic temperatures

Authors: P. Kurpiers, T. Walter, P. Magnard, Y. Salathe, A. Wallraff

Abstract: Low-loss waveguides are required for quantum communication at distances beyond the chip-scale for any low-temperature solid-state implementation of quantum information processors. We measure and analyze the attenuation constant of commercially available microwave-frequency waveguides down to millikelvin temperatures and single photon levels. More specifically, we characterize the frequency-depende… ▽ More Low-loss waveguides are required for quantum communication at distances beyond the chip-scale for any low-temperature solid-state implementation of quantum information processors. We measure and analyze the attenuation constant of commercially available microwave-frequency waveguides down to millikelvin temperatures and single photon levels. More specifically, we characterize the frequency-dependent loss of a range of coaxial and rectangular microwave waveguides down to $0.005\,\rm{dB}/\rm{m}$ using a resonant-cavity technique. We study the loss tangent and relative permittivity of commonly used dielectric waveguide materials by measurements of the internal quality factors and their comparison with established loss models. The results of our characterization are relevant for accurately predicting the signal levels at the input of cryogenic devices, for reducing the loss in any detection chain, and for estimating the heat load induced by signal dissipation in cryogenic systems. △ Less

Submitted 23 December, 2016; originally announced December 2016.

Characterizing classes of regular languages using prefix codes of bounded synchronization delay

Authors: Volker Diekert, Tobias Walter

Abstract: In this paper we continue a classical work of Schützenberger on codes with bounded synchronization delay. He was interested to characterize those regular languages where the groups in the syntactic monoid belong to a variety $H$. He allowed operations on the language side which are union, intersection, concatenation and modified Kleene-star involving a map** of a prefix code of bounded synchroni… ▽ More In this paper we continue a classical work of Schützenberger on codes with bounded synchronization delay. He was interested to characterize those regular languages where the groups in the syntactic monoid belong to a variety $H$. He allowed operations on the language side which are union, intersection, concatenation and modified Kleene-star involving a map** of a prefix code of bounded synchronization delay to a group $G\in H$, but no complementation. In our notation this leads to the language classes $SD_G(A^\infty)$ and $SD_H(A^\infty$). Our main result shows that $SD_H(A^\infty)$ always corresponds to the languages having syntactic monoids where all subgroups are in $H$. Schützenberger showed this for a variety $H$ if $H$ contains Abelian groups, only. Our method shows the general result for all $H$ directly on finite and infinite words. Furthermore, we introduce the notion of local Rees products which refers to a simple type of classical Rees extensions. We give a decomposition of a monoid in terms of its groups and local Rees products. This gives a somewhat similar, but simpler decomposition than in Rhodes' synthesis theorem. Moreover, we need a singly exponential number of operations, only. Finally, our decomposition yields an answer to a question in a recent paper of Almeida and Klíma about varieties that are closed under Rees products. △ Less

Submitted 29 February, 2016; originally announced February 2016.

Level Two of the Quantifier Alternation Hierarchy over Infinite Words

Authors: Manfred Kufleitner, Tobias Walter

Abstract: The study of various decision problems for logic fragments has a long history in computer science. This paper is on the membership problem for a fragment of first-order logic over infinite words; the membership problem asks for a given language whether it is definable in some fixed fragment. The alphabetic topology was introduced as part of an effective characterization of the fragment $Σ_2$ over… ▽ More The study of various decision problems for logic fragments has a long history in computer science. This paper is on the membership problem for a fragment of first-order logic over infinite words; the membership problem asks for a given language whether it is definable in some fixed fragment. The alphabetic topology was introduced as part of an effective characterization of the fragment $Σ_2$ over infinite words. Here, $Σ_2$ consists of the first-order formulas with two blocks of quantifiers, starting with an existential quantifier. Its Boolean closure is $\mathbb{B}Σ_2$. Our first main result is an effective characterization of the Boolean closure of the alphabetic topology, that is, given an $ω$-regular language $L$, it is decidable whether $L$ is a Boolean combination of open sets in the alphabetic topology. This is then used for transferring Place and Zeitoun's recent decidability result for $\mathbb{B}Σ_2$ from finite to infinite words. △ Less

Submitted 21 September, 2015; originally announced September 2015.

Assessment of algorithms for mitosis detection in breast cancer histopathology images

Authors: Mitko Veta, Paul J. van Diest, Stefan M. Willems, Haibo Wang, Anant Madabhushi, Angel Cruz-Roa, Fabio Gonzalez, Anders B. L. Larsen, Jacob S. Vestergaard, Anders B. Dahl, Dan C. Cireşan, Jürgen Schmidhuber, Alessandro Giusti, Luca M. Gambardella, F. Boray Tek, Thomas Walter, Ching-Wei Wang, Satoshi Kondo, Bogdan J. Matuszewski, Frederic Precioso, Violet Snell, Josef Kittler, Teofilo E. de Campos, Adnan M. Khan, Nasir M. Rajpoot , et al. (4 additional authors not shown)

Abstract: The proliferative activity of breast tumors, which is routinely estimated by counting of mitotic figures in hematoxylin and eosin stained histology sections, is considered to be one of the most important prognostic markers. However, mitosis counting is laborious, subjective and may suffer from low inter-observer agreement. With the wider acceptance of whole slide images in pathology labs, automati… ▽ More The proliferative activity of breast tumors, which is routinely estimated by counting of mitotic figures in hematoxylin and eosin stained histology sections, is considered to be one of the most important prognostic markers. However, mitosis counting is laborious, subjective and may suffer from low inter-observer agreement. With the wider acceptance of whole slide images in pathology labs, automatic image analysis has been proposed as a potential solution for these issues. In this paper, the results from the Assessment of Mitosis Detection Algorithms 2013 (AMIDA13) challenge are described. The challenge was based on a data set consisting of 12 training and 11 testing subjects, with more than one thousand annotated mitotic figures by multiple observers. Short descriptions and results from the evaluation of eleven methods are presented. The top performing method has an error rate that is comparable to the inter-observer agreement among pathologists. △ Less

Submitted 21 November, 2014; originally announced November 2014.

Comments: 23 pages, 5 figures, accepted for publication in the journal Medical Image Analysis

One Quantifier Alternation in First-Order Logic with Modular Predicates

Authors: Manfred Kufleitner, Tobias Walter

Abstract: Adding modular predicates yields a generalization of first-order logic FO over words. The expressive power of FO[<,MOD] with order comparison $x<y$ and predicates for $x \equiv i \mod n$ has been investigated by Barrington, Compton, Straubing and Therien. The study of FO[<,MOD]-fragments was initiated by Chaubard, Pin and Straubing. More recently, Dartois and Paperman showed that definability in t… ▽ More Adding modular predicates yields a generalization of first-order logic FO over words. The expressive power of FO[<,MOD] with order comparison $x<y$ and predicates for $x \equiv i \mod n$ has been investigated by Barrington, Compton, Straubing and Therien. The study of FO[<,MOD]-fragments was initiated by Chaubard, Pin and Straubing. More recently, Dartois and Paperman showed that definability in the two-variable fragment FO2[<,MOD] is decidable. In this paper we continue this line of work. We give an effective algebraic characterization of the word languages in Sigma2[<,MOD]. The fragment Sigma2 consists of first-order formulas in prenex normal form with two blocks of quantifiers starting with an existential block. In addition we show that Delta2[<,MOD], the largest subclass of Sigma2[<,MOD] which is closed under negation, has the same expressive power as two-variable logic FO2[<,MOD]. This generalizes the result FO2[<] = Delta2[<] of Therien and Wilke to modular predicates. As a byproduct, we obtain another decidable characterization of FO2[<,MOD]. △ Less

Submitted 1 July, 2014; v1 submitted 18 October, 2013; originally announced October 2013.

ACM Class: F.4.1; F.4.3

Regular Languages are Church-Rosser Congruential

Authors: Volker Diekert, Manfred Kufleitner, Klaus Reinhardt, Tobias Walter

Abstract: This paper proves a long standing conjecture in formal language theory. It shows that all regular languages are Church-Rosser congruential. The class of Church-Rosser congruential languages was introduced by McNaughton, Narendran, and Otto in 1988. A language L is Church-Rosser congruential, if there exists a finite confluent, and length-reducing semi-Thue system S such that L is a finite union of… ▽ More This paper proves a long standing conjecture in formal language theory. It shows that all regular languages are Church-Rosser congruential. The class of Church-Rosser congruential languages was introduced by McNaughton, Narendran, and Otto in 1988. A language L is Church-Rosser congruential, if there exists a finite confluent, and length-reducing semi-Thue system S such that L is a finite union of congruence classes modulo S. It was known that there are deterministic linear context-free languages which are not Church-Rosser congruential, but on the other hand it was strongly believed that all regular language are of this form. Actually, this paper proves a more general result. △ Less

Submitted 6 February, 2012; originally announced February 2012.

MSC Class: 68Q42 (Primary) 68Q45; 68Q70 (Secondary) ACM Class: F.4.2; F.4.3

Search for First-Generation Scalar Leptoquarks in $\bm{p \bar{p}}$ collisions at $\sqrt{s}$=1.96 TeV

Authors: The CDF Collaboration, D. Acosta, J. Adelman, T. Affolder, T. Akimoto, M. G. Albrow, D. Ambrose, S. Amerio, D. Amidei, A. Anastassov, K. Anikeev, A. Annovi, J. Antos, M. Aoki, G. Apollinari, T. Arisawa, J-F. Arguin, A. Artikov, W. Ashmanskas, A. Attal, F. Azfar, P. Azzi-Bacchetta, N. Bacchetta, H. Bachacou, W. Badgett , et al. (605 additional authors not shown)

Abstract: We report on a search for pair production of first-generation scalar leptoquarks ($LQ$) in $p \bar{p}$ collisions at $\sqrt{s}$=1.96 TeV using an integrated luminosity of 203 $pb^{-1}$ collected at the Fermilab Tevatron collider by the CDF experiment. We observe no evidence for $LQ$ production in the topologies arising from $LQ \bar{LQ} \to eqeq$ and $LQ \bar{LQ} \to eq νq$, and derive 95% C.L.… ▽ More We report on a search for pair production of first-generation scalar leptoquarks ($LQ$) in $p \bar{p}$ collisions at $\sqrt{s}$=1.96 TeV using an integrated luminosity of 203 $pb^{-1}$ collected at the Fermilab Tevatron collider by the CDF experiment. We observe no evidence for $LQ$ production in the topologies arising from $LQ \bar{LQ} \to eqeq$ and $LQ \bar{LQ} \to eq νq$, and derive 95% C.L. upper limits on the $LQ$ production cross section. %as a function of $β$, where $β$ is the branching fraction for $LQ \to eq$. The results are combined with those obtained from a separately reported CDF search in the topology arising from $LQ\bar{LQ} \to νq νq$ and 95% C.L. lower limits on the LQ mass as a function of $β= BR(LQ \to eq) $ are derived. The limits are 236, 205 and 145 GeV/c$^2$ for $β$ = 1, $β$ = 0.5 and $β$ = 0.1, respectively. △ Less

Submitted 29 June, 2005; originally announced June 2005.

Comments: submitted to PRL

Report number: FERMILAB-PUB-05-254-E

Journal ref: Phys.Rev.D72:051107,2005

Physics Analysis Expert PAX: First Applications

Authors: M. Erdmann, D. Hirschbuehl, C. Jung, S. Kappler, Y. Kemp, M. Kirsch, D. Miksat, C. Piasecki, G. Quast, K. Rabbertz, P. Schemitz, A. Schmidt, T. Walter, C. Weiser

Abstract: PAX (Physics Analysis Expert) is a novel, C++ based toolkit designed to assist teams in particle physics data analysis issues. The core of PAX are event interpretation containers, holding relevant information about and possible interpretations of a physics event. Providing this new level of abstraction beyond the results of the detector reconstruction programs, PAX facilitates the buildup and us… ▽ More PAX (Physics Analysis Expert) is a novel, C++ based toolkit designed to assist teams in particle physics data analysis issues. The core of PAX are event interpretation containers, holding relevant information about and possible interpretations of a physics event. Providing this new level of abstraction beyond the results of the detector reconstruction programs, PAX facilitates the buildup and use of modern analysis factories. Class structure and user command syntax of PAX are set up to support expert teams as well as newcomers in preparing for the challenges expected to arise in the data analysis at future hadron colliders. △ Less

Submitted 11 June, 2003; originally announced June 2003.

Comments: Talk from the 2003 Computing in High Energy and Nuclear Physics (CHEP03), La Jolla, Ca, USA, March 2003, 7 pages, LaTeX, 10 eps figures. PSN THLT008

Report number: IEKP-KA/2003-14

Dislocation Dynamics in Rayleigh-Bénard Convection

Authors: Th. Walter, W. Pesch, E. Bodenschatz

Abstract: Theoretical results on the dynamics of dislocations in Rayleigh-Bénard convection are reported both for Swift-Hohenberg models and the Boussinesq equations. For intermediate Prandtl numbers the motion of dislocations is found to be driven by the superposition of two independent contributions: (i) the Peach-Koehler force derived from the change of a Lyapunov potential with pattern wave number; (i… ▽ More Theoretical results on the dynamics of dislocations in Rayleigh-Bénard convection are reported both for Swift-Hohenberg models and the Boussinesq equations. For intermediate Prandtl numbers the motion of dislocations is found to be driven by the superposition of two independent contributions: (i) the Peach-Koehler force derived from the change of a Lyapunov potential with pattern wave number; (ii) a non-potential advection force on the dislocation core by its self-generated mean flow. Their competition allows for the first time to understand the experimentally observed bound dislocation pairs. △ Less

Submitted 23 December, 2002; originally announced December 2002.

Comments: 4 pages, submitted to PRL

Studies of aging and HV break down problems during development and operation of MSGC and GEM detectors for the Inner Tracking System of HERA-B

Authors: HERA-B Inner Tracker Collaboration, :, Y. Bagaturia, O. Baruth, H. B. Dreis, F. Eisele, I. Gorbunov, S. Gradl, W. Gradl, S. Hausmann, M. Hildebrandt, T. Hott, S. Keller, C. Krauss, B. Lomonosov, M. Negodaev, C. Richter, P. Robmann, B. Schmidt, U. Straumann, P. Truoel, S. Visbeck, T. Walter, C. Werner, U. Werthenbach , et al. (3 additional authors not shown)

Abstract: The results of five years of development of the inner tracking system of the HERA-B experiment and first experience from the data taking period of the year 2000 are reported. The system contains 184 chambers, covering a sensitive area of about 20 * 20 cm2 each. The detector is based on microstrip gas counters (MSGCs) with diamond like coated (DLC) glass wafers and gas electron multipliers (GEMs)… ▽ More The results of five years of development of the inner tracking system of the HERA-B experiment and first experience from the data taking period of the year 2000 are reported. The system contains 184 chambers, covering a sensitive area of about 20 * 20 cm2 each. The detector is based on microstrip gas counters (MSGCs) with diamond like coated (DLC) glass wafers and gas electron multipliers (GEMs). The main problems in the development phase were gas discharges in intense hadron beams and aging in a high radiation dose environment. The observation of gas discharges which damage the electrode structure of the MSGC led to the addition of the GEM as a first amplification step. Spurious sparking at the GEM cannot be avoided completely. It does not affect the GEM itself but can produce secondary damage of the MSGC if the electric field between the GEM and the MSGC is above a threshold depending on operation conditions. We observed that aging does not only depend on the dose but also on the spot size of the irradiated area. Ar-DME mixtures had to be abandoned whereas a mixture of 70% Ar and 30% CO2 showed no serious aging effects up to about 40 mC/cm deposited charge on the anodes. X-ray measurements indicate that the DLC of the MSGC is deteriorated by the gas amplification process. As a consequence, long term gain variations are expected. The Inner Tracker has successfully participated in the data taking at HERA-B during summer 2000. △ Less

Submitted 9 April, 2002; originally announced April 2002.

Comments: 29 pages, 22 figures

Journal ref: Nucl.Instrum.Meth.A490:223,2002; ICFA Instrum.Bull.24:54-84,2002

Current-induced conductance switching in epitaxial La0.7Sr0.3MnO3/SrTiO3 multilayers

Authors: K. Doerr, K. -H. Mueller, T. Walter, M. Sahana, D. Eckert, K. Nenkov, L. Schultz, K. Brand, M. Lehmann

Abstract: We report on the non-linear in-plane electrical transport in coherently grown [La0.7Sr0.3MnO3/SrTiO3] multilayers with ultrathin (< 3 nm) single layers. Current-induced switching of the conductance, with low conductance at larger currents, is demonstrated. The conductance switching is modified under a magnetic field, resulting in an extremely large magnetoresistance of negative, or in a special… ▽ More We report on the non-linear in-plane electrical transport in coherently grown [La0.7Sr0.3MnO3/SrTiO3] multilayers with ultrathin (< 3 nm) single layers. Current-induced switching of the conductance, with low conductance at larger currents, is demonstrated. The conductance switching is modified under a magnetic field, resulting in an extremely large magnetoresistance of negative, or in a special case even positive, sign. Our results suggest a percolative nature of transport where a large local current density gives rise to a spin-polarizing and a thermal effect of current. △ Less

Submitted 29 December, 2000; originally announced December 2000.

Comments: 10 pages, 6 figures