Showing 1–18 of 18 results for author: Krstić, S

Towards an Enforceable GDPR Specification

Authors: François Hublet, Alexander Kvamme, Srđan Krstić

Abstract: While Privacy by Design (PbD) is prescribed by modern privacy regulations such as the EU's GDPR, achieving PbD in real software systems is a notoriously difficult task. One emerging technique to realize PbD is Runtime enforcement (RE), in which an enforcer, loaded with a specification of a system's privacy requirements, observes the actions performed by the system and instructs it to perform actio… ▽ More While Privacy by Design (PbD) is prescribed by modern privacy regulations such as the EU's GDPR, achieving PbD in real software systems is a notoriously difficult task. One emerging technique to realize PbD is Runtime enforcement (RE), in which an enforcer, loaded with a specification of a system's privacy requirements, observes the actions performed by the system and instructs it to perform actions that will ensure compliance with these requirements at all times. To be able to use RE techniques for PbD, privacy regulations first need to be translated into an enforceable specification. In this paper, we report on our ongoing work in formalizing the GDPR. We first present a set of requirements and an iterative methodology for creating enforceable formal specifications of legal provisions. Then, we report on a preliminary case study in which we used our methodology to derive an enforceable specification of part of the GDPR. Our case study suggests that our methodology can be effectively used to develop accurate enforceable specifications. △ Less

Submitted 27 February, 2024; originally announced February 2024.

Efficient Evaluation of Arbitrary Relational Calculus Queries

Authors: Martin Raszyk, David Basin, Srđan Krstić, Dmitriy Traytel

Abstract: The relational calculus (RC) is a concise, declarative query language. However, existing RC query evaluation approaches are inefficient and often deviate from established algorithms based on finite tables used in database management systems. We devise a new translation of an arbitrary RC query into two safe-range queries, for which the finiteness of the query's evaluation result is guaranteed. Ass… ▽ More The relational calculus (RC) is a concise, declarative query language. However, existing RC query evaluation approaches are inefficient and often deviate from established algorithms based on finite tables used in database management systems. We devise a new translation of an arbitrary RC query into two safe-range queries, for which the finiteness of the query's evaluation result is guaranteed. Assuming an infinite domain, the two queries have the following meaning: The first is closed and characterizes the original query's relative safety, i.e., whether given a fixed database, the original query evaluates to a finite relation. The second safe-range query is equivalent to the original query, if the latter is relatively safe. We compose our translation with other, more standard ones to ultimately obtain two SQL queries. This allows us to use standard database management systems to evaluate arbitrary RC queries. We show that our translation improves the time complexity over existing approaches, which we also empirically confirm in both realistic and synthetic experiments. △ Less

Submitted 20 December, 2023; v1 submitted 18 October, 2022; originally announced October 2022.

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 4 (December 22, 2023) lmcs:10182

Collisional S-Matrix for the Vibrational Dynamics of H+H2 by Quantum Computing

Authors: Yulun Wang, Predrag S. Krstic

Abstract: An algorithm and a system of quantum circuits is developed and applied to compute accurately the S matrix for the transitions between vibrational states of H2 for collisions with H. The algorithm was applied to 100 eV laboratory collision energy at a quantum circuit simulator. The effects of the discretized dissociative continuum to the transition cross sections are carefully studied and accuracy… ▽ More An algorithm and a system of quantum circuits is developed and applied to compute accurately the S matrix for the transitions between vibrational states of H2 for collisions with H. The algorithm was applied to 100 eV laboratory collision energy at a quantum circuit simulator. The effects of the discretized dissociative continuum to the transition cross sections are carefully studied and accuracy and convergence of the results with the chosen parameters of the algorithm and the collision system are verified by comparison with a solution of the time-dependent Schrodinger equation using the classical algorithm as well as comparison with a few results from the literature. △ Less

Submitted 3 January, 2023; v1 submitted 27 May, 2022; originally announced May 2022.

Comments: 21 pages, 12 figrues

Multistate Transition Dynamics by Strong Time-Dependent Perturbation in NISQ era

Authors: Yulun Wang, Predrag S. Krstic

