-
Qudit inspired optimization for graph coloring
Authors:
David Jansen,
Timothy Heightman,
Luke Mortimer,
Ignacio Perito,
Antonio Acín
Abstract:
We introduce a quantum-inspired algorithm for Graph Coloring Problems (GCPs) that utilizes qudits in a product state, with each qudit representing a node in the graph and parameterized by d-dimensional spherical coordinates. We propose and benchmark two optimization strategies: qudit gradient descent (QdGD), initiating qudits in random states and employing gradient descent to minimize a cost funct…
▽ More
We introduce a quantum-inspired algorithm for Graph Coloring Problems (GCPs) that utilizes qudits in a product state, with each qudit representing a node in the graph and parameterized by d-dimensional spherical coordinates. We propose and benchmark two optimization strategies: qudit gradient descent (QdGD), initiating qudits in random states and employing gradient descent to minimize a cost function, and qudit local quantum annealing (QdLQA), which adapts the local quantum annealing method to optimize an adiabatic transition from a tractable initial function to a problem-specific cost function. Our approaches are benchmarked against established solutions for standard GCPs, showing that our methods not only rival but frequently surpass the performance of recent state-of-the-art algorithms in terms of solution quality and computational efficiency. The adaptability of our algorithm and its high-quality solutions, achieved with minimal computational resources, point to an advancement in the field of quantum-inspired optimization, with potential applications extending to a broad spectrum of optimization problems.
△ Less
Submitted 2 June, 2024;
originally announced June 2024.
-
Molecular order induced charge transfer in a C$_{60}$-topological insulator moiré heterostructure
Authors:
Ram Prakash Pandeya,
Konstantin P. Shchukin,
Yannic Falke,
Gregor Mussler,
Jalil Abdur Rehman,
Nicolae Atodiresei,
Alexander V. Fedorov,
Boris V. Senkovskiy,
Daniel Jansen,
Giovanni Di Santo,
Luca Petaccia,
Alexander Grüneis
Abstract:
We synthesize and spectroscopically investigate monolayer C$_{60}$ on the topological insulator (TI) Bi$_4$Te$_3$. This C$_{60}$/Bi$_4$Te$_3$ heterostructure is characterized by excellent translational order in a novel (4 x 4) C$_{60}$ superstructure on a (9 x 9) unit of Bi$_4$Te$_3$. We measure the full two-dimensional energy band structure of C$_{60}$/Bi$_4$Te$_3$ using angle-resolved photoemiss…
▽ More
We synthesize and spectroscopically investigate monolayer C$_{60}$ on the topological insulator (TI) Bi$_4$Te$_3$. This C$_{60}$/Bi$_4$Te$_3$ heterostructure is characterized by excellent translational order in a novel (4 x 4) C$_{60}$ superstructure on a (9 x 9) unit of Bi$_4$Te$_3$. We measure the full two-dimensional energy band structure of C$_{60}$/Bi$_4$Te$_3$ using angle-resolved photoemission spectroscopy (ARPES). We find that C$_{60}$ accepts electrons from the TI at room temperature but no charge transfer occurs at low temperatures. We unravel this peculiar behaviour by Raman spectroscopy of C$_{60}$/Bi$_4$Te$_3$ and density functional theory (DFT) calculations of the electronegativity of C$_{60}$. Both methods are sensitive to orientational order of C$_{60}$. At low temperatures, Raman spectroscopy shows a dramatic intensity increase of the C$_{60}$ Raman signal, evidencing a transition to a rotationally ordered state. DFT reveals that the orientational order of C$_{60}$ at low temperatures has a higher electron affinity than at high temperatures. These results neatly explain the temperature-dependent charge transfer observed in ARPES. Our conclusions are supported by the appearance of a strong photoluminescence from C$_{60}$/Bi$_4$Te$_3$ at low temperatures.
△ Less
Submitted 15 May, 2024;
originally announced May 2024.
-
Tip-induced creation and Jahn-Teller distortions of sulfur vacancies in single-layer MoS$_{2}$
Authors:
Daniel Jansen,
Tfyeche Tounsi,
Jeison Fischer,
Arkady V. Krasheninnikov,
Thomas Michely,
Hannu-Pekka Komsa,
Wouter Jolie
Abstract:
We present an atomically precise technique to create sulfur vacancies and control their atomic configurations in single-layer MoS$_{2}$. It involves adsorbed Fe atoms and the tip of a scanning tunneling microscope, which enables single sulfur removal from the top sulfur layer at the initial position of Fe. Using scanning tunneling spectroscopy, we show that the STM tip can also induce two Jahn-Tel…
▽ More
We present an atomically precise technique to create sulfur vacancies and control their atomic configurations in single-layer MoS$_{2}$. It involves adsorbed Fe atoms and the tip of a scanning tunneling microscope, which enables single sulfur removal from the top sulfur layer at the initial position of Fe. Using scanning tunneling spectroscopy, we show that the STM tip can also induce two Jahn-Teller distorted states with reduced orbital symmetry in the sulfur vacancies. Density functional theory calculations rationalize our experimental results. Additionally, we provide evidence for molecule-like hybrid orbitals in artificially created sulfur vacancy dimers, which illustrates the potential of our technique for the development of extended defect lattices and tailored electronic band structures.
△ Less
Submitted 26 March, 2024; v1 submitted 18 January, 2024;
originally announced January 2024.
-
Linear-Time--Branching-Time Spectroscopy Accounting for Silent Steps
Authors:
Benjamin Bis**,
David N. Jansen
Abstract:
We provide the first generalized game characterization of van Glabbeek's linear-time--branching-time spectrum with silent steps. Thereby, one multi-dimensional energy game can be used to decide a wide array of behavioral equivalences between stability-respecting branching bisimilarity and weak trace equivalence in one go. To establish correctness, we relate attacker-winning energy budgets and dist…
▽ More
We provide the first generalized game characterization of van Glabbeek's linear-time--branching-time spectrum with silent steps. Thereby, one multi-dimensional energy game can be used to decide a wide array of behavioral equivalences between stability-respecting branching bisimilarity and weak trace equivalence in one go. To establish correctness, we relate attacker-winning energy budgets and distinguishing sublanguages of Hennessy--Milner logic characterized by eight dimensions of formula expressiveness.
△ Less
Submitted 17 October, 2023; v1 submitted 28 May, 2023;
originally announced May 2023.
-
Thermal and optical conductivity in the Holstein model at half filling and at finite temperature in the Luttinger-liquid and charge-density-wave regime
Authors:
David Jansen,
Fabian Heidrich-Meisner
Abstract:
Electron-phonon interactions play a key role in many branches of solid-state physics. Here, our focus is on the transport properties of one-dimensional systems, and we apply efficient real-time matrix-product state methods to compute the optical and thermal conductivities of Holstein chains at finite temperatures and filling. We validate our approach by comparison with analytical results applicabl…
▽ More
Electron-phonon interactions play a key role in many branches of solid-state physics. Here, our focus is on the transport properties of one-dimensional systems, and we apply efficient real-time matrix-product state methods to compute the optical and thermal conductivities of Holstein chains at finite temperatures and filling. We validate our approach by comparison with analytical results applicable to single polarons valid in the small polaron limit. Our work provides a systematic study of contributions to the thermal conductivity at finite frequencies and elucidates differences in the spectrum compared to the optical conductivity, covering both the Luttinger-liquid and charge-density-wave regimes. Finally, we demonstrate that our approach is capable of extracting the DC conductivities as well. Beyond this first application, several future extensions seem feasible, such as, the inclusion of dispersive phonons, different types of local electron-phonon coupling, and a systematic study of drag effects in this electron-phonon coupled system.
△ Less
Submitted 3 August, 2023; v1 submitted 25 April, 2023;
originally announced April 2023.
-
Finite-temperature optical conductivity with density-matrix renormalization group methods for the Holstein polaron and bipolaron with dispersive phonons
Authors:
David Jansen,
Janez Bonča,
Fabian Heidrich-Meisner
Abstract:
A comprehensive picture of polaron and bipolaron physics is essential to understand the optical absorption spectrum in many materials with electron-phonon interactions. In particular, the finite-temperature properties are of interest since they play an important role in many experiments. Here, we combine the parallel two-site time-dependent variational principle algorithm (p2TDVP) with local basis…
▽ More
A comprehensive picture of polaron and bipolaron physics is essential to understand the optical absorption spectrum in many materials with electron-phonon interactions. In particular, the finite-temperature properties are of interest since they play an important role in many experiments. Here, we combine the parallel two-site time-dependent variational principle algorithm (p2TDVP) with local basis optimization (LBO) and purification to calculate time-dependent current-current correlation functions. From this information, we extract the optical conductivity for the Holstein polaron and bipolaron with dispersive phonons at finite temperatures. For the polaron in the weak and intermediate electron-phonon coupling regimes, we analyze the influence of phonon dispersion relations on the spectra. For strong electron-phonon coupling, the known result of an asymmetric Gaussian is reproduced for a flat phonon band. For a finite phonon bandwidth, the center of the Gaussian is either shifted to larger or smaller frequencies, depending on the sign of the phonon hop**. We illustrate that this can be well understood by considering the Born-Oppenheimer surfaces. A similar behavior is seen for the bipolaron for strong coupling. For the bipolaron with weak and intermediate coupling strengths and a flat phonon band, we obtain two very different spectra. The latter also has a temperature-dependent resonance at a frequency below the phonon frequency.
△ Less
Submitted 26 October, 2022; v1 submitted 2 June, 2022;
originally announced June 2022.
-
Real-time non-adiabatic dynamics in the one-dimensional Holstein model: Trajectory-based vs exact methods
Authors:
Michael ten Brink,
Stefan Gräber,
Miroslav Hopjan,
David Jansen,
Jan Stolpp,
Fabian Heidrich-Meisner,
Peter E. Blöchl
Abstract:
We benchmark a set of quantum-chemistry methods, including multitrajectory Ehrenfest, fewest-switches surface-hop**, and multiconfigurational-Ehrenfest dynamics, against exact quantum-many-body techniques by studying real-time dynamics in the Holstein model. This is a paradigmatic model in condensed matter theory incorporating a local coupling of electrons to Einstein phonons. For the two-site a…
▽ More
We benchmark a set of quantum-chemistry methods, including multitrajectory Ehrenfest, fewest-switches surface-hop**, and multiconfigurational-Ehrenfest dynamics, against exact quantum-many-body techniques by studying real-time dynamics in the Holstein model. This is a paradigmatic model in condensed matter theory incorporating a local coupling of electrons to Einstein phonons. For the two-site and three-site Holstein model, we discuss the exact and quantum-chemistry methods in terms of the Born-Huang formalism, covering different initial states, which either start on a single Born-Oppenheimer surface, or with the electron localized to a single site. For extended systems with up to 51 sites, we address both the physics of single Holstein polarons and the dynamics of charge-density waves at finite electron densities. For these extended systems, we compare the quantum-chemistry methods to exact dynamics obtained from time-dependent density matrix renormalization group calculations with local basis optimization (DMRG-LBO). We observe that the multitrajectory Ehrenfest method, in general, only captures the ultrashort time dynamics accurately. In contrast, the surface-hop** method with suitable corrections provides a much better description of the long-time behavior but struggles with the short-time description of coherences between different Born-Oppenheimer states. We show that the multiconfigurational Ehrenfest method yields a significant improvement over the multitrajectory Ehrenfest method and can be converged to the exact results in small systems with moderate computational efforts. We further observe that for extended systems, this convergence is slower with respect to the number of configurations. Our benchmark study demonstrates that DMRG-LBO is a useful tool for assessing the quality of the quantum-chemistry methods.
△ Less
Submitted 30 June, 2022; v1 submitted 14 March, 2022;
originally announced March 2022.
-
Deciding All Behavioral Equivalences at Once: A Game for Linear-Time--Branching-Time Spectroscopy
Authors:
Benjamin Bis**,
David N. Jansen,
Uwe Nestmann
Abstract:
We introduce a generalization of the bisimulation game that finds distinguishing Hennessy-Milner logic formulas from every finitary, subformula-closed language in van Glabbeek's linear-time--branching-time spectrum between two finite-state processes. We identify the relevant dimensions that measure expressive power to yield formulas belonging to the coarsest distinguishing behavioral preorders and…
▽ More
We introduce a generalization of the bisimulation game that finds distinguishing Hennessy-Milner logic formulas from every finitary, subformula-closed language in van Glabbeek's linear-time--branching-time spectrum between two finite-state processes. We identify the relevant dimensions that measure expressive power to yield formulas belonging to the coarsest distinguishing behavioral preorders and equivalences; the compared processes are equivalent in each coarser behavioral equivalence from the spectrum. We prove that the induced algorithm can determine the best fit of (in)equivalences for a pair of processes.
△ Less
Submitted 8 August, 2022; v1 submitted 30 September, 2021;
originally announced September 2021.
-
Charge density wave breakdown in a heterostructure with electron-phonon coupling
Authors:
David Jansen,
Christian Jooss,
Fabian Heidrich-Meisner
Abstract:
Understanding the influence of vibrational degrees of freedom on transport through a heterostructure poses considerable theoretical and numerical challenges. In this work, we use the density-matrix renormalization group (DMRG) method together with local basis optimization (LBO) to study the half-filled Holstein model in the presence of a linear potential, either isolated or coupled to tight-bindin…
▽ More
Understanding the influence of vibrational degrees of freedom on transport through a heterostructure poses considerable theoretical and numerical challenges. In this work, we use the density-matrix renormalization group (DMRG) method together with local basis optimization (LBO) to study the half-filled Holstein model in the presence of a linear potential, either isolated or coupled to tight-binding leads. In both cases, we observe a decay of charge-density-wave (CDW) states at a sufficiently strong potential strength. Local basis optimization selects the most important linear combinations of local oscillator states to span the local phonon space. These states are referred to as optimal modes. We show that many of these local optimal modes are needed to capture the dynamics of the decay, that the most significant optimal mode on the initially occupied sites remains well described by a coherent-state typical for small polarons, and that those on the initially empty sites deviate from the coherent-state form. Additionally, we compute the current through the structure in the metallic regime as a function of voltage. For small voltages, we reproduce results for the Luttinger parameters. As the voltage is increased, the effect of larger electron-phonon coupling strengths becomes prominent. Further, the most significant optimal mode remains almost unchanged when going from the ground state to the current-carrying state in the metallic regime.
△ Less
Submitted 16 November, 2021; v1 submitted 15 September, 2021;
originally announced September 2021.
-
What do all these Buttons do? Statically Mining Android User Interfaces at Scale
Authors:
Konstantin Kuznetsov,
Chen Fu,
Song Gao,
David N. Jansen,
Lijun Zhang,
Andreas Zeller
Abstract:
We introduce FRONTMATTER: a tool to automatically mine both user interface models and behavior of Android apps at a large scale with high precision. Given an app, FRONTMATTER statically extracts all declared screens, the user interface elements, their textual and graphical features, as well as Android APIs invoked by interacting with them. Executed on tens of thousands of real-world apps, FRONTMAT…
▽ More
We introduce FRONTMATTER: a tool to automatically mine both user interface models and behavior of Android apps at a large scale with high precision. Given an app, FRONTMATTER statically extracts all declared screens, the user interface elements, their textual and graphical features, as well as Android APIs invoked by interacting with them. Executed on tens of thousands of real-world apps, FRONTMATTER opens the door for comprehensive mining of mobile user interfaces, jumpstarting empirical research at a large scale, addressing questions such as "How many travel apps require registration?", "Which apps do not follow accessibility guidelines?", "Does the user interface correspond to the description?", and many more. FRONTMATTER and the mined dataset are available under an open-source license.
△ Less
Submitted 7 May, 2021;
originally announced May 2021.
-
Eigenstate thermalization hypothesis through the lens of autocorrelation functions
Authors:
C. Schönle,
D. Jansen,
F. Heidrich-Meisner,
L. Vidmar
Abstract:
Matrix elements of observables in eigenstates of generic Hamiltonians are described by the Srednicki ansatz within the eigenstate thermalization hypothesis (ETH). We study a quantum chaotic spin-fermion model in a one-dimensional lattice, which consists of a spin-1/2 XX chain coupled to a single itinerant fermion. In our study, we focus on translationally invariant observables including the charge…
▽ More
Matrix elements of observables in eigenstates of generic Hamiltonians are described by the Srednicki ansatz within the eigenstate thermalization hypothesis (ETH). We study a quantum chaotic spin-fermion model in a one-dimensional lattice, which consists of a spin-1/2 XX chain coupled to a single itinerant fermion. In our study, we focus on translationally invariant observables including the charge and energy current, thereby also connecting the ETH with transport properties. Considering observables with a Hilbert-Schmidt norm of one, we first perform a comprehensive analysis of ETH in the model taking into account latest developments. A particular emphasis is on the analysis of the structure of the offdiagonal matrix elements $|\langle α| \hat O | β\rangle|^2$ in the limit of small eigenstate energy differences $ω= E_β- E_α$. Removing the dominant exponential suppression of $|\langle α| \hat O | β\rangle|^2$, we find that: (i) the current matrix elements exhibit a system-size dependence that is different from other observables under investigation, (ii) matrix elements of several other observables exhibit a Drude-like structure with a Lorentzian frequency dependence. We then show how this information can be extracted from the autocorrelation functions as well. Finally, our study is complemented by a numerical analysis of the fluctuation-dissipation relation for eigenstates in the bulk of the spectrum. We identify the regime of $ω$ in which the well-known fluctuation-dissipation relation is valid with high accuracy for finite systems.
△ Less
Submitted 25 September, 2021; v1 submitted 27 November, 2020;
originally announced November 2020.
-
Finite-temperature density-matrix renormalization group method for electron-phonon systems: Thermodynamics and Holstein-polaron spectral functions
Authors:
David Jansen,
Janez Bonča,
Fabian Heidrich-Meisner
Abstract:
We investigate the thermodynamics and finite-temperature spectral functions of the Holstein polaron using a density-matrix renormalization group method. Our method combines purification and local basis optimization (LBO) as an efficient treatment of phonon modes. LBO is a scheme which relies on finding the optimal local basis by diagonalizing the local reduced density matrix. By transforming the s…
▽ More
We investigate the thermodynamics and finite-temperature spectral functions of the Holstein polaron using a density-matrix renormalization group method. Our method combines purification and local basis optimization (LBO) as an efficient treatment of phonon modes. LBO is a scheme which relies on finding the optimal local basis by diagonalizing the local reduced density matrix. By transforming the state into this basis, one can truncate the local Hilbert space with a negligible loss of accuracy for a wide range of parameters. In this work, we focus on the crossover regime between large and small polarons of the Holstein model. Here, no analytical solution exists and we show that the thermal expectation values at low temperatures are independent of the phonon Hilbert space truncation provided the basis is chosen large enough. We then demonstrate that we can extract the electron spectral function and establish consistency with results from a finite-temperature Lanczos method. We additionally calculate the electron emission spectrum and the phonon spectral function and show that all the computations are significantly simplified by the local basis optimization. We observe that the electron emission spectrum shifts spectral weight to both lower frequencies and larger momenta as the temperature is increased. The phonon spectral function experiences a large broadening and the polaron peak at large momenta gets significantly flattened and merges almost completely into the free-phonon peak.
△ Less
Submitted 10 November, 2020; v1 submitted 22 July, 2020;
originally announced July 2020.
-
A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems
Authors:
David N. Jansen,
Jan Friso Groote,
Jeroen J. A. Keiren,
Anton Wijs
Abstract:
Branching bisimilarity is a behavioural equivalence relation on labelled transition systems that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than all algorithms for other weak behavioural equivalences, especially weak bisimilarity. With $m$ the number of transitions and $n$ the number of states, the classic…
▽ More
Branching bisimilarity is a behavioural equivalence relation on labelled transition systems that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than all algorithms for other weak behavioural equivalences, especially weak bisimilarity. With $m$ the number of transitions and $n$ the number of states, the classic $O(m n)$ algorithm was recently replaced by an $O(m (\log \lvert \mathit{Act}\rvert + \log n))$ algorithm, which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari. This results in a simpler algorithm with complexity $O(m \log n)$. Benchmarks show that this new algorithm is also faster and often far more memory efficient than its predecessors. This makes it the best option for branching bisimulation minimisation and preprocessing for weak bisimulation of LTSs.
△ Less
Submitted 6 November, 2019; v1 submitted 24 September, 2019;
originally announced September 2019.
-
Eigenstate thermalization and quantum chaos in the Holstein polaron model
Authors:
David Jansen,
Jan Stolpp,
Lev Vidmar,
Fabian Heidrich-Meisner
Abstract:
The eigenstate thermalization hypothesis (ETH) is a successful theory that provides sufficient criteria for ergodicity in quantum many-body systems. Most studies were carried out for Hamiltonians relevant for ultracold quantum gases and single-component systems of spins, fermions, or bosons. The paradigmatic example for thermalization in solid-state physics are phonons serving as a bath for electr…
▽ More
The eigenstate thermalization hypothesis (ETH) is a successful theory that provides sufficient criteria for ergodicity in quantum many-body systems. Most studies were carried out for Hamiltonians relevant for ultracold quantum gases and single-component systems of spins, fermions, or bosons. The paradigmatic example for thermalization in solid-state physics are phonons serving as a bath for electrons. This situation is often viewed from an open-quantum system perspective. Here, we ask whether a minimal microscopic model for electron-phonon coupling is quantum chaotic and whether it obeys ETH, if viewed as a closed quantum system. Using exact diagonalization, we address this question in the framework of the Holstein polaron model. Even though the model describes only a single itinerant electron, whose coupling to dispersionless phonons is the only integrability-breaking term, we find that the spectral statistics and the structure of Hamiltonian eigenstates exhibit essential properties of the corresponding random-matrix ensemble. Moreover, we verify the ETH ansatz both for diagonal and offdiagonal matrix elements of typical phonon and electron observables, and show that the ratio of their variances equals the value predicted from random-matrix theory.
△ Less
Submitted 26 April, 2019; v1 submitted 8 February, 2019;
originally announced February 2019.
-
Finding polynomial loop invariants for probabilistic programs
Authors:
Yijun Feng,
Lijun Zhang,
David N. Jansen,
Naijun Zhan,
Bican Xia
Abstract:
Quantitative loop invariants are an essential element in the verification of probabilistic programs. Recently, multivariate Lagrange interpolation has been applied to synthesizing polynomial invariants. In this paper, we propose an alternative approach. First, we fix a polynomial template as a candidate of a loop invariant. Using Stengle's Positivstellensatz and a transformation to a sum-of-square…
▽ More
Quantitative loop invariants are an essential element in the verification of probabilistic programs. Recently, multivariate Lagrange interpolation has been applied to synthesizing polynomial invariants. In this paper, we propose an alternative approach. First, we fix a polynomial template as a candidate of a loop invariant. Using Stengle's Positivstellensatz and a transformation to a sum-of-squares problem, we find sufficient conditions on the coefficients. Then, we solve a semidefinite programming feasibility problem to synthesize the loop invariants. If the semidefinite program is unfeasible, we backtrack after increasing the degree of the template. Our approach is semi-complete in the sense that it will always lead us to a feasible solution if one exists and numerical errors are small. Experimental results show the efficiency of our approach.
△ Less
Submitted 10 July, 2017;
originally announced July 2017.
-
Distribution-based bisimulation for labelled Markov processes
Authors:
Pengfei Yang,
David N. Jansen,
Lijun Zhang
Abstract:
In this paper we propose a (sub)distribution-based bisimulation for labelled Markov processes and compare it with earlier definitions of state and event bisimulation, which both only compare states. In contrast to those state-based bisimulations, our distribution bisimulation is weaker, but corresponds more closely to linear properties. We construct a logic and a metric to describe our distributio…
▽ More
In this paper we propose a (sub)distribution-based bisimulation for labelled Markov processes and compare it with earlier definitions of state and event bisimulation, which both only compare states. In contrast to those state-based bisimulations, our distribution bisimulation is weaker, but corresponds more closely to linear properties. We construct a logic and a metric to describe our distribution bisimulation and discuss linearity, continuity and compositional properties.
△ Less
Submitted 30 June, 2017;
originally announced June 2017.
-
Über die Präzision interprozeduraler Analysen
Authors:
Dorothea Jansen
Abstract:
In this work, we examine two approaches to interprocedural data-flow analysis of Sharir and Pnueli in terms of precision: the functional and the call-string approach. In doing so, not only the theoretical best, but all solutions are regarded which occur when using abstract interpretation or widening additionally. It turns out that the solutions of both approaches coincide. This property is preserv…
▽ More
In this work, we examine two approaches to interprocedural data-flow analysis of Sharir and Pnueli in terms of precision: the functional and the call-string approach. In doing so, not only the theoretical best, but all solutions are regarded which occur when using abstract interpretation or widening additionally. It turns out that the solutions of both approaches coincide. This property is preserved when using abstract interpretation; in the case of widening, a comparison of the results is not always possible.
△ Less
Submitted 29 March, 2017;
originally announced March 2017.
-
Notes on Pointed Gromov-Hausdorff Convergence
Authors:
Dorothea Jansen
Abstract:
The present article addresses to everyone who starts working with (pointed) Gromov-Hausdorff convergence. In the major part, both Gromov-Hausdorff convergence of compact and of pointed metric spaces are introduced and investigated. Moreover, the relation of sublimits occurring with pointed Gromov-Hausdorff convergence and ultralimits is discussed.
The present article addresses to everyone who starts working with (pointed) Gromov-Hausdorff convergence. In the major part, both Gromov-Hausdorff convergence of compact and of pointed metric spaces are introduced and investigated. Moreover, the relation of sublimits occurring with pointed Gromov-Hausdorff convergence and ultralimits is discussed.
△ Less
Submitted 28 March, 2017;
originally announced March 2017.
-
Existence of Typical Scales for Manifolds with Lower Ricci Curvature Bound
Authors:
Dorothea Jansen
Abstract:
For collapsing sequences of Riemannian manifolds which satisfy a uniform lower Ricci curvature bound it is shown that there is a sequence of scales such that for a set of good base points of large measure the pointed rescaled manifolds subconverge to a product of a Euclidean and a compact space. All Euclidean factors have the same dimension, all possible compact factors satisfy the same diameter b…
▽ More
For collapsing sequences of Riemannian manifolds which satisfy a uniform lower Ricci curvature bound it is shown that there is a sequence of scales such that for a set of good base points of large measure the pointed rescaled manifolds subconverge to a product of a Euclidean and a compact space. All Euclidean factors have the same dimension, all possible compact factors satisfy the same diameter bounds and their dimension does not depend on the choice of the base point (along a fixed subsequence).
△ Less
Submitted 28 March, 2017;
originally announced March 2017.
-
Stuttering equivalence is too slow!
Authors:
David N. Jansen,
Jeroen J. A. Keiren
Abstract:
Groote and Wijs recently described an algorithm for deciding stuttering equivalence and branching bisimulation equivalence, acclaimed to run in $\mathcal{O}(m \log n)$ time. Unfortunately, the algorithm does not always meet the acclaimed running time. In this paper, we present two counterexamples where the algorithms uses $Ω(md)$ time. A third example shows that the correction is not trivial. In o…
▽ More
Groote and Wijs recently described an algorithm for deciding stuttering equivalence and branching bisimulation equivalence, acclaimed to run in $\mathcal{O}(m \log n)$ time. Unfortunately, the algorithm does not always meet the acclaimed running time. In this paper, we present two counterexamples where the algorithms uses $Ω(md)$ time. A third example shows that the correction is not trivial. In order to analyse the problem we present pseudocode of the algorithm, and indicate the time that can be spent on each part of the algorithm in order to meet the desired bound. We also propose fixes to the algorithm such that it indeed runs in $\mathcal{O}(m \log n)$ time.
△ Less
Submitted 22 September, 2016; v1 submitted 18 March, 2016;
originally announced March 2016.
-
Efficient CSL Model Checking Using Stratification
Authors:
Lijun Zhang,
David N. Jansen,
Flemming Nielson,
Holger Hermanns
Abstract:
For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996. Their proof can be turned into an approximation algorithm with worse than exponential complexity. In 2000, Baier, Haverkort, Hermanns and Katoen presented an efficient polynomial-time approx…
▽ More
For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996. Their proof can be turned into an approximation algorithm with worse than exponential complexity. In 2000, Baier, Haverkort, Hermanns and Katoen presented an efficient polynomial-time approximation algorithm for the sublogic in which only binary until is allowed. In this paper, we propose such an efficient polynomial-time approximation algorithm for full CSL. The key to our method is the notion of stratified CTMCs with respect to the CSL property to be checked. On a stratified CTMC, the probability to satisfy a CSL path formula can be approximated by a transient analysis in polynomial time (using uniformization). We present a measure-preserving, linear-time and -space transformation of any CTMC into an equivalent, stratified one. This makes the present work the centerpiece of a broadly applicable full CSL model checker. Recently, the decision algorithm by Aziz et al. was shown to work only for stratified CTMCs. As an additional contribution, our measure-preserving transformation can be used to ensure the decidability for general CTMCs.
△ Less
Submitted 27 June, 2012; v1 submitted 26 April, 2011;
originally announced April 2011.
-
Erratum to: Model-checking continuous-time Markov chains by Aziz et al
Authors:
David N. Jansen
Abstract:
This note corrects a discrepancy between the semantics and the algorithm of the multiple until operator of CSL, like in Pr_{> 0.0025} (a until[1,2] b until[3,4] c), of the article: Model-checking continuous-time Markov chains by Aziz, Sanwal, Singhal and Brayton, TOCL 1(1), July 2000, pp. 162-170.
This note corrects a discrepancy between the semantics and the algorithm of the multiple until operator of CSL, like in Pr_{> 0.0025} (a until[1,2] b until[3,4] c), of the article: Model-checking continuous-time Markov chains by Aziz, Sanwal, Singhal and Brayton, TOCL 1(1), July 2000, pp. 162-170.
△ Less
Submitted 10 February, 2011;
originally announced February 2011.
-
Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations
Authors:
Lijun Zhang,
Holger Hermanns,
Friedrich Eisenbrand,
David N. Jansen
Abstract:
Strong and weak simulation relations have been proposed for Markov chains, while strong simulation and strong probabilistic simulation relations have been proposed for probabilistic automata. However, decision algorithms for strong and weak simulation over Markov chains, and for strong simulation over probabilistic automata are not efficient, which makes it as yet unclear whether they can be use…
▽ More
Strong and weak simulation relations have been proposed for Markov chains, while strong simulation and strong probabilistic simulation relations have been proposed for probabilistic automata. However, decision algorithms for strong and weak simulation over Markov chains, and for strong simulation over probabilistic automata are not efficient, which makes it as yet unclear whether they can be used as effectively as their non-probabilistic counterparts. This paper presents drastically improved algorithms to decide whether some (discrete- or continuous-time) Markov chain strongly or weakly simulates another, or whether a probabilistic automaton strongly simulates another. The key innovation is the use of parametric maximum flow techniques to amortize computations. We also present a novel algorithm for deciding strong probabilistic simulation preorders on probabilistic automata, which has polynomial complexity via a reduction to an LP problem. When extending the algorithms for probabilistic automata to their continuous-time counterpart, we retain the same complexity for both strong and strong probabilistic simulations.
△ Less
Submitted 18 November, 2008; v1 submitted 27 August, 2008;
originally announced August 2008.
-
A computer program for fast non-LTE analysis of interstellar line spectra
Authors:
Floris van der Tak,
John Black,
Fredrik Schoeier,
David Jansen,
Ewine van Dishoeck
Abstract:
The large quantity and high quality of modern radio and infrared line observations require efficient modeling techniques to infer physical and chemical parameters such as temperature, density, and molecular abundances. We present a computer program to calculate the intensities of atomic and molecular lines produced in a uniform medium, based on statistical equilibrium calculations involving coll…
▽ More
The large quantity and high quality of modern radio and infrared line observations require efficient modeling techniques to infer physical and chemical parameters such as temperature, density, and molecular abundances. We present a computer program to calculate the intensities of atomic and molecular lines produced in a uniform medium, based on statistical equilibrium calculations involving collisional and radiative processes and including radiation from background sources. Optical depth effects are treated with an escape probability method. The program is available on the World Wide Web at http://www.sron.rug.nl/~vdtak/radex/index.shtml . The program makes use of molecular data files maintained in the Leiden Atomic and Molecular Database (LAMDA), which will continue to be improved and expanded. The performance of the program is compared with more approximate and with more sophisticated methods. An Appendix provides diagnostic plots to estimate physical parameters from line intensity ratios of commonly observed molecules. This program should form an important tool in analyzing observations from current and future radio and infrared telescopes.
△ Less
Submitted 2 April, 2007;
originally announced April 2007.
-
Search for flavor-changing neutral currents and lepton-family-number violation in two-body D0 decays
Authors:
D. Pripstein,
C. N. Brown,
T. A. Carey,
Y. C. Chen,
R. L. Childers,
W. E. Cooper,
C. W. Darden,
G. Gidal,
K. N. Gounder,
P. M. Ho,
L. D. Isenhower,
D. M. Jansen,
R. G. Jeppesen,
D. M. Kaplan,
J. S. Kapustinsky,
G. C. Kiang,
M. S. Kowitt,
D. W. Lane,
L. M. Lederman,
M. J. Leitch,
J. W. Lillberg,
W. R. Luebke,
K. B. Luk,
P. L. McGaughey,
C. S. Mishra
, et al. (10 additional authors not shown)
Abstract:
Results of a search for the three neutral charm decays, D0 -> mu e, D0 -> mu mu, and D0 -> e e, are presented. This study was based on data collected in Experiment 789 at the Fermi National Accelerator Laboratory using 800 GeV/c proton-Au and proton-Be interactions. No evidence is found for any of the decays. Upper limits on the branching ratios, at the 90% confidence level, are obtained.
Results of a search for the three neutral charm decays, D0 -> mu e, D0 -> mu mu, and D0 -> e e, are presented. This study was based on data collected in Experiment 789 at the Fermi National Accelerator Laboratory using 800 GeV/c proton-Au and proton-Be interactions. No evidence is found for any of the decays. Upper limits on the branching ratios, at the 90% confidence level, are obtained.
△ Less
Submitted 5 October, 1999; v1 submitted 11 June, 1999;
originally announced June 1999.
-
Diffractive Interactions at DIS99: Experimental Summary
Authors:
D. M. Jansen,
M. Albrow,
R. Brugnera
Abstract:
Experimental results on diffraction, which were presented at the 7th International Workshop on Deep Inelastic Scattering and QCD (DIS99), are summarized.
Experimental results on diffraction, which were presented at the 7th International Workshop on Deep Inelastic Scattering and QCD (DIS99), are summarized.
△ Less
Submitted 28 May, 1999;
originally announced May 1999.
-
Far-Infrared and Sub-Millimeter Observations and Physical Models of the Reflection Nebula Ced 201
Authors:
Ciska Kemper,
Marco Spaans,
David J. Jansen,
Michiel R. Hogerheijde,
Ewine F. van Dishoeck,
Xander G. G. M. Tielens
Abstract:
ISO [C II] 158 micron, [O I] 63 micron, and H_2 9 and 17 micron observations are presented of the reflection nebula Ced 201, which is a photon-dominated region illuminated by a B9.5 star with a color temperature of 10,000 K (a cool PDR). In combination with ground based [C I] 609 micron, CO, 13CO, CS and HCO+ data, the carbon budget and physical structure of the reflection nebula are constrained…
▽ More
ISO [C II] 158 micron, [O I] 63 micron, and H_2 9 and 17 micron observations are presented of the reflection nebula Ced 201, which is a photon-dominated region illuminated by a B9.5 star with a color temperature of 10,000 K (a cool PDR). In combination with ground based [C I] 609 micron, CO, 13CO, CS and HCO+ data, the carbon budget and physical structure of the reflection nebula are constrained. The obtained data set is the first one to contain all important cooling lines of a cool PDR, and allows a comparison to be made with classical PDRs. To this effect one- and three-dimensional PDR models are presented which incorporate the physical characteristics of the source, and are aimed at understanding the dominant heating processes of the cloud. The contribution of very small grains to the photo-electric heating rate is estimated from these models and used to constrain the total abundance of PAHs and small grains. Observations of the pure rotational H_2 lines with ISO, in particular the S(3) line, indicate the presence of a small amount of very warm, approximately 330 K, molecular gas. This gas cannot be accommodated by the presented models.
△ Less
Submitted 16 November, 1998;
originally announced November 1998.
-
Structure Function Subgroup Summary
Authors:
D. Harris,
F. I. Olness,
S. Ritz,
M. Albrow,
E. Berger,
T. Bolton,
A. Caldwell,
A. El-Khadra,
B. Ermolaev,
J. W. Gary,
E. Hughes,
J. Huston,
D. Jansen,
Y. -K. Kim,
D. Krakauer,
S. Kuhlmann,
H. Lai,
D. Naples,
J. Qiu,
D. Reeder,
M. H. Reno,
R. J. Scalise,
B. Schumm,
P. Spentzouris,
C. Taylor
, et al. (8 additional authors not shown)
Abstract:
We summarize the studies and discussions of the Structure Function subgroup of the QCD working group of the Snowmass 1996 Workshop: New Directions for High Energy Physics.
We summarize the studies and discussions of the Structure Function subgroup of the QCD working group of the Snowmass 1996 Workshop: New Directions for High Energy Physics.
△ Less
Submitted 22 December, 1997; v1 submitted 23 June, 1997;
originally announced June 1997.
-
Probing u-bar/d-bar Asymmetry in the Proton via Quarkonium Production
Authors:
J. C. Peng,
D. M. Jansen,
Y. C. Chen
Abstract:
The sensitivity of proton-induced $J/ψ$ and $Υ$ production to the possible $\bar u/\bar d$ asymmetry in the nucleon is studied. The ratio of the quarkonium production cross sections at large $x_F$ on hydrogen over deuterium targets, $σ(p+p) / σ(p+d)$, is shown to be sensitive to this asymmetry. Predictions of various theoretical models for this ratio are presented.
The sensitivity of proton-induced $J/ψ$ and $Υ$ production to the possible $\bar u/\bar d$ asymmetry in the nucleon is studied. The ratio of the quarkonium production cross sections at large $x_F$ on hydrogen over deuterium targets, $σ(p+p) / σ(p+d)$, is shown to be sensitive to this asymmetry. Predictions of various theoretical models for this ratio are presented.
△ Less
Submitted 6 August, 1995; v1 submitted 5 August, 1995;
originally announced August 1995.
-
Probing u-bar/d-bar Asymmetry in the Proton via W and Z Production
Authors:
J. C. Peng,
D. M. Jansen
Abstract:
The sensitivity of $W$ and $Z$ production at RHIC to the possible $\bar u/\bar d$ asymmetry in the proton is studied. The ratios of the $W^+$ over $W^-$ production cross sections in $p + p$ collision, as well as the ratios of the $W^+$ and $Z$ production cross sections for $p + p$ over $p + d$ collisions, are shown to be sensitive to this asymmetry. Predictions of various theoretical models for…
▽ More
The sensitivity of $W$ and $Z$ production at RHIC to the possible $\bar u/\bar d$ asymmetry in the proton is studied. The ratios of the $W^+$ over $W^-$ production cross sections in $p + p$ collision, as well as the ratios of the $W^+$ and $Z$ production cross sections for $p + p$ over $p + d$ collisions, are shown to be sensitive to this asymmetry. Predictions of various theoretical models for these ratios are presented.
△ Less
Submitted 6 August, 1995; v1 submitted 5 August, 1995;
originally announced August 1995.