Abstract: We develop a quantum computing scheme utilizing McLachlan variational principle in a hybrid quantum-classical algorithm to accurately calculate the transition dynamics of a closed quantum system with many excited states subject to a strong time-dependent perturbation. A systematic approach for optimal construction of a general N-state ansatz with unary N-qubit encoding is refined. We also utilize… ▽ More We develop a quantum computing scheme utilizing McLachlan variational principle in a hybrid quantum-classical algorithm to accurately calculate the transition dynamics of a closed quantum system with many excited states subject to a strong time-dependent perturbation. A systematic approach for optimal construction of a general N-state ansatz with unary N-qubit encoding is refined. We also utilize qubit efficient encoding in McLachlan variational quantum algorithm to reduce the number of qubits to log2 N, simultaneously diminishing depths of the quantum circuits. The significant reduction of the number of time steps is achieved by use of the second order marching method. Instrumental in obtaining high accuracy are adaptations of the circuits to include time-dependent global phase correction. We illustrated, tested and optimized our quantum computing algorithm on a set of 16 bound hydrogenic eigenstates exposed to a strong laser attosecond pulse. Results for transition probabilities are obtained with accuracy better than 1%, as established by comparison to the benchmark data. Use of interaction representation of the Hamiltonian reduces the effect of both NISQ noise and sampling errors accumulation while the quantum system evolves in time. △ Less

Submitted 24 April, 2022; v1 submitted 12 December, 2021; originally announced December 2021.

Comments: 17 pages, 12 figures

Prospect of using Grover's search in the noisy-intermediate-scale quantum-computer era

Authors: Yulun Wang, Predrag S. Krstic

Abstract: In order to understand the bounds of utilization of the Grover's search algorithm for the large unstructured data in presence of the quantum computer noise, we undertake a series of simulations by inflicting various types of noise, modelled by the IBM QISKit. We apply three forms of Grover's algorithms: (1) the standard one, with 4-10 qubits, (2) recently published modified Grover's algorithm, set… ▽ More In order to understand the bounds of utilization of the Grover's search algorithm for the large unstructured data in presence of the quantum computer noise, we undertake a series of simulations by inflicting various types of noise, modelled by the IBM QISKit. We apply three forms of Grover's algorithms: (1) the standard one, with 4-10 qubits, (2) recently published modified Grover's algorithm, set to reduce the circuit depth, and (3) the algorithms in (1) and (2) with multi-control Toffoli's modified by addition of an ancilla qubit. Based on these simulations, we find the upper bound of noise for these cases, establish its dependence on the quantum depth of the circuit and provide comparison among them. By extrapolation of the fitted thresholds, we predict what would be the typical gate error bounds when apply the Grover's algorithms for the search of a data in a data set as large as thirty two thousands. △ Less

Submitted 18 September, 2020; v1 submitted 17 June, 2020; originally announced June 2020.

Journal ref: Phys. Rev. A 102, 042609 (2020)

Formation of C$_{18}$H and C$_{18}$H$_2$ molecules by low energy irradiation with atomic and molecular hydrogen

Authors: F. J. Domínguez-Gutiérrez, C. Martínez-Flores, P. S. Krstic, R. Cabrera-Trujillo, U. von Toussaint

Abstract: We study the formation of C$_{18}$H and C$_{18}$H$_2$ by irradiating a cyclo[$18$]carbon molecule with atomic and molecular hydrogen at impact energy, $E$, in the range of 0.5-25 eV. We utilize the density-functional tight-binding method to perform molecular dynamics simulations to emulate the interaction of a carbon ring when colliding with atomic or molecular hydrogen. From our results, the form… ▽ More We study the formation of C$_{18}$H and C$_{18}$H$_2$ by irradiating a cyclo[$18$]carbon molecule with atomic and molecular hydrogen at impact energy, $E$, in the range of 0.5-25 eV. We utilize the density-functional tight-binding method to perform molecular dynamics simulations to emulate the interaction of a carbon ring when colliding with atomic or molecular hydrogen. From our results, the formation of the C$_{18}$H molecules is likely to occur upon irradiating by H atoms at $E < 10$ eV and by H$_2$ molecules at $2 < E < 15$ eV center of mass energy. Formation of C$_{18}$H$_2$ molecules is only observed at around $E = 2$ eV. Our results show that the absorption of hydrogen is more prone in atomic than in molecular hydrogen atmosphere. Thus, we find that the probability of physio-absorption reaches up to 80 \% for atomic projectiles with $E < 5$ eV but only up to 10 \% for the molecular ones. Our analysis shows that the deformation of the carbon ring due to the hydrogen bonding produces transition from $sp$ to $sp^2$ hybridization. The angle between the carbon atoms at the locations near to the H bond in the resulting ring is not 120$^o$ but instead 110$^o$ degrees. No molecular fragmentation of the C$_{18}$ ring is observed. △ Less

Submitted 7 April, 2020; originally announced April 2020.

COST Action IC 1402 ArVI: Runtime Verification Beyond Monitoring -- Activity Report of Working Group 1

Authors: Wolfgang Ahrendt, Cyrille Artho, Christian Colombo, Yliès Falcone, Srdan Krstic, Martin Leucker, Florian Lorber, Joao Lourenço, Leonardo Mariani, César Sánchez, Gerardo Schneider, Volker Stolz

Abstract: This report presents the activities of the first working group of the COST Action ArVI, Runtime Verification beyond Monitoring. The report aims to provide an overview of some of the major core aspects involved in Runtime Verification. Runtime Verification is the field of research dedicated to the analysis of system executions. It is often seen as a discipline that studies how a system run satisfie… ▽ More This report presents the activities of the first working group of the COST Action ArVI, Runtime Verification beyond Monitoring. The report aims to provide an overview of some of the major core aspects involved in Runtime Verification. Runtime Verification is the field of research dedicated to the analysis of system executions. It is often seen as a discipline that studies how a system run satisfies or violates correctness properties. The report exposes a taxonomy of Runtime Verification (RV) presenting the terminology involved with the main concepts of the field. The report also develops the concept of instrumentation, the various ways to instrument systems, and the fundamental role of instrumentation in designing an RV framework. We also discuss how RV interplays with other verification techniques such as model-checking, deductive verification, model learning, testing, and runtime assertion checking. Finally, we propose challenges in monitoring quantitative and statistical data beyond detecting property violation. △ Less

Submitted 11 February, 2019; originally announced February 2019.

FAR-Cubicle - A new reachability algorithm for Cubicle

Authors: Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, Mattias Roux

Abstract: We present a fully automatic algorithm for verifying safety properties of parameterized software systems. This algorithm is based on both IC3 and Lazy Annotation. We implemented it in Cubicle, a model checker for verifying safety properties of array-based systems. Cache-coherence protocols and mutual exclusion algorithms are known examples of such systems. Our algorithm iteratively builds an abstr… ▽ More We present a fully automatic algorithm for verifying safety properties of parameterized software systems. This algorithm is based on both IC3 and Lazy Annotation. We implemented it in Cubicle, a model checker for verifying safety properties of array-based systems. Cache-coherence protocols and mutual exclusion algorithms are known examples of such systems. Our algorithm iteratively builds an abstract reachability graph refining the set of reachable states from counterexamples. Refining is made through counterexample approximation. We show the effectiveness and limitations of this algorithm and tradeoffs that results from it. △ Less

Submitted 20 November, 2018; originally announced November 2018.

Journal ref: 2017 Formal Methods in Computer-Aided Design (FMCAD), Oct 2017, Vienna, France. IEEE

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

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

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

Submitted 16 November, 2018; originally announced November 2018.

Efficient Large-scale Trace Checking Using MapReduce

Authors: Marcello M. Bersani, Domenico Bianculli, Carlo Ghezzi, Srdan Krstic, Pierluigi San Pietro

Abstract: The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic) do not scale with respect to two crucial dimensions: the length of the trace and the size of the time interval for which logged events must be buffered to check satisfaction of the specification.… ▽ More The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic) do not scale with respect to two crucial dimensions: the length of the trace and the size of the time interval for which logged events must be buffered to check satisfaction of the specification. The former issue can be addressed by distributed and parallel trace checking algorithms that can take advantage of modern cloud computing and programming frameworks like MapReduce. Still, the latter issue remains open with current state-of-the-art approaches. In this paper we address this memory scalability issue by proposing a new semantics for MTL, called lazy semantics. This semantics can evaluate temporal formulae and boolean combinations of temporal-only formulae at any arbitrary time instant. We prove that lazy semantics is more expressive than standard point-based semantics and that it can be used as a basis for a correct parametric decomposition of any MTL formula into an equivalent one with smaller, bounded time intervals. We use lazy semantics to extend our previous distributed trace checking algorithm for MTL. We evaluate the proposed algorithm in terms of memory scalability and time/memory tradeoffs. △ Less

Submitted 26 August, 2015; originally announced August 2015.

Comments: 13 pages, 8 figures

MSC Class: 68N30 ACM Class: D.2.4

InstaCluster: Building A Big Data Cluster in Minutes

Authors: Giovanni Paolo Gibilisco, Srdan Krstic

Abstract: Deploying, configuring, and managing large clusters is very a demanding and cumbersome task due to the complexity of such systems and the variety of skills needed. One needs to perform low-level configuration of the cluster nodes to ensure their interoperability and connectivity, as well as install, configure and provision the needed services. In this paper we address this problem and demonstrat… ▽ More Deploying, configuring, and managing large clusters is very a demanding and cumbersome task due to the complexity of such systems and the variety of skills needed. One needs to perform low-level configuration of the cluster nodes to ensure their interoperability and connectivity, as well as install, configure and provision the needed services. In this paper we address this problem and demonstrate how to build a Big Data analytic platform on Amazon EC2 in a matter of minutes. Moreover, to use our tool, embedded into a public Amazon Machine Image, the user does not need to be an expert in system administration or Big Data service configuration. Our tool dramatically reduces the time needed to provision clusters, as well as the cost of the infrastructure. Researchers enjoy an additional benefit of having a simple way to specify the experimental environments they use, so that their experiments can be easily reproduced by anyone using our tool. △ Less

Submitted 20 August, 2015; originally announced August 2015.

Comments: 5 pages, 1 figure

MSC Class: 68M14 ACM Class: D.2.7

Offline Trace Checking of Quantitative Properties of Service-Based Applications

Authors: Domenico Bianculli, Carlo Ghezzi, Srdan Krstic, Pierluigi San Pietro

Abstract: Service-based applications are often developed as compositions of partner services. A service integrator needs precise methods to specify the quality attributes expected by each partner service, as well as effective techniques to verify these attributes. In previous work, we identified the most common specification patterns related to provisioning service-based applications and developed an expres… ▽ More Service-based applications are often developed as compositions of partner services. A service integrator needs precise methods to specify the quality attributes expected by each partner service, as well as effective techniques to verify these attributes. In previous work, we identified the most common specification patterns related to provisioning service-based applications and developed an expressive specification language (SOLOIST) that supports them. SOLOIST is an extension of metric temporal logic with aggregate temporal modalities that can be used to write quantitative temporal properties. In this paper we address the problem of performing offline checking of service execution traces against quantitative requirements specifications written in SOLOIST. We present a translation of SOLOIST into CLTLB(D), a variant of linear temporal logic, and reduce the trace checking of SOLOIST to bounded satisfiability checking of CLTLB(D), which is supported by ZOT, an SMT-based verification toolkit. We detail the results of applying the proposed offline trace checking procedure to different types of traces, and compare its performance with previous work. △ Less

Submitted 16 September, 2014; originally announced September 2014.

Comments: 19 pages, 7 figures, Extended version of the SOCA 2014 paper

ACM Class: D.2.4

Trace checking of Metric Temporal Logic with Aggregating Modalities using MapReduce

Authors: Domenico Bianculli, Carlo Ghezzi, Srdan Krstic

Abstract: Modern complex software systems produce a large amount of execution data, often stored in logs. These logs can be analyzed using trace checking techniques to check whether the system complies with its requirements specifications. Often these specifications express quantitative properties of the system, which include timing constraints as well as higher-level constraints on the occurrences of signi… ▽ More Modern complex software systems produce a large amount of execution data, often stored in logs. These logs can be analyzed using trace checking techniques to check whether the system complies with its requirements specifications. Often these specifications express quantitative properties of the system, which include timing constraints as well as higher-level constraints on the occurrences of significant events, expressed using aggregate operators. In this paper we present an algorithm that exploits the MapReduce programming model to check specifications expressed in a metric temporal logic with aggregating modalities, over large execution traces. The algorithm exploits the structure of the formula to parallelize the evaluation, with a significant gain in time. We report on the assessment of the implementation - based on the Hadoop framework - of the proposed algorithm and comment on its scalability. △ Less

Submitted 13 June, 2014; originally announced June 2014.

Comments: 16 pages, 6 figures, Extended version of the SEFM 2014 paper

ACM Class: D.2.4

Coroutining Folds with Hyperfunctions

Authors: J. Launchbury, S. Krstic, T. E. Sauerwein

Abstract: Fold functions are a general mechanism for computing over recursive data structures. First-order folds compute results bottom-up. With higher-order folds, computations that inherit attributes from above can also be expressed. In this paper, we explore folds over a form of recursive higher-order function, called hyperfunctions, and show that hyperfunctions allow fold computations to coroutine acros… ▽ More Fold functions are a general mechanism for computing over recursive data structures. First-order folds compute results bottom-up. With higher-order folds, computations that inherit attributes from above can also be expressed. In this paper, we explore folds over a form of recursive higher-order function, called hyperfunctions, and show that hyperfunctions allow fold computations to coroutine across data structures, as well as compute bottom up and top down. We use the compiler technique of foldr-build as an exemplar to show how hyperfunctions can be used. △ Less

Submitted 19 September, 2013; originally announced September 2013.

Comments: In Proceedings Festschrift for Dave Schmidt, arXiv:1309.4557. It is a privilege to submit a paper for the Festschrift symposium held to honor Dave Schmidt's lifetime of contributions on the occasion of his 60th birthday. Many years ago, as a fresh PhD student, Dave's excellent book on Denotational Semantics opened my eyes to rich possibilities of building functions over functions (recursively!) and our continued interactions over the years were always insightful. So it seemed appropriate to offer a paper whose foundations rely on the same mathematical models that Dave so ably expounded all those years ago, constructing recursive function spaces in a way that is not possible in traditional set-theoretic models. -- John Launchbury, 2013

ACM Class: D.1.1

Journal ref: EPTCS 129, 2013, pp. 121-135

Collisions, magnetization, and transport coefficients in the lower solar atmosphere

Authors: J. Vranjes, P. S. Krstic

Abstract: The lower solar atmosphere is an intrinsically multi-component and collisional environment with electron and proton collision frequencies in the range $10^{8}-10^{10}$ Hz, which may be considerably higher than the gyro-frequencies for both species. We aim to provide a reliable quantitative set of data for collision frequencies, magnetization, viscosity, and thermal conductivity for the most import… ▽ More The lower solar atmosphere is an intrinsically multi-component and collisional environment with electron and proton collision frequencies in the range $10^{8}-10^{10}$ Hz, which may be considerably higher than the gyro-frequencies for both species. We aim to provide a reliable quantitative set of data for collision frequencies, magnetization, viscosity, and thermal conductivity for the most important species in the lower solar atmosphere. Having such data at hand is essential for any modeling that is aimed at describing realistic properties of the considered environment. We describe the altitude dependence of the parameters and the different physics of collisions between charged species, and between charged and neutrals species. Regions of dominance of each type of collisions are clearly identified. We determine the layers within which either electrons or ions or both are unmagnetized. Protons are shown to be un-magnetized in the lower atmosphere in a layer that is at least 1000 km thick even for a kilo-Gauss magnetic field that decreases exponentially with altitude. In these layers the dynamics of charged species cannot be affected by the magnetic field, and this fact is used in our modeling. Viscosity and thermal conductivity coefficients are calculated for layers where ions are unmagnetized. We compare viscosity and friction and determine the regions of dominance of each of the phenomena. We provide the most reliable quantitative values for most important parameters in the lower solar atmosphere to be used in analytical modeling and numerical simulations of various phenomena such as waves, transport and magnetization of particles, and the triggering mechanism of coronal mass ejections. △ Less

Submitted 15 April, 2013; originally announced April 2013.

Comments: To appear in Astron. Astrophys

Journal ref: Astron. Astrophys. 554, A22 (2013)

Ground interpolation for the theory of equality

Authors: Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstić, Cesare Tinelli

Abstract: Theory interpolation has found several successful applications in model checking. We present a novel method for computing interpolants for ground formulas in the theory of equality. The method produces interpolants from colored congruence graphs representing derivations in that theory. These graphs can be produced by conventional congruence closure algorithms in a straightforward manner. By worki… ▽ More Theory interpolation has found several successful applications in model checking. We present a novel method for computing interpolants for ground formulas in the theory of equality. The method produces interpolants from colored congruence graphs representing derivations in that theory. These graphs can be produced by conventional congruence closure algorithms in a straightforward manner. By working with graphs, rather than at the level of individual proof steps, we are able to derive interpolants that are pleasingly simple (conjunctions of Horn clauses) and smaller than those generated by other tools. Our interpolation method can be seen as a theory-specific implementation of a cooperative interpolation game between two provers. We present a generic version of the interpolation game, parametrized by the theory T, and define a general method to extract runs of the game from proofs in T and then generate interpolants from these runs. △ Less

Submitted 15 February, 2012; v1 submitted 23 November, 2011; originally announced November 2011.

ACM Class: D.2.4, F.3.1, F.4.1, I.2.3

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 1 (February 16, 2012) lmcs:709

Rate Coefficient for H^+ + H_2(X ^1Sigma_g^+, nu=0, J=0) --> H(1s) + H_2^+ Charge Transfer and Some Cosmological Implications

Authors: Daniel Wolf Savin, Predrag S. Krstic, Zoltan Haiman, Phillip C. Stancil

Abstract: Krstic has carried out the first quantum mechanical calculations near threshold for the charge transfer (CT) process H^+ + H_2(X ^1Sigma_g^+, nu=0, J=0) --> H(1s) + H_2^+. These results are relevant for models of primordial galaxy and first star formation that require reliable atomic and molecular data for obtaining the early universe hydrogen chemistry. Using the results of Krstic, we calculate… ▽ More Krstic has carried out the first quantum mechanical calculations near threshold for the charge transfer (CT) process H^+ + H_2(X ^1Sigma_g^+, nu=0, J=0) --> H(1s) + H_2^+. These results are relevant for models of primordial galaxy and first star formation that require reliable atomic and molecular data for obtaining the early universe hydrogen chemistry. Using the results of Krstic, we calculate the relevant CT rate coefficient for temperatures between 100 and 30,000 K. We also present a simple fit which can be readily implemented into early universe chemical models. Additionally, we explore how the range of previously published data for this reaction translates into uncertainties in the predicted gas temperature and H_2 relative abundance in a collapsing primordial gas cloud. Our new data significantly reduce these cosmological uncertainties that are due to the uncertainties in the previously published CT rate coefficients. △ Less

Submitted 14 April, 2004; originally announced April 2004.

Comments: This version corrects a typo in Eq. 4 of our ApJL. 11 pages, 2 figures

Ionization of hydrogen and hydrogenic ions by antiprotons

Authors: D. R. Schultz, P. S. Krstic, C. O. Reinhold, J. C. Wells

Abstract: Presented here is a description of the ionization of hydrogen and hydrogenic ions by antiproton-impact, based on very large scale numerical solutions of the time-dependent Schrödinger equation in three spatial dimensions and on analysis of the topology of the electronic eigenenergy surfaces in the plane of complex internuclear distance. Comparison is made with other theories and very recent meas… ▽ More Presented here is a description of the ionization of hydrogen and hydrogenic ions by antiproton-impact, based on very large scale numerical solutions of the time-dependent Schrödinger equation in three spatial dimensions and on analysis of the topology of the electronic eigenenergy surfaces in the plane of complex internuclear distance. Comparison is made with other theories and very recent measurements. △ Less

Submitted 4 March, 1996; originally announced March 1996.

Comments: RevTex document, 11 pages, 4 Postscript figures are available from the authors, in press Phys. Rev. Lett