Phys. Rev. A Phys. Rev. A Decoherence in a scalable adiabatic quantum computer Ashhab S Johansson J R Nori F 2006 74 We consider the effects of decoherence on Landau-Zener crossings encountered in a large-scale adiabatic-quantum-computing setup. We analyze the dependence of the success probability, i.e. the probability to end up in the new ground state, on the noise amplitude and correlation time. We determine the optimal sweep rate that is required to maximize the success probability. We then discuss the scaling of decoherence effects with increasing system size. We find that those effects can be important for large systems, even if they are small for each of the small building blocks. research-article

2007

Equation-of-motion treatment of hyperfine interaction in a quantum dot Deng C Hu X 2006 Isolated electron spins in semiconductor nanostructures are promising qubit candidates for a solid state quantum computer, There have seen truly impressive experimental progresses in the study of single spins in the past two years. In this paper we analytically solve the {\it Non-Markovian} single electron spin dynamics due to inhomogeneous hyperfine couplings with surrounding nuclei in a quantum dot. We use the equation-of-motion method assisted with a large field expansion in a full quantum mechanical treatment. We recover the exact solution for fully polarized nuclei. By considering virtual nuclear spin flip-flops mediated by the electron, which generate fluctuations in the Overhauser field (the nuclear field) for the electron spin, we find that the decay amplitude of the transverse electron spin correlation function for partially polarized nuclear spin configurations is of the order unity instead of $\text{O}(1/N)$ ($N$ being the number of nuclei in the dot) obtained in previous studies. We show that the complete amplitude decay can be understood with the spectrum broadening of the correlation function near the electron spin Rabi frequency induced by nuclear spin flip-flops. Our results show that a 90% nuclear polarization can enhance the electron spin $T_2$ time by more than one order of magnitude in some parameter regime. In the long time limit, the envelope of the transverse electron spin correlation function has a non-exponential $1/t^2$ decay in the presence of both polarized and unpolarized nuclei. PREPRINT

Nucl. Instrum. Methods Phys. Res., B Nucl. Instrum. Methods Phys. Res., B Computer simulation of coherent interaction of charged particles and photons with crystalline solids at high energies Apyan A 2007 255 269 275 Monte Carlo simulation code has been developed and tested for studying the passage of charged particle beams and radiation through the crystalline matter at the energies from tens of MeV up to hundreds of GeV. The developed Monte Carlo code simulates electron, positron and photon shower in single crystals and amorphous media. The Monte Carlo code tracks the all generations of charged particles and photons through the aligned crystal by taking into account the parameters of incoming beam, multiple scattering, energy loss, emission angles, transverse dimension of beams, and linear polarization of produced photons. The simulation results are compared with the CERN-NA-59 experimental data. The realistic descriptions of the electron and photon beams and the physical processes within the silicon and germanium single crystals have been implemented. research-article

Automated verification of weak equivalence within the SMODELS system Janhunen T Oikarinen E 2006 In answer set programming (ASP), a problem at hand is solved by (i) writing a logic program whose answer sets correspond to the solutions of the problem, and by (ii) computing the answer sets of the program using an answer set solver as a search engine. Typically, a programmer creates a series of gradually improving logic programs for a particular problem when optimizing program length and execution time on a particular solver. This leads the programmer to a meta-level problem of ensuring that the programs are equivalent, i.e., they give rise to the same answer sets. To ease answer set programming at methodological level, we propose a translation-based method for verifying the equivalence of logic programs. The basic idea is to translate logic programs P and Q under consideration into a single logic program EQT(P,Q) whose answer sets (if such exist) yield counter-examples to the equivalence of P and Q. The method is developed here in a slightly more general setting by taking the visibility of atoms properly into account when comparing answer sets. The translation-based approach presented in the paper has been implemented as a translator called lpeq that enables the verification of weak equivalence within the smodels system using the same search engine as for the search of models. Our experiments with lpeq and smodels suggest that establishing the equivalence of logic programs in this way is in certain cases much faster than naive cross-checking of answer sets. PREPRINT

Logic programs with monotone abstract constraint atoms Marek V W Niemela I Truszczynski] M 2006 We introduce and study logic programs whose clauses are built out of monotone constraint atoms. We show that the operational concept of the one-step provability operator generalizes to programs with monotone constraint atoms, but the generalization involves nondeterminism. Our main results demonstrate that our formalism is a common generalization of (1) normal logic programming with its semantics of models, supported models and stable models, (2) logic programming with weight atoms (lparse programs) with the semantics of stable models, as defined by Niemela, Simons and Soininen, and (3) of disjunctive logic programming with the possible-model semantics of Sakama and Inoue. PREPRINT

Intrinsic Universality in Real Computation Zenil H 2006 Models of computation operating over real numbers and computing a larger class of functions compared to the class of general recursive functions invariably introduce a non-finite amount of information encoded in an arbitrary non-computable real number or at least one non-recursive function. In this paper we prove that it is not possible in general to allow universality in the Turing sense in those models assuming the complete set of real numbers unless assuming both : non-Turing computable real numbers and non-recursive functions operating through all the arithmetical hierarchy. A model M does not allow universality unless M be bounded by a maximal degree of unsolvability, i.e. computing a finite set of complexity classes. We name this relative universality to its complexity M-universality, where M can take the name of any level in the arithmetical or hyper-arithmetical hierarchy. PREPRINT

A study of fuzzy and many-valued logics in cellular automata Mingarelli A B 2006 In this paper we provide an analytical study of the theory of multi-valued and fuzzy cellular automata where the fuzziness appears as the result of the application of an underlying multi-valued or continuous logic as opposed to standard logic as used conventionally. Using the disjunctive normal form of any one of the 255 ECA's so defined, we modify the underlying logic structure and redefine the ECA within the framework of this new logic. The idea here is to show that the evolution of space-time diagrams of ECA's under even a probabilistic logic can exhibit non-chaotic behavior. This is looked at specifically for Probabilistic Rule 110, in contrast with Boolean Rule 110 which is known to be capable of universal computation. PREPRINT

Stationary Algorithmic Probability Müller M 2006 Kolmogorov complexity and algorithmic probability quantify the randomness and universal a priori probability of finite binary strings. Nevertheless, they share the disadvantage of depending on the choice of the universal computer which is used as a reference computer to count the program lengths. In this paper, we propose an approach to algorithmic probability that tries to eliminate this machine-dependence. Elaborating on the idea that computers with ``atypical'' algorithmic probability should be hard to emulate, we define the notion of emulation complexity. This naturally leads to a Markov process of universal computers that randomly emulate each other, yielding stationary probability distributions on the computers and finite binary strings. By proving symmetry relations with respect to input and output transformations, we show that properties of individual computers are successfully eliminated. Our approach is not limited to prefix-free computers, but can be applied to more general sets of computers. The question for what computer sets such stationary distributions exist remains open in general, but is answered in some special cases and is shown to be closely related to the aforementioned symmetry relations. PREPRINT

Aperiodic packings of clusters obtained by projection Cotfas N 2006 We present a modified version of the strip projection method which allows one to generate aperiodic packings of clusters. By including some points that are outside the projection strip, and deleting some that are inside, a structure with a higher density of complete symmetric clusters is achieved. Our algorithm may be useful in structure description of quasicrystals. PREPRINT

Neural Network Clustering Based on Distances Between Objects Litinskii L B Romanov D E 2006 We present an algorithm of clustering of many-dimensional objects, where only the distances between objects are used. Centers of classes are found with the aid of neuron-like procedure with lateral inhibition. The result of clustering does not depend on starting conditions. Our algorithm makes it possible to give an idea about classes that really exist in the empirical data. The results of computer simulations are presented. PREPRINT

Calculating modules in contextual logic program refinement Colvin R Hayes O J Strooper P 2006 The refinement calculus for logic programs is a framework for deriving logic programs from specifications. It is based on a wide-spectrum language that can express both specifications and code, and a refinement relation that models the notion of correct implementation. In this paper we extend and generalise earlier work on contextual refinement. Contextual refinement simplifies the refinement process by abstractly capturing the context of a subcomponent of a program, which typically includes information about the values of the free variables. This paper also extends and generalises module refinement. A module is a collection of procedures that operate on a common data type; module refinement between a specification module A and an implementation module C allows calls to the procedures of A to be systematically replaced with calls to the corresponding procedures of C. Based on the conditions for module refinement, we present a method for calculating an implementation module from a specification module. Both contextual and module refinement within the refinement calculus have been generalised from earlier work and the results are presented in a unified framework. PREPRINT

Some Pattern Recognition Challenges in Data-Intensive Astronomy Djorgovski S G Donalek C Mahabal A Williams R Drake A Graham M Glikman E 2006 We review some of the recent developments and challenges posed by the data analysis in modern digital sky surveys, which are representative of the information-rich astronomy in the context of Virtual Observatory. Illustrative examples include the problems of an automated star-galaxy classification in complex and heterogeneous panoramic imaging data sets, and an automated, iterative, dynamical classification of transient events detected in synoptic sky surveys. These problems offer good opportunities for productive collaborations between astronomers and applied computer scientists and statisticians, and are representative of the kind of challenges now present in all data-intensive fields. We discuss briefly some emergent types of scalable scientific data analysis systems with a broad applicability. PREPRINT

A multiplexed single electron transistor for application in scalable solid-state quantum computing Conrad V I Greentree A D Hollenberg L C L 2006 Single Electron Transistors (SETs) are nanoscale electrometers of unprecedented sensitivity, and as such have been proposed as read-out devices in a number of quantum computer architectures. We show that the functionality of a standard SET can be multiplexed so as to operate as both read-out device and control gate for a solid-state qubit. Multiplexing in this way may be critical in lowering overall gate densities in scalable quantum computer architectures. PREPRINT

Scaled Particle Theory for Hard Sphere Pairs. II. Numerical Analysis Chatterjee S De Benedetti P G Stillinger F H 2006 We use the extension of scaled particle theory (ESPT) presented in the accompanying paper [Stillinger et al. J. Chem. Phys. xxx, xxx (2007)] to calculate numerically pair correlation function of the hard sphere fluid over the density range $0\leq \rho\sigma^3\leq 0.96$. Comparison with computer simulation results reveals that the new theory is able to capture accurately the fluid's structure across the entire density range examined. The pressure predicted via the virial route is systematically lower than simulation results, while that obtained using the compressibility route is lower than simulation predictions for $\rho\sigma^3\leq 0.67$ and higher than simulation predictions for $\rho\sigma^3\geq 0.67$. Numerical predictions are also presented for the surface tension and Tolman length of the hard sphere fluid. PREPRINT

Putting your computer to work to fight against malaria in Africa 2006 "While your are sending an email or surfing the web, your computer could be helping to tackle one of Africa's major humanitarian challenges, malaria." (1 page) CUTTING

Key dates in 25 years of the PC 2006 Important dates from January 1973 to December 2004 CUTTING

World Wide Web also celebrating a birthday 2006 "The PC isn't the only electronic wonder that recently had an anniversary. The World Wide Web turned 15 this month." (1/2 page) CUTTING

Massive Parallel Quantum Computer Simulator De Raedt K Arnold G De Raedt H Ito N Lippert T Michielsen K Richter M Trieu B Watanabe H 2006 We describe portable software to simulate universal quantum computers on massive parallel computers. We illustrate the use of the simulation software by running various quantum algorithms on different computer architectures, such as a IBM BlueGene/L, a IBM Regatta p690+, a Hitachi SR11000/J1, a Cray X1E, a SGI Altix 3700 and clusters of PCs running Windows XP. We study the performance of the software by simulating quantum computers containing up to 36 qubits, using up to 4096 processors and up to 1 TB of memory. Our results demonstrate that the simulator exhibits nearly ideal scaling as a function of the number of processors and suggest that the simulation software described in this paper may also serve as benchmark for testing high-end parallel computers. PREPRINT

Context for models of concurrency Bubenik P 2006 Many categories have been used to model concurrency. Using any of these, the challenge is to reduce a given model to a smaller representation which nevertheless preserves the relevant computer-scientific information. That is, one wants to replace a given model with a simpler model with the same directed homotopy-type. Unfortunately, the obvious definition of directed homotopy equivalence is too coarse. This paper introduces the notion of context to refine this definition. PREPRINT

Technology Transfer 1994 ARC012614

Gauge sector statistics of intersecting D-brane models Gmeiner F 2006 In this article, which is based on the first part of my PhD thesis, I review the statistics of the open string sector in T^6/(Z_2xZ_2) orientifold compactifications of the type IIA string. After an introduction to the orientifold setup, I discuss the two different techniques that have been developed to analyse the gauge sector statistics, using either a saddle point approximation or a direct computer based method. The two approaches are explained and compared by means of eight- and six-dimensional toy models. In the four-dimensional case the results are presented in detail. Special emphasis is put on models containing phenomenologically interesting gauge groups and chiral matter, in particular those containing a standard model or SU(5) part. PREPRINT

Towards a Solution of the Polycyclic Aromatic Hydrocarbon - Diffuse Interstellar Band Hypothesis Tan X 2006 A novel theoretical method is developed to study the polycyclic aromatic hydrocarbon - diffuse interstellar band (PAH-DIB) hypothesis. In this method, a computer program is used to enumerate all PAH molecules with up to a specific number of fused benzene rings. Fast quantum chemical calculations are then employed to calculate the electronic transition energies, oscillator strengths, and rotational constants of these molecules. An electronic database of all PAHs with up to any specific number of benzene rings can be constructed this way. Comparison of the electronic transition energies, oscillator strengths, and rotational band contours of all PAHs in the database with astronomical spectra allows one to identify possible individual PAH carriers of some of the intense narrow DIBs. Using the current database containing up to 10 benzene rings we have selected 8 closed-shell PAHs as possible carriers of the intense lambda6614 DIB. PREPRINT

Resolving photon number states in a superconducting circuit Schuster D I Houck A A Schreier J A Wallraff A Gambetta J M Blais A Frunzio L Johnson B Devoret M H Girvin S M Schölkopf R J 2006 Electromagnetic signals are always composed of photons, though in the circuit domain those signals are carried as voltages and currents on wires, and the discreteness of the photon's energy is usually not evident. However, by coupling a superconducting qubit to signals on a microwave transmission line, it is possible to construct an integrated circuit where the presence or absence of even a single photon can have a dramatic effect. This system is called circuit quantum electrodynamics (QED) because it is the circuit equivalent of the atom-photon interaction in cavity QED. Previously, circuit QED devices were shown to reach the resonant strong coupling regime, where a single qubit can absorb and re-emit a single photon many times. Here, we report a circuit QED experiment which achieves the strong dispersive limit, a new regime of cavity QED in which a single photon has a large effect on the qubit or atom without ever being absorbed. The hallmark of this strong dispersive regime is that the qubit transition can be resolved into a separate spectral line for each photon number state of the microwave field. The strength of each line is a measure of the probability to find the corresponding photon number in the cavity. This effect has been used to distinguish between coherent and thermal fields and could be used to create a photon statistics analyzer. Since no photons are absorbed by this process, one should be able to generate non-classical states of light by measurement and perform qubit-photon conditional logic, the basis of a logic bus for a quantum computer. PREPRINT

Antipersistant Effects in the Dynamics of a Competing Population Lee K H Wong K Y M 2006 We consider a population of agents competing for finite resources using strategies based on two channels of signals. The model is applicable to financial markets, ecosystems and computer networks. We find that the dynamics of the system is determined by the correlation between the two channels. In particular, occasional mismatches of the signals induce a series of transitions among numerous attractors. Surprisingly, in contrast to the effects of noises on dynamical systems normally resulting in a large number of attractors, the number of attractors due to the mismatched signals remains finite. Both simulations and analyses show that this can be explained by the antipersistent nature of the dynamics. Antipersistence refers to the response of the system to a given signal being opposite to that of the signal's previous occurrence, and is a consequence of the competition of the agents to make minority decisions. Thus, it is essential for stabilizing the dynamical systems. PREPRINT

Time's Arrow from the Multiverse Point of View Tamm M 2006 In this paper I suggest a possible explanation for the asymmetry of time. In the models that I study, the dynamical laws and the boundary conditions are completely symmetric, but the behaviour of time is not. The underlying mechanism is a spontaneously broken symmetry on the micro-level which is closely related to the idea of multiple histories in quantum mechanics. The situations that I will discuss are very simple and could even in a sense be called classical, but the character of the mechanism is so general that the results are likely to carry over to more complicated cases. Since the computational difficulties are enormous, I mainly use heuristic methods and computer computations to exploit these ideas. PREPRINT

One method for proving inequalities by computer Malesevic B J 2006 In this paper we consider a method for proving a class of analytical inequalities via minimax rational approximations. All numerical calculations in this paper are given by Maple computer program. PREPRINT

Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations Blanqui F 2006 Since Val Tannen's pioneer work on the combination of simply-typed lambda-calculus and first-order rewriting (LICS'88), many authors have contributed to this subject by extending it to richer typed lambda-calculi and rewriting paradigms, culminating in calculi like the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are defined by oriented higher-order equations. This kind of definitions subsumes induction-based definitions, is easier to write and provides more automation. On the other hand, checking that user-defined rewrite rules are strongly normalizing and confluent, and preserve the decidability of type-checking when combined with beta-reduction, is more difficult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of ``sized types'' studied by several authors in the simpler framework of ML-like languages, and proved that it preserves strong normalization. The main contribution of the present paper is twofold. First, we prove that, in the Calculus of Algebraic Constructions with size annotations, the problems of type inference and type-checking are decidable, provided that the sets of constraints generated by size annotations are satisfiable and admit most general solutions. Second, we prove the later properties for a size algebra rich enough for capturing usual induction-based definitions and much more. PREPRINT

Adaptive molecular resolution via a continuous change of the phase space dimensionality Praprotnik M Kremer K Site L D 2006 For the study of complex synthetic and biological molecular systems by computer simulations one is still restricted to simple model systems or to by far too small time scales. To overcome this problem multiscale techniques are being developed for many applications. However in almost all cases, the regions of different resolution are fixed and not in a true equilibrium with each other. We here give the theoretical framework for an efficient and flexible coupling of the different regimes. The approach leads to an analog of a geometry induced phase transition and a counterpart of the equipartition theorem for fractional degrees of freedom. This provides a rather general formal basis for advanced computer simulation methods applying different levels of resolution. PREPRINT

981547 oai:cds.cern.ch:981547 DELETED

On the confluence of lambda-calculus with conditional rewriting Blanqui F Kirchner C Riba C 2006 The confluence of untyped lambda-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the confluence of lambda-calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Muller and Dougherty for unconditional rewriting. Two cases are considered, whether beta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty's result is improved from the assumption of strongly normalizing beta-reduction to weakly normalizing beta-reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using an extended notion of orthogonality that takes advantage of the conditional part of rewrite rules. PREPRINT

Connection between continuous and digital n-manifolds and the Poincare conjecture Evako A 2006 We introduce LCL covers of closed n-dimensional manifolds by n-dimensional disks and study their properties. We show that any LCL cover of an n-dimensional sphere can be converted to the minimal LCL cover, which consists of 2n+2 disks. We prove that an LCL collection of n-disks is a cover of a continuous n-sphere if and only if the intersection graph of this collection is a digital n-sphere. Using a link between LCL covers of closed continuous n-manifolds and digital n-manifolds, we find conditions where a continuous closed three-dimensional manifold is the three-dimensional sphere. We discuss a connection between the classification problems for closed continuous three-dimensional manifolds and digital three-manifolds. PREPRINT

Controller synthesis & Ordinal Automata Cachat T 2006 Ordinal automata are used to model physical systems with Zeno behavior. Using automata and games techniques we solve a control problem formulated and left open by Demri and Nowak in 2005. It involves partial observability and a new synchronization between the controller and the environment. PREPRINT

A general relativistic model for the light propagation in the gravitational field of the Solar System: the dynamical case De Felice F Vecchiato A Crosta M T Lattanzi M G Bucciarelli B 2006 Modern astrometry is based on angular measurements at the micro-arcsecond level. At this accuracy a fully general relativistic treatment of the data reduction is required. This paper concludes a series of articles dedicated to the problem of relativistic light propagation, presenting the final microarcsecond version of a relativistic astrometric model which enable us to trace back the light path to its emitting source throughout the non-stationary gravity field of the moving bodies in the Solar System. The previous model is used as test-bed for numerical comparisons to the present one. Here we also test different versions of the computer code implementing the model at different levels of complexity to start exploring the best trade-off between numerical efficiency and the micro-arcsecond accuracy needed to be reached. PREPRINT

Introduction to Non-Linear Algebra Dolotin V Morozov A 2006 Concise introduction to a relatively new subject of non-linear algebra: literal extension of text-book linear algebra to the case of non-linear equations and maps. This powerful science is based on the notions of discriminant (hyperdeterminant) and resultant, which today can be effectively studied both analytically and by modern computer facilities. The paper is mostly focused on resultants of non-linear maps. First steps are described in direction of Mandelbrot-set theory, which is direct extension of the eigenvalue problem from linear algebra, and is related by renormalization group ideas to the theory of phase transitions and dualities. PREPRINT

In Quest of Image Semantics: Are We Looking for It Under the Right Lamppost? Diamant E 2006 In the last years we witness a dramatic growth of research focused on semantic image understanding. Indeed, without understanding image content successful accomplishment of any image-processing task is simply incredible. Up to the recent times, the ultimate need for such understanding has been met by the knowledge that a domain expert or a vision system supervisor have contributed to every image-processing application. The advent of the Internet has drastically changed this situation. Internet sources of visual information are diffused and dispersed over the whole Web, so the duty of information content discovery and evaluation must be relegated now to an image understanding agent (a machine or a computer program) capable to perform image content assessment at a remote image location. Development of Content Based Image Retrieval (CBIR) techniques was a right move in a right direction, launched about ten years ago. Unfortunately, very little progress has been made since then. The reason for this can be seen in a rank of long lasting misconceptions that CBIR designers are continuing to adhere to. I hope, my arguments will help them to change their minds. PREPRINT

An effective edge--directed frequency filter for removal of aliasing in upsampled images Rataj A 2006 Raster images can have a range of various distortions connected to their raster structure. Upsampling them might in effect substantially yield the raster structure of the original image, known as aliasing. The upsampling itself may introduce aliasing into the upsampled image as well. The presented method attempts to remove the aliasing using frequency filters based on the discrete fast Fourier transform, and applied directionally in certain regions placed along the edges in the image. As opposed to some anisotropic smoothing methods, the presented algorithm aims to selectively reduce only the aliasing, preserving the sharpness of image details. The method can be used as a post--processing filter along with various upsampling algorithms. It was experimentally shown that the method can improve the visual quality of the upsampled images. PREPRINT

On the freeze quantifier in Constraint LTL: decidability and complexity Demri S Lazic R Nowak D 2006 Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for sequence diagrams, navigation logics, logics with lambda-abstraction etc.). We show that Constraint LTL over the simple domain (N,=) augmented with the freeze quantifier is undecidable which is a surprising result in view of the poor language for constraints (only equality tests). Many versions of freeze-free Constraint LTL are decidable over domains with qualitative predicates and our undecidability result actually establishes Sigma_1^1-completeness. On the positive side, we provide complexity results when the domain is finite (EXPSPACE-completeness) or when the formulae are flat in a sense introduced in the paper. Our undecidability results are sharp (i.e. with restrictions on the number of variables) and all our complexity characterisations ensure completeness with respect to some complexity class (mainly PSPACE and EXPSPACE). PREPRINT

On class visualisation for high dimensional data: Exploring scientific datasets Kaban Ata Sun J Raychaudhuri S Nolan L 2006 Parametric Embedding (PE) has recently been proposed as a general-purpose algorithm for class visualisation. It takes class posteriors produced by a mixture-based clustering algorithm and projects them in 2D for visualisation. However, although this fully modularised combination of objectives (clustering and projection) is attractive for its conceptual simplicity, in the case of high dimensional data, we show that a more optimal combination of these objectives can be achieved by integrating them both into a consistent probabilistic model. In this way, the projection step will fulfil a role of regularisation, guarding against the curse of dimensionality. As a result, the tradeoff between clustering and visualisation turns out to enhance the predictive abilities of the overall model. We present results on both synthetic data and two real-world high-dimensional data sets: observed spectra of early-type galaxies and gene expression arrays. PREPRINT

Hybrid Dynamic Density Functional Theory for Polymer Melts and Blends Honda T Kawakatsu T 2006 We propose a high-speed and accurate hybrid dynamic density functional theory for the computer simulations of the phase separation processes of polymer melts and blends. The proposed theory is a combination of the dynamic self-consistent field (SCF) theory and a time-dependent Ginzburg-Landau type theory with the random phase approximation (GRPA). The SCF theory is known to be accurate in evaluating the free energy of the polymer systems in both weak and strong segregation regions although it has a disadvantage of the requirement of a considerable amount of computational cost. On the other hand, the GRPA theory has an advantage of much smaller amount of required computational cost than the SCF theory while its applicability is limited to the weak segregation region. To make the accuracy of the SCF theory and the high-performance of the GRPA theory compatible, we adjust the chemical potential of the GRPA theory by using the SCF theory every constant time steps in the dynamic simulations. The performance of the GRPA and the hybrid theories is tested by using several systems composed of an A/B homopolymer, an AB diblock copolymer, or an ABC triblock copolymer. Using the hybrid theory, we succeeded in reproducing the metastable complex phase-separated domain structures of an ABC triblock copolymer observed by experiments. PREPRINT

Liquid-vapor transition of systems with mean field universality class Pauschenwein G J Caillol J M Levesque D Weis J J Schoell-Paschinger E Kahl G 2006 We have considered a system where the interaction, v(r) = v_IS(r) + xi^2 v_MF(r), is given as a linear combination of two potentials, each of which being characterized with a well-defined critical behavior: for v_IS(r) we have chosen the potential of the restricted primitive model which is known to belong to the Ising 3D (IS) universality class, while for v_MF(r) we have considered a long-range interaction in the Kac-limit, displaying mean field (MF) behavior. We study the performance of two theoretical approaches and of computer simulations in the critical region for this particular system and give a detailed comparison between theories and simulation of the critical region and the location of the critical point. Both, theory and simulation give evidence that the system belongs to the MF universality class for any positive value of xi and that it shows only non-classical behavior for xi=0. While in this limiting case theoretical approaches are known to fail, we find good agreement for the critical properties between the theoretical approaches and the simulations for xi^2 larger than 0.05. PREPRINT

Mobile particles in an immobile environment: Molecular Dynamics simulation of a binary Yukawa mixture Kikuchi N Horbach J 2006 Molecular dynamics computer simulations are used to investigate thedynamics of a binary mixture of charged (Yukawa) particles with a size-ratio of 1:5. We find that the system undergoes a phase transition where the large particles crystallize while the small particles remain in a fluid-like (delocalized) phase. Upon decreasing temperature below the transition, the small particles become increasingly localized on intermediate time scales. This is reflected in the incoherent intermediate scattering functions by the appearance of a plateau with a growing height. At long times, the small particles show a diffusive hopping motion. We find that these transport properties are related to structural correlations and the single-particle potential energy distribution of the small particles. PREPRINT

Philos. Trans. R. Soc. Lond., A Philos. Trans. R. Soc. Lond., A A random walk approach to quantum algorithms Kendon V 2006 364 3407 3422 The development of quantum algorithms based on quantum versions of random walks is placed in the context of the emerging field of quantum computing. Constructing a suitable quantum version of a random walk is not trivial: pure quantum dynamics is deterministic, so randomness only enters during the measurement phase, i.e., when converting the quantum information into classical information. The outcome of a quantum random walk is very different from the corresponding classical random walk, due to interference between the different possible paths. The upshot is that quantum walkers find themselves further from their starting point on average than a classical walker, and this forms the basis of a quantum speed up that can be exploited to solve problems faster. Surprisingly, the effect of making the walk slightly less than perfectly quantum can optimize the properties of the quantum walk for algorithmic applications. Looking to the future, with even a small quantum computer available, development of quantum walk algorithms might proceed more rapidly than it has, especially for solving real problems. research-article

Residual Finite Tree Automata Carme J Gilleron R Lemay A Terlutte A Tommasi M 2006 Tree automata based algorithms are essential in many fields in computer science such as verification, specification, program analysis. They become also essential for databases with the development of standards such as XML. In this paper, we define new classes of non deterministic tree automata, namely residual finite tree automata (RFTA). In the bottom-up case, we obtain a new characterization of regular tree languages. In the top-down case, we obtain a subclass of regular tree languages which contains the class of languages recognized by deterministic top-down tree automata. RFTA also come with the property of existence of canonical non deterministic tree automata. PREPRINT

Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems Blanqui F Riba C 2006 In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially developed for ML-like programs. Here, we go one step further by considering conditional rewriting and explicit quantifications and constraints on size annotations. This allows to describe more precisely how the size of the output of a function depends on the size of its inputs. Hence, we can check the termination of more functions. We first give a general type-checking algorithm based on constraint solving. Then, we give a termination criterion with constraints in Presburger arithmetic. To our knowledge, this is the first termination criterion for higher-order conditional rewriting taking into account the conditions in termination. PREPRINT

Robust quantum searching using spontaneous decay Spreeuw R J C Hijmans T W 2006 We introduce spontaneous decay of qubits to damp the oscillations in a single-item quantum search. This allows a more robust mode of operation where the readout is performed after the system has reached a steady state, rather than after a prescribed number of iterations. We show numerically for up to q=29 qubits that, with near-unit probability, the readout yields an error-free solution after O(log q) repetitions. The huge size of the state space is dealt with by exploiting a symmetry in the master equation that reduces the scaling of computer resources from exponential to polynomial. PREPRINT

Non uniform (hyper/multi)coherence spaces Boudes P 2006 In (hyper)coherence semantics, proofs/terms are cliques in (hyper)graphs. Intuitively, vertices represent results of computations and the edge relation witnesses the ability of being assembled into a same piece of data or a same (strongly) stable function, at arrow types. In (hyper)coherence semantics, the argument of a (strongly) stable functional is always a (strongly) stable function. As a consequence, comparatively to the relational semantics, where there is no edge relation, some vertices are missing. Recovering these vertices is essential for the purpose of reconstructing proofs/terms from their interpretations. It shall also be useful for the comparison with other semantics, like game semantics. In [BE01], Bucciarelli and Ehrhard introduced a so called non uniform coherence space semantics where no vertex is missing. By constructing the co-free exponential we set a new version of this last semantics, together with non uniform versions of hypercoherences and multicoherences, a new semantics where an edge is a finite multiset. Thanks to the co-free construction, these non uniform semantics are deterministic in the sense that the intersection of a clique and of an anti-clique contains at most one vertex, a result of interaction, and extensionally collapse onto the corresponding uniform semantics. PREPRINT

Dichotomies and Duality in First-order Model Checking Problems Martin B 2006 We study the complexity of the model checking problem, for fixed model A, over certain fragments L of first-order logic. These are sometimes known as the expression complexities of L. We obtain various complexity classification theorems for these logics L as each ranges over models A, in the spirit of the dichotomy conjecture for the Constraint Satisfaction Problem -- which itself may be seen as the model checking problem for existential conjunctive positive first-order logic. PREPRINT

Efficient algorithm for multi-qudit twirling Tóth G García-Ripoll J J 2006 We present an efficient algorithm for computing the state obtained from twirling a multi-qudit density matrix. The algorithm can be used both for approximating the twirling operation in a physical system and for computing the twirled density matrix on a classical computer. The method is based on a simple non-unitary operation involving a random unitary. When applying this basic building block iteratively, the mean squared error of the approximation decays exponentially. In contrast, when averaging over random unitary matrices the error decreases only algebraically. We present evidence that the unitaries in our algorithm can come from a very imperfect random source or can even be chosen deterministically from a set of cyclically alternating matrices. Based on these ideas we present a quantum circuit realizing twirling efficiently. PREPRINT

Characterizing multiparticle entanglement in symmetric N-qubit states via negativity of covariance matrices Devi A R U Prabhu R Rajagopal A K 2006 We show that higher order inter-group correlations involving even number of qubits are necessarily positive semidefinite for separable symmetric N qubit states. This identification leads to a family of inseparability conditions based on the negativity of 2kth order inter-group covariance matrices of symmetric N-qubit systems. These conditions have a simple structure and detect multiparty entanglement in both pure and mixed symmetric multiqubit states. The correlation observables involved are feasible experimental quantities and do not demand full state determination through quantum state tomography. PREPRINT

Upgrade of the Cellular General Purpose Monte Carlo Tool FOAM to version 2.06 Jadach Stanislaw Sawicki P 2006 FOAM-2.06 is an upgraded version of FOAM, a general purpose, self-adapting Monte Carlo event generator. In comparison with FOAM-2.05, it has two important improvements. New interface to random numbers lets the user to choose from the three "state of the art" random number generators. Improved algorithms for simplical grid need less computer memory; the problem of the prohibitively large memory allocation required for the large number ($>10^6$) of simplical cells is now eliminated -- the new version can handle such cases even on the average desktop computers. In addition, generation of the Monte Carlo events, in case of large number of cells, may be even significantly faster. PREPRINT

Reduced Area Low Power High Throughput BCD Adders for IEEE 754r Format Thapliyal H Arabnia H R Srinivas M B 2006 IEEE 754r is the ongoing revision to the IEEE 754 floating point standard and a major enhancement to the standard is the addition of decimal format. Firstly, this paper proposes novel two transistor AND and OR gates. The proposed AND gate has no power supply, thus it can be referred as the Powerless AND gate. Similarly, the proposed two transistor OR gate has no ground and can be referred as Groundless OR. Secondly for IEEE 754r format, two novel BCD adders called carry skip and carry look-ahead BCD adders are also proposed in this paper. In order to design the carry look-ahead BCD adder, a novel 4 bit carry look-ahead adder called NCLA is proposed which forms the basic building block of the proposed carry look-ahead BCD adder. Finally, the proposed two transistors AND and OR gates are used to provide the optimized small area low power high throughput circuitries of the proposed BCD adders. PREPRINT

Social Decision Making with Multi-Relational Networks and Grammar-Based Particle Swarms Rodríguez M A 2006 Social decision support systems are able to aggregate the local perspectives of a diverse group of individuals into a global social decision. This paper presents a multi-relational network ontology and grammar-based particle swarm algorithm capable of aggregating the decisions of millions of individuals. This framework supports a diverse problem space and a broad range of vote aggregation algorithms. These algorithms account for individual expertise and representation across different domains of the group problem space. Individuals are able to pose and categorize problems, generate potential solutions, choose trusted representatives, and vote for particular solutions. Ultimately, via a social decision making algorithm, the system aggregates all the individual votes into a single collective decision. PREPRINT

(HO)RPO Revisited Blanqui F 2006 The notion of computability closure has been introduced for proving the termination of the combination of higher-order rewriting and beta-reduction. It is also used for strengthening the higher-order recursive path ordering. In the present paper, we study in more details the relations between the computability closure and the (higher-order) recursive path ordering. We show that the first-order recursive path ordering is equal to an ordering naturally defined from the computability closure. In the higher-order case, we get an ordering containing the higher-order recursive path ordering whose well-foundedness relies on the correctness of the computability closure. This provides a simple way to extend the higher-order recursive path ordering to richer type systems. PREPRINT

Higher-Order Termination: from Kruskal to Computability Blanqui F Jouannaud J P Rubio A 2006 In this paper, we reformulate and improve a recent idea of Blanqui (see the paper "(HO)RPO Revisited") by defining a new version of the HORPO with computability closure which integrates smoothly the idea of the general schema into HORPO in the form of a new ordering definition. PREPRINT

Elgot Algebras Adamek J Milius S Velebil J 2006 Denotational semantics can be based on algebras with additional structure (order, metric, etc.) which makes it possible to interpret recursive specifications. It was the idea of Elgot to base denotational semantics on iterative theories instead, i.e., theories in which abstract recursive specifications are required to have unique solutions. Later Bloom and Esik studied iteration theories and iteration algebras in which a specified solution has to obey certain axioms. We propose so-called Elgot algebras as a convenient structure for semantics in the present paper. An Elgot algebra is an algebra with a specified solution for every system of flat recursive equations. That specification satisfies two simple and well motivated axioms: functoriality (stating that solutions are stable under renaming of recursion variables) and compositionality (stating how to perform simultaneous recursion). These two axioms stem canonically from Elgot's iterative theories: We prove that the category of Elgot algebras is the Eilenberg-Moore category of the monad given by a free iterative theory. PREPRINT

Rational Secret Sharing and Multiparty Computation: Extended Abstract Halpern J Y Teague V 2006 We consider the problems of secret sharing and multiparty computation, assuming that agents prefer to get the secret (resp., function value) to not getting it, and secondarily, prefer that as few as possible of the other agents get it. We show that, under these assumptions, neither secret sharing nor multiparty function computation is possible using a mechanism that has a fixed running time. However, we show that both are possible using randomized mechanisms with constant expected running time. PREPRINT

JHEP JHEP The last of the seven-parton tree amplitudes de Florian D Zurita J 2006 11 We compute the four-quark plus three-gluon and six-quark plus one-gluon tree level amplitudes using on-shell recursion relations. They are needed for the calculation of the 5-jet cross-section at the Born level, and constitute an essential ingredient for next-to-leading order 4-jet and next-to-next-to-leading order 3-jet production at hadronic colliders. Very compact expressions for all possible helicity configurations are provided, allowing direct implementation in computer codes. With the results presented in this paper, the full set of seven-parton tree amplitudes becomes available. research-article

Finite Size Polyelectrolyte Bundles at Thermodynamic Equilibrium Sayar M Holm C 2006 We present the results of extensive computer simulations performed on solutions of monodisperse charged rod-like polyelectrolytes in the presence of trivalent counterions. To overcome energy barriers we used a combination of parallel tempering and hybrid Monte Carlo techniques. Our results show that for small values of the electrostatic interaction the solution mostly consists of dispersed single rods. The potential of mean force between the polyelectrolyte monomers yields an attractive interaction at short distances. For a range of larger values of the Bjerrum length, we find finite size polyelectrolyte bundles at thermodynamic equilibrium. Further increase of the Bjerrum length eventually leads to phase separation and precipitation. We discuss the origin of the observed thermodynamic stability of the finite size aggregates. PREPRINT

On domino insertion and Kazhdan--Lusztig cells in type $B_n$ Bonnaf'e C Geck M Iancu L Lam T 2006 Based on empirical evidence obtained using the {\sf CHEVIE} computer algebra system, we present a series of conjectures concerning the combinatorial description of the Kazhdan--Lusztig cells for type $B_n$ with unequal parameters. These conjectures form a far-reaching extension of the results of Bonnaf\'e and Iancu obtained earlier in the so-called ``asymptotic case''. We give some partial results in support of our conjectures. PREPRINT

J. Automat. Lang. Comput. J. Automat. Lang. Comput. On the logical definability of certain graph and poset languages Weil P 2004 9 147 165 We show that it is equivalent, for certain sets of finite graphs, to be definable in CMS (counting monadic second-order logic, a natural extension of monadic second-order logic), and to be recognizable in an algebraic framework induced by the notion of modular decomposition of a finite graph. More precisely, we consider the set $F\_\infty$ of composition operations on graphs which occur in the modular decomposition of finite graphs. If $F$ is a subset of $F\_{\infty}$, we say that a graph is an $\calF$-graph if it can be decomposed using only operations in $F$. A set of $F$-graphs is recognizable if it is a union of classes in a finite-index equivalence relation which is preserved by the operations in $F$. We show that if $F$ is finite and its elements enjoy only a limited amount of commutativity -- a property which we call weak rigidity, then recognizability is equivalent to CMS-definability. This requirement is weak enough to be satisfied whenever all $F$-graphs are posets, that is, transitive dags. In particular, our result generalizes Kuske's recent result on series-parallel poset languages. research-article

Undecidability of the unification and admissibility problems for modal and description logics Wolter F Zakharyaschev M 2006 We show that the unification problem `is there a substitution instance of a given formula that is provable in a given logic?' is undecidable for basic modal logics K and K4 extended with the universal modality. It follows that the admissibility problem for inference rules is undecidable for these logics as well. These are the first examples of standard decidable modal logics for which the unification and admissibility problems are undecidable. We also prove undecidability of the unification and admissibility problems for K and K4 with at least two modal operators and nominals (instead of the universal modality), thereby showing that these problems are undecidable for basic hybrid logics. Recently, unification has been introduced as an important reasoning service for description logics. The undecidability proof for K with nominals can be used to show the undecidability of unification for boolean description logics with nominals (such as ALCO and SHIQO). The undecidability proof for K with the universal modality can be used to show that the unification problem relative to role boxes is undecidable for Boolean description logic with transitive roles, inverse roles, and role hierarchies (such as SHI and SHIQ). PREPRINT

Digital control system analysis and design Phillips Charles L Nagle H Troy 1984 BOOK

Exploring Computer Science Concepts with a Ready-made Computer Game Framework Distasio J Way T P 2006 Leveraging the prevailing interest in computer games among college students, both for entertainment and as a possible career path, is a major reason for the increasing prevalence of computer game design courses in computer science curricula. Because implementing a computer game requires strong programming skills, game design courses are most often restricted to more advanced computer science students. This paper reports on a ready-made game design and experimentation framework, implemented in Java, that makes game programming more widely accessible. This framework, called Labyrinth, enables students at all programming skill levels to participate in computer game design. We describe the architecture of the framework, and discuss programming projects suitable for a wide variety of computer science courses, from capstone to non-major. PREPRINT

Nominal Logic Programming Cheney J R Urban C 2006 Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, alpha-equivalence). This article investigates logic programming based on nominal logic. This technique is especially well-suited for prototyping type systems, proof theories, operational semantics rules, and other formal systems in which bound names are present. In many cases, nominal logic programs are essentially literal translations of ``paper'' specifications. As such, nominal logic programming provides an executable specification language for prototyping, communicating, and experimenting with formal systems. We describe some typical nominal logic programs, and develop the model-theoretic, proof-theoretic, and operational semantics of such programs. Besides being of interest for ensuring the correct behavior of implementations, these results provide a rigorous foundation for techniques for analysis and reasoning about nominal logic programs, as we illustrate via two examples. PREPRINT

Matrix Games, Linear Programming, and Linear Approximation Vaserstein L N 2006 The following four classes of computational problems are equivalent: solving matrix games, solving linear programs, best $l^{\infty}$ linear approximation, best $l^1$ linear approximation. PREPRINT

Entangling spins by measuring charge: a parity-gate toolbox Ionicioiu R 2006 The parity gate emerged recently as a promising resource for performing universal quantum computation with fermions using only linear interactions. Here we analyse the parity gate (P-gate) from a theoretical point of view in the context of quantum networks. We present several schemes for entanglement generation with P-gates and show that native networks simplify considerably the resources required for producing multi-qubit entanglement, like n-GHZ states. Other applications include a novel Bell-state analyser and teleportation. We then extend this analysis to hybrid quantum networks containing spin and mode qubits. Starting from an easy-to-prepare resource (spin-mode entanglement of single electrons) we show how to produce a spin n-GHZ state with linear elements (beam-splitters and local spin-flips) and charge-parity detectors; this state can be used as a resource in a spin quantum computer or as a precursor for constructing cluster states. Finally, we construct a novel spin CZ-gate by using the mode degrees of freedom as ancillae. PREPRINT

Alexandrov's theorem, weighted Delaunay triangulations, and mixed volumes Bobenko Alexander I Izmestiev I 2006 We present a constructive proof of Alexandrov's theorem regarding the existence of a convex polytope with a given metric on the boundary. The polytope is obtained as a result of a certain deformation in the class of generalized convex polytopes with the given boundary. We study the space of generalized convex polytopes and discover a relation with the weighted Delaunay triangulations of polyhedral surfaces. The existence of the deformation follows from the non-degeneracy of the Hessian of the total scalar curvature of a positively curved generalized convex polytope. The latter is shown to be equal to the Hessian of the volume of the dual generalized polyhedron. We prove the non-degeneracy by generalizing the Alexandrov-Fenchel inequality. Our construction of a convex polytope from a given metric is implemented in a computer program. PREPRINT

RFI detection by automated feature extraction and statistical analysis Winkel B Kerp J Stanko S 2006 In this paper we present an interference detection toolbox consisting of a high dynamic range Digital Fast-Fourier-Transform spectrometer (DFFT, based on FPGA-technology) and data analysis software for automated radio frequency interference (RFI) detection. The DFFT spectrometer allows high speed data storage of spectra on time scales of less than a second. The high dynamic range of the device assures constant calibration even during extremely powerful RFI events. The software uses an algorithm which performs a two-dimensional baseline fit in the time-frequency domain, searching automatically for RFI signals superposed on the spectral data. We demonstrate, that the software operates successfully on computer-generated RFI data as well as on real DFFT data recorded at the Effelsberg 100-m telescope. At 21-cm wavelength RFI signals can be identified down to the 4-sigma level. A statistical analysis of all RFI events detected in our observational data revealed that: (1) mean signal strength is comparable to the astronomical line emission of the Milky Way, (2) interferences are polarised, (3) electronic devices in the neighbourhood of the telescope contribute significantly to the RFI radiation. We also show that the radiometer equation is no longer fulfilled in presence of RFI signals. PREPRINT

Transient Nucleation near the Mean-Field Spinodal Schweiger A O Klein W 2006 We consider nucleation in a one-dimensional $\phi^4$ model with a non-conserved order parameter and long-range interactions. For a sufficiently large system with a slow relaxation to metastable equilibrium, there is a non-negligible probability of nucleation occurring before reaching metastable equilibrium, which we will refer to as transient nucleation. We define the critical droplet to be the object of maximum likelihood that nucleates the system with probability 1/2. We derive time-dependent droplet profiles and nucleation rates; theoretical results are compared to computer simulation. We find a distribution of nucleation times with a distinct peak characteristic of a non-stationary nucleation rate, and that early-time critical droplets are more compact than the droplets found in metastable equilibrium simulations and theoretical predictions. PREPRINT

Large Fourier transforms never exactly realized by braiding conformal blocks Freedman M H Wang Z 2006 Fourier transform is an essential ingredient in Shor's factoring algorithm. In the standard quantum circuit model with the gate set $\{\U(2), \textrm{CNOT}\}$, the discrete Fourier transforms $F_N=(\omega^{ij})_{N\times N},i,j=0,1,..., N-1, \omega=e^{\frac{2\pi i}{N}}$, can be realized exactly by quantum circuits of size $O(n^2), n=\textrm{log}N$, and so can the discrete sine/cosine transforms. In topological quantum computing, the simplest universal topological quantum computer is based on the Fibonacci (2+1)-topological quantum field theory (TQFT), where the standard quantum circuits are replaced by unitary transformations realized by braiding conformal blocks. We report here that the large Fourier transforms $F_N$ and the discrete sine/cosine transforms can never be realized exactly by braiding conformal blocks for a fixed TQFT. It follows that approximation is unavoidable to implement the Fourier transforms by braiding conformal blocks. PREPRINT

Experimental entanglement of six photons in graph states Lu C Y Zhou X Q Gühne O Gao W B Zhang J Yuan Z S Goebel A Yang T Pan J W 2006 Graph states are special kinds of multipartite entangled states that correspond to mathematical graphs where the vertices take the role of quantum spin systems and the edges represent interactions. They not only provide an efficient model to study multiparticle entanglement, but also find wide applications in quantum error correction, multi-party quantum communication and most prominently, serve as the central resource in one-way quantum computation. Here we report the creation of two special instances of graph states, the six-photon Greenberger-Horne-Zeilinger states -- the largest photonic Schr\"{o}dinger cat, and the six-photon cluster states-- a state-of-the-art one-way quantum computer. Flexibly, slight modifications of our method allow creation of many other graph states. Thus we have demonstrated the ability of entangling six photons and engineering multiqubit graph states, and created a test-bed for investigations of one-way quantum computation and studies of multiparticle entanglement as well as foundational issues such as nonlocality and decoherence. PREPRINT

Samba Eckstein Robert Collier-Brown David Kelly Peter 2001 BOOK

Extremal Real Algebraic Geometry and A-Discriminants Dickenstein A Rojas J M Rusek K Shih J 2006 We present a new, far simpler family of counter-examples to Kushnirenko's Conjecture. Along the way, we illustrate a computer-assisted approach to finding sparse polynomial systems with maximally many real roots, thus shedding light on the nature of optimal upper bounds in real fewnomial theory. We use a powerful recent formula for the A-discriminant, and give new bounds on the topology of certain A-discriminant varieties. A consequence of the latter result is a new upper bound on the number of topological types of certain real algebraic sets defined by sparse polynomial equations, e.g., the number of smooth topological types attainable in certain families of real algebraic surfaces. PREPRINT

Total Variation Minimization and Graph Cuts for Moving Objects Segmentation Ranchin F Chambolle A 2006 In this paper, we are interested in the application to video segmentation of the discrete shape optimization problem involving the shape weighted perimeter and an additional term depending on a parameter. Based on recent works and in particular the one of Darbon and Sigelle, we justify the equivalence of the shape optimization problem and a weighted total variation regularization. For solving this problem, we adapt the projection algorithm proposed recently for solving the basic TV regularization problem. Another solution to the shape optimization investigated here is the graph cut technique. Both methods have the advantage to lead to a global minimum. Since we can distinguish moving objects from static elements of a scene by analyzing norm of the optical flow vectors, we choose the optical flow norm as initial data. In order to have the contour as close as possible to an edge in the image, we use a classical edge detector function as the weight of the weighted total variation. This model has been used in one of our former works. We also apply the same methods to a video segmentation model used by Jehan-Besson, Barlaud and Aubert. In this case, only standard perimeter is incorporated in the shape functional. We also propose another way for finding moving objects by using an a contrario detection of objects on the image obtained by solving the Rudin-Osher-Fatemi Total Variation regularization problem.We can notice the segmentation can be associated to a level set in the former methods. PREPRINT

Free Choice Petri Nets without frozen tokens and Bipolar Synchronization Systems Wehler J 2006 Bipolar synchronization systems (BP-systems) constitute a class of coloured Petri nets, well suited for modeling the control flow of discrete, dynamical systems. Every BP-system has an underlying ordinary Petri net, which is a T-system. Moreover, it has a second ordinary net attached, which is a free-choice system. We prove that a BP-system is live and safe if the T-system and the free-choice system are live and safe and if the free-choice system has no frozen tokens. This result is the converse of a theorem of Genrich and Thiagarajan and proves an elder conjecture. The proof compares the different Petri nets by Petri net morphisms and makes use of the classical theory of free-choice systems PREPRINT

Using groups for investigating rewrite systems Dehornoy P 2006 We describe several technical tools that prove to be efficient for investigating the rewrite systems associated with a family of algebraic laws, and might be useful for more general rewrite systems. These tools consist in introducing a monoid of partial operators, listing the monoid relations expressing the possible local confluence of the rewrite system, then introducing the group presented by these relations, and finally replacing the initial rewrite system with a internal process entirely sitting in the latter group. When the approach can be completed, one typically obtains a practical method for constructing algebras satisfying prescribed laws and for solving the associated word problem. PREPRINT

On Verifying Complex Properties using Symbolic Shape Analysis Wies T Kuncak V Zee K Podelski A Rinard M 2006 One of the main challenges in the verification of software systems is the analysis of unbounded data structures with dynamic memory allocation, such as linked data structures and arrays. We describe Bohne, a new analysis for verifying data structures. Bohne verifies data structure operations and shows that 1) the operations preserve data structure invariants and 2) the operations satisfy their specifications expressed in terms of changes to the set of objects stored in the data structure. During the analysis, Bohne infers loop invariants in the form of disjunctions of universally quantified Boolean combinations of formulas. To synthesize loop invariants of this form, Bohne uses a combination of decision procedures for Monadic Second-Order Logic over trees, SMT-LIB decision procedures (currently CVC Lite), and an automated reasoner within the Isabelle interactive theorem prover. This architecture shows that synthesized loop invariants can serve as a useful communication mechanism between different decision procedures. Using Bohne, we have verified operations on data structures such as linked lists with iterators and back pointers, trees with and without parent pointers, two-level skip lists, array data structures, and sorted lists. We have deployed Bohne in the Hob and Jahob data structure analysis systems, enabling us to combine Bohne with analyses of data structure clients and apply it in the context of larger programs. This report describes the Bohne algorithm as well as techniques that Bohne uses to reduce the ammount of annotations and the running time of the analysis. PREPRINT

Mathematica 1993 BOOK

Helix formation in linear achiral dendronized polymers. A computer simulation study Christopoulos D K Terzis A F Vanakaras A G Photinos D J 2006 We present a molecular simulation study of the structure of linear dendronized polymers. We use excluded volume interactions in the context of a generic coarse-grained molecular model whose geometrical parameters are tuned to represent a poly(para-phenylene) backbone with benzyl ether, Frechet type dendrons. We apply Monte Carlo sampling in order to investigate the formation of packing-induced chiral structures along the polymer backbone of these chemically non-chiral systems. We find that helical structures can be formed, usually with defects consisting of domains with reversed helical handedness. Clear signs of helical arrangements of the dendrons begin to appear for dendritic generation g=4, while for g=5 these arrangements dominate and perfect helices can even be observed as equilibrium structures obtained from certain types of starting configurations. PREPRINT

Equation of State for Supercooled Water Near the Liquid-Liquid Critical Point Anisimov M A Fuentevilla D A 2006 We have developed a scaled parametric equation of state to describe and predict thermodynamic properties of supercooled water. The equation of state, built on the growing evidence that the critical point of supercooled liquid-liquid water separation exists, is universal in terms of theoretical scaling fields and is shown to belong to the Ising-model class of universality. The theoretical scaling fields are postulated to be analytical combinations of the physical fields, pressure and temperature. The equation of state enables us to accurately locate the "Widom line" (the locus of stability minima) and determine that the critical pressure is considerably lower than predicted by computer simulations. PREPRINT

Generalized Majority-Minority Operations are Tractable Dalmau V 2006 Let $A$ be a finite set and let $\phi:A^k\to A$ with $k\geq 3$ be a $k$-ary operation on $A$. We say that $\phi$ is a generalized majority-minority (GMM) operation if for all $a,b\in A$ we have that $\phi(x,y,..,y)=\phi(y,x,..,y)=...=\phi(y,y,..,x)=y$ for all $x,y\in\{a,b\}$ or $\phi(x,y,..,y)=\phi(y,y,..,x)=x \text{for all} x,y\in\{a,b\}$ Near-unanimity and Mal'tsev operations are particular instances of GMM operations. We prove that every CSP instance where all constraint relations are invariant under a (fixed) GMM operation is solvable in polynomial time. This constitutes one of the largest tractable cases of the CSP. PREPRINT

Theor. Comput. Sci. Theor. Comput. Sci. The recognizability of sets of graphs is a robust property Courcelle B Weil P 2005 342 173 228 Once the set of finite graphs is equipped with an algebra structure (arising from the definition of operations that generalize the concatenation of words), one can define the notion of a recognizable set of graphs in terms of finite congruences. Applications to the construction of efficient algorithms and to the theory of context-free sets of graphs follow naturally. The class of recognizable sets depends on the signature of graph operations. We consider three signatures related respectively to Hyperedge Replacement (HR) context-free graph grammars, to Vertex Replacement (VR) context-free graph grammars, and to modular decompositions of graphs. We compare the corresponding classes of recognizable sets. We show that they are robust in the sense that many variants of each signature (where in particular operations are defined by quantifier-free formulas, a quite flexible framework) yield the same notions of recognizability. We prove that for graphs without large complete bipartite subgraphs, HR-recognizability and VR-recognizability coincide. The same combinatorial condition equates HR-context-free and VR-context-free sets of graphs. Inasmuch as possible, results are formulated in the more general framework of relational structures. research-article

Algebraic recognizability of languages Weil P 2006 Recognizable languages of finite words are part of every computer science cursus, and they are routinely described as a cornerstone for applications and for theory. We would like to briefly explore why that is, and how this word-related notion extends to more complex models, such as those developed for modeling distributed or timed behaviors. PREPRINT

Discovery Mondays: 'The Grid: a universal computer' 2006 BULLETINNEWS

CERN Technical Training 2006 - WBTechT offers online training 2006 BULLETINTRAINING

Computational potency of quantum many-body systems Gross D Eisert J 2006 We establish a framework which allows one to systematically construct novel schemes for measurement-based quantum computation. The technique utilizes tools from many-body physics - based on finitely correlated or projected entangled pair states - to go beyond the cluster-state based one-way computer. We also identify resource states with radically different entanglement properties than the cluster state. It is shown that there exist universal resource states which are locally arbitrarily close to a pure state. We find that non-vanishing two-point correlation functions are no obstacle to universality. An explicit example for a resource state is presented, which can partly be prepared by gates with non-maximal entangling power. Finally, we comment on the possibility of tailoring computational models to specific physical systems as, e.g. in linear optical experiments. PREPRINT

On the additive theory of prime numbers II Cegielski P Richard D Vsemirnov M 2006 The undecidability of the additive theory of primes (with identity) as well as the theory Th(N,+, n -> p\_n), where p\_n denotes the (n+1)-th prime, are open questions. As a possible approach, we extend the latter theory by adding some extra function. In this direction we show the undecidability of the existential part of the theory Th(N, +, n -> p\_n, n -> r\_n), where r\_n is the remainder of p\_n divided by n in the euclidian division. PREPRINT

Theor. Comput. Sci. Theor. Comput. Sci. Algebraic recognizability of regular tree languages Esik Z Weil P 2005 340 291 321 We propose a new algebraic framework to discuss and classify recognizable tree languages, and to characterize interesting classes of such languages. Our algebraic tool, called preclones, encompasses the classical notion of syntactic Sigma-algebra or minimal tree automaton, but adds new expressivity to it. The main result in this paper is a variety theorem \`{a} la Eilenberg, but we also discuss important examples of logically defined classes of recognizable tree languages, whose characterization and decidability was established in recent papers (by Benedikt and S\'{e}goufin, and by Bojanczyk and Walukiewicz) and can be naturally formulated in terms of pseudovarieties of preclones. Finally, this paper constitutes the foundation for another paper by the same authors, where first-order definable tree languages receive an algebraic characterization. research-article

A Richer Understanding of the Complexity of Election Systems Faliszewski P Hemaspaandra E Hemaspaandra L A Rothe J 2006 We provide an overview of some recent progress on the complexity of election systems. The issues studied include the complexity of the winner, manipulation, bribery, and control problems. PREPRINT

Influence of qubit displacements on quantum logic operations in a silicon-based quantum computer with constant interaction Kamenev D I Berman G P Tsifrinovich V I 2006 The errors caused by qubit displacements from their prescribed locations in an ensemble of spin chains are estimated analytically and calculated numerically for a quantum computer based on phosphorus donors in silicon. We show that it is possible to polarize (initialize) the nuclear spins even with displaced qubits by using Controlled NOT gates between the electron and nuclear spins of the same phosphorus atom. However, a Controlled NOT gate between the displaced electron spins is implemented with large error because of the exponential dependence of exchange interaction constant on the distance between the qubits. If quantum computation is implemented on an ensemble of many spin chains, the errors can be small if the number of chains with displaced qubits is small. PREPRINT

Some notes on the program GKINT: Transient-field g-factor kinematics at intermediate energies Stuchbery A E 2006 This report describes the computer program GKINT, which was developed to plan, analyze and interpret the first High Velocity Transient Field (HVTF) g-factor measurements on radioactive beams produced as fast fragments. The computer program and these notes were written in September 2004. Minor corrections and updates have been added to these notes since then. The experiment, NSCL experiment number 02020, 'Excited-state configurations in S-38 and S-40 through transient-field g-factor measurements on fast fragments', was performed in October 2004; results have been published in Physical Review Letters 96, 112503 (2006). PREPRINT

Impact of non-Poisson activity patterns on spreading processes Vazquez A Andras L Balazs R Barabási A L 2007 Halting a computer or biological virus outbreak requires a detailed understanding of the timing of the interactions between susceptible and infected individuals. For example, the spread of email viruses and worms is driven by the email communication and computer usage patterns of individuals. While current spreading models assume that users interact uniformly in time, following a Poisson process, a series of recent measurements indicate that the inter-contact time distribution is heavy tailed, corresponding to a temporally inhomogeneous bursty contact process. Here we show that the non-Poisson nature of the contact dynamics results in prevalence decay times significantly larger than predicted by the standard Poisson process based models. Our predictions are in agreement with the detailed time resolved prevalence data of computer viruses, which, according to virus bulletins, show a decay time close to a year, in contrast with the one day decay predicted by the standard Poisson process based models. PREPRINT

Skew Hadamard difference sets from the Ree-Tits slice symplectic spreads in PG(3,3^{2h+1}) Ding C Wang Z Xiang Q 2006 Using a class of permutation polynomials of $F_{3^{2h+1}}$ obtained from the Ree-Tits symplectic spreads in $PG(3,3^{2h+1})$, we construct a family of skew Hadamard difference sets in the additive group of $F_{3^{2h+1}}$. With the help of a computer, we show that these skew Hadamard difference sets are new when $h=2$ and $h=3$. We conjecture that they are always new when $h>3$. Furthermore, we present a variation of the classical construction of the twin prime power difference sets, and show that inequivalent skew Hadamard difference sets lead to inequivalent difference sets with twin prime power parameters. PREPRINT

Rule-based Knowledge Representation for Service Level Agreement Paschke A 2006 Automated management and monitoring of service contracts like Service Level Agreements (SLAs) or higher-level policies is vital for efficient and reliable distributed service-oriented architectures (SOA) with high quality of ser-vice (QoS) levels. IT service provider need to manage, execute and maintain thousands of SLAs for different customers and different types of services, which needs new levels of flexibility and automation not available with the current technol-ogy. I propose a novel rule-based knowledge representation (KR) for SLA rules and a respective rule-based service level management (RBSLM) framework. My rule-based approach based on logic programming provides several advantages including automated rule chaining allowing for compact knowledge representation and high levels of automation as well as flexibility to adapt to rapidly changing business requirements. Therewith, I address an urgent need service-oriented busi-nesses do have nowadays which is to dynamically change their business and contractual logic in order to adapt to rapidly changing business environments and to overcome the restricting nature of slow change cycles. PREPRINT

Reversible Vortex Ratchet Effects and Ordering in Superconductors with One-Dimensional Asymmetric Potential Arrays Lu Q Olson-Reichhardt C J Reichhardt C 2006 We demonstrate using computer simulations that the simplest vortex ratchet system for type-II superconductors with artificial pinning arrays, an asymmetric one-dimensional (1D) potential array, exhibits the same features as more complicated two-dimensional vortex ratchets that have been studied in recent experiments. We show that the 1D geometry, originally proposed by Lee et al. [Nature 400, 337 (1999)], undergoes multiple reversals in the sign of the ratchet effect as a function of vortex density, substrate strength, and ac drive amplitude, and that the sign of the ratchet effect is related to the type of vortex lattice structure present. When the vortex lattice is highly ordered, an ordinary vortex ratchet effect occurs which is similar to the response of an isolated particle in the same ratchet geometry. In regimes where the vortices form a smectic or disordered phase, the vortex-vortex interactions are relevant and we show with force balance arguments that the ratchet effect can reverse in sign. The dc response of this system features a reversible diode effect and a variety of vortex states including triangular, smectic, disordered and square. PREPRINT

On Bus Graph Realizability Ada A Coggan M Marco P D Doyon A Flookes L Heilala S Kim E Wing J L O Preville-Ratelle L F Whitesides S Yu N 2006 In this paper, we consider the following graph embedding problem: Given a bipartite graph G = (V1; V2;E), where the maximum degree of vertices in V2 is 4, can G be embedded on a two dimensional grid such that each vertex in V1 is drawn as a line segment along a grid line, each vertex in V2 is drawn as a point at a grid point, and each edge e = (u; v) for some u 2 V1 and v 2 V2 is drawn as a line segment connecting u and v, perpendicular to the line segment for u? We show that this problem is NP-complete, and sketch how our proof techniques can be used to show the hardness of several other related problems. PREPRINT

The Three Gap Theorem (Steinhauss Conjecture) Mayero M 2006 We deal with the distribution of N points placed consecutively around the circle by a fixed angle of a. From the proof of Tony van Ravenstein, we propose a detailed proof of the Steinhaus conjecture whose result is the following: the N points partition the circle into gaps of at most three different lengths. We study the mathematical notions required for the proof of this theorem revealed during a formal proof carried out in Coq. PREPRINT

Lect. Notes Comput. Sci. Lect. Notes Comput. Sci. Pores in a two-dimensional network of DNA strands - computer simulations Krawczyk M J Kulakowski K 2006 3991 Formation of random network of DNA strands is simulated on a two-dimensional triangular lattice. We investigate the size distribution of pores in the network. The results are interpreted within theory of percolation on Bethe lattice. research-article

First Principles Calculations of Shock Compressed Fluid Helium Militzer B 2006 The properties of hot dense helium at megabar pressures were studied with two first-principles computer simulation techniques, path integral Monte Carlo and density functional molecular dynamics. The simulations predicted that the compressibility of helium is substantially increased by electronic excitations that are present in the hot fluid at thermodynamic equilibrium. A maximum compression ratio of 5.24(4)-fold the initial density was predicted for 360 GPa and 150000 K. This result distinguishes helium from deuterium, for which simulations predicted a maximum compression ratio of 4.3(1). Hugoniot curves for statically precompressed samples are also discussed. PREPRINT

Verification of crystal collimation model in experiment Biryukov V.M. Serpukhov, IHEP 2006 The studies of crystal collimation in the experiments at Relativistic Heavy Ion Collider and Tevatron and in computer simulations reveal strong coherent effects observed in a very broad angular range. Our theory explains the effects by coherent scattering on the potential of bent crystal atomic planes, which amplifies beam diffusion in accelerator by orders of magnitude. This coherent scattering in bent crystal is being studied in a CERN SPS experiment. We present Monte Carlo predictions for the SPS and Tevatron experiments, and show the implications of the coherent scattering effect for crystal collimation in the Large Hadron Collider. research-article

Interactive computer simulations of electrokinetic physics phenomena Murariu G 2006 In our days, the necessity of laboratory apparatus accustoming by building up specific software objects for studying the virtual evolution of physical phenomena is a major request. In this respect, the aim of the present paper is to present a developed set of electricity interactive simulation computer applica-tions. By following an Object Oriented Programming technology, the necessary software objects are described. Finally, specific examples are extensively presented as well as some screen-shots of the applications interface. PREPRINT

A Predicative Harmonization of the Time and Provable Hierarchies Caporaso S 2006 A decidable transfinite hierarchy is defined by assigning ordinals to the programs of an imperative language. It singles out: the classes TIMEF(n^c) and TIMEF(n_c); the finite Grzegorczyk classes at and above the elementary level, and the \Sigma_k-IND fragments of PA. Limited operators, diagonalization, and majorization functions are not used. PREPRINT

Nucl. Instrum. Methods Phys. Res., A Nucl. Instrum. Methods Phys. Res., A 0167-5087 Position-sensitive Si pad detectors for electron emission channeling experiments Wahl Ulrich Correia J G Czermak Adam Jahn S G Jalocha Pawel Marques J G Rudge Alan Schopper Florian Carvalho-Soares João Vantomme A Weilhammer Peter 2004 524 245 256 Position-sensitive detector systems, initially developed for the detection of X-rays, have been adapted for their use in electron emission channeling experiments. Each detection system consists of a 30.8x30.8 mm$^{2}$ 22x22 -pad Si detector, either of 0.3 mm, 0.5 mm or 1 mm thickness, four 128$-$channel preamplifier chips, a backplane trigger circuit, a sampling analog to digital converter, a digital signal processor, and a personal computer for data display and storage. The operational principle of these detection systems is described, and characteristic features such as energy and position resolution and maximum count rate, which have been determined from tests with conversion electrons and $\beta^-\!$ -particles in the energy range 40--600 keV, are presented. research-article

Phys. Rev. D Phys. Rev. D Mass Spectrum in R-Parity Violating mSUGRA and Benchmark Points Allanach Benjamin C Bernhardt M A Dreiner H K Kom C H Richardson P 2007 75 We investigate in detail the low-energy spectrum of the R-parity violating mSUGRA model using the computer program \texttt{SOFTSUSY}. We impose the experimental constraints from the measurement of the anomalous magnetic moment of the muon, $(g-2)_\mu$, the decay $b\ra s\gamma$ as well as the mass bounds from direct searches at colliders, in particular on the Higgs boson and the lightest chargino. We also include a new calculation for the R parity violating contribution to $\Br(B_s\ra \mu^+\mu^-)$. We then focus on cases where the lightest neutralino is {\em not} the lightest supersymmetric particle (LSP). In this region of parameter space either the lightest scalar tau (stau) or the scalar tau neutrino (tau sneutrino) is the LSP. We suggest four benchmark points with typical spectra and novel collider signatures for detailed phenomenological analysis and simulation by the LHC collaborations. research-article

Adv. Phys. Adv. Phys. Statistical Models of Fracture Alava M J Nukala P K Zapperi S 2006 55 349 476 Disorder and long-range interactions are two of the key components that make material failure an interesting playfield for the application of statistical mechanics. The cornerstone in this respect has been lattice models of the fracture in which a network of elastic beams, bonds or electrical fuses with random failure thresholds are subject to an increasing external load. These models describe on a qualitative level the failure processes of real, brittle or quasi-brittle materials. This has been particularly important in solving the classical engineering problems of material strength: the size dependence of maximum stress and its sample to sample statistical fluctuations. At the same time, lattice models pose many new fundamental questions in statistical physics, such as the relation between fracture and phase transitions. Experimental results point out to the existence of an intriguing crackling noise in the acoustic emission and of self-affine fractals in the crack surface morphology. Recent advances in computer power have enabled considerable progress in the understanding of such models. Among these partly still controversial issues, are the scaling and size effects in material strength and accumulated damage, the statistics of avalanches or bursts of microfailures, and the morphology of the crack surface. Here we present an overview of the results obtained with lattice models for fracture, highlighting the relations with statistical physics theories and more conventional fracture mechanics approaches. research-article

Dynamics in inhomogeneous liquids and glasses via the test particle limit Archer A J Hopkins P Schmidt M 2006 We show that one may view the self and the distinct part of the van Hove dynamic correlation function of a simple fluid as the one-body density distributions of a binary mixture that evolve in time according to dynamical density functional theory. For a test case of soft core Brownian particles the theory yields results for the van Hove function that agree quantitatively with those of our Brownian dynamics computer simulations. At sufficiently high densities the free energy landscape underlying the dynamics exhibits a barrier as a function of the mean particle displacement, shedding new light on the nature of glass formation. For hard spheres confined between parallel planar walls the barrier height oscillates in-phase with the local density, implying that the mobility is maximal between layers, which should be experimentally observable in confined colloidal dispersions. PREPRINT

ECA-LP / ECA-RuleML: A Homogeneous Event-Condition-Action Logic Programming Language Paschke A 2006 Event-driven reactive functionalities are an urgent need in nowadays distributed service-oriented applications and (Semantic) Web-based environments. An important problem to be addressed is how to correctly and efficiently capture and process the event-based behavioral, reactive logic represented as ECA rules in combination with other conditional decision logic which is represented as derivation rules. In this paper we elaborate on a homogeneous integration approach which combines derivation rules, reaction rules (ECA rules) and other rule types such as integrity constraint into the general framework of logic programming. The developed ECA-LP language provides expressive features such as ID-based updates with support for external and self-updates of the intensional and extensional knowledge, transac-tions including integrity testing and an event algebra to define and process complex events and actions based on a novel interval-based Event Calculus variant. PREPRINT

On some winning strategies for the Iterated Prisoner's Dilemma or Mr. Nice Guy and the Cosa Nostra Slany W Kienreich W 2006 We submitted two kinds of strategies to the iterated prisoner's dilemma (IPD) competitions organized by Graham Kendall, Paul Darwen and Xin Yao in 2004 and 2005. Our strategies performed exceedingly well in both years. One type is an intelligent and optimistic enhanced version of the well known TitForTat strategy which we named OmegaTitForTat. It recognizes common behaviour patterns and detects and recovers from repairable mutual defect deadlock situations, otherwise behaving much like TitForTat. The second type consists of a set of strategies working together as a team. These group strategies have one distinguished individual Godfather strategy that plays OmegaTitForTat against non-members while heavily profiting from the behaviour of the other members of his group, the Hitman. The Hitman willingly let themselves being abused by their Godfather while themselves lowering the scores of all other players as much as possible, thus further maximizing the performance of their Godfather in relation to other participants. The study of collusion in the simplified framework of the iterated prisoner's dilemma allows us to draw parallels to many common aspects of reality both in Nature as well as Human Society, and therefore further extends the scope of the iterated prisoner's dilemma as a metaphor for the study of cooperative behaviour in a new and natural direction. We further provide evidence that it will be unavoidable that such group strategies will dominate all future iterated prisoner's dilemma competitions as they can be stealthy camouflaged as non-group strategies with arbitrary subtlety. Moreover, we show that the general problem of recognizing stealth colluding strategies is undecidable in the theoretical sense. PREPRINT

A comparative analysis of the geometrical surface texture of a real and virtual model of a tooth flank of a cylindrical gear Michalski J Skoczylas L 2006 The paper presents the methodology of modelling tooth flanks of cylindrical gears in the Cad environment. The modelling consists in a computer simulation of gear generation. A model of tooth flanks is an envelope curve of a family of envelopes that originate from the rolling motion of a solid tool model in relation to a solid model of the cylindrical gear. The surface stereometry and topography of the tooth flanks, hobbed and chiselled by Fellows method, are compared to their numerical models. Metrological measurements of the real gears were carried out using a coordinated measuring machine and a two - and a three-dimensional profilometer. A computer simulation of the gear generation was performed in the Mechanical Desktop environment. PREPRINT

The Origin of the Decoupling of Oxygen and Silicon Dynamics in Liquid Silica as Expressed by its Potential Energy Landscape Saksaengwijit A Heuer A 2006 The oxygen and silicon dynamics in silica is compared via computer simulations. In agreement with experimental data and previous simulations a decoupling of oxygen and silicon dynamics is observed upon cooling. The origin of this decoupling is studied in the framework of the potential energy landscape. From analysis of the transition features between neighboring superstructures of minima, denoted metabasins, the differences between the oxygen and the silicon dynamics can be quantified. The decoupling can be explicitly related to the presence of generalized rotational processes, giving rise to oxygen but not to silicon displacement. Closer analysis of these processes yields important insight into the nature of the potential energy landscape of silica. The physical picture of relaxation processes in silica, obtained in previous work for the oxygen dynamics, is consistent with the decoupling effects, elucidated here. PREPRINT

J. Phys. Chem. B J. Phys. Chem. B 0092-7325 Microscopic description of the low-temperature anomalies in silica and lithium silicate via computer simulations Reinisch J Heuer A 2006 110 Information about the nature of the low-temperature anomalies and in particular the properties of the tunneling systems in silica and lithium silica glasses are revealed via computer simulations. The potential energy landscape of these systems is systematically explored for adjacent pairs of local minima which may act as double-well potentials (DWP) at low temperatures. Three different types of DWP are distinguished, related to perfectly coordinated silica, intrinsic silica defects, and extrinsic defects. Their properties like the spatial extension and the dipole moment are characterized in detail. Furthermore, the absolute number of tunneling systems, i.e. symmetric DWP, is estimated. The results are compared with dielectric echo, specific heat and acoustic experiments on Suprasil I and Suprasil W. A semi-quantitative agreement for all relevant features is obtained. research-article

Implementation of Grover search algorithm with Josephson charge qubits Zheng X H Dong P Xue Z Y Cao Z L 2006 A scheme for the implementation of Grover search algorithm based on Josephson charge qubits is proposed. The scheme is simple and easily manipulated, because any two charge qubits can be selectively and effectively coupled by a common inductance. More manipulations can be realized before decoherence sets in. All the devices in the scheme are well within the current technology. Moreover, the implementation would be a key step to construct real quantum computer via Josephson charge qubits. PREPRINT

Out-of-equilibrium dynamics in a gaussian trap model Diezemann G 2006 The violations of the fluctuation-dissipation theorem are analyzed for a trap model with a gausssian density of states. In this model, the system reaches thermal equilibrium for long times after a quench to any finite temperature and therefore all aging effect are of a transient nature. For not too long times after the quench it is found that the so-called fluctuation-dissipation ratio tends to a non-trivial limit, thus inicating the possibility for the definition of a time scale dependent effective temperature. However, different definitions of the effective temperature yield distinct results. In particular plots of the integrated response versus the correlation function strongly depend on the way they are constructed. Also the definition of effective temperatures in the frequency domain is not unique for the model considered. This may have some implications for the interpretation of results from computer simulations and experimental determinations of effective temperatures. PREPRINT

Conditional Expressions for Blind Deconvolution: Multi-point form Aogaki S Moritani I Sugai T Takeutchi F Toyama F M 2006 We present conditional expression (CE) for finding blurs convolved in given images. The CE is given in terms of the zero-values of the blurs evaluated at multi-point. The CE can detect multiple blur all at once. We illustrate the multiple blur-detection by using a test image. PREPRINT

Simple method to eliminate blur based on Lane and Bates algorithm Aogaki S Moritani I Sugai T Takeutchi F Toyama F M 2006 A simple search method for finding a blur convolved in a given image is presented. The method can be easily extended to a large blur. The method has been experimentally tested with a model blurred image. PREPRINT

Updates in Answer Set Programming: An Approach Based on Basic Structural Properties Osorio M Cuevas V 2006 We have studied the update operator defined for update sequences by Eiter et al. without tautologies and we have observed that it satisfies an interesting property This property, which we call Weak Independence of Syntax (WIS), is similar to one of the postulates proposed by Alchourron, Gardenfors, and Makinson (AGM); only that in this case it applies to nonmonotonic logic. In addition, we consider other five additional basic properties about update programs and we show that the operator of Eiter et al. satisfies them. This work continues the analysis of the AGM postulates under a refined view that considers nelson logic as a monotonic logic which allows us to expand our understanding of answer sets. Moreover, nelson logic helped us to derive an alternative definition of the operator defined by Eiter et al. avoiding the use of unnecessary extra atoms. PREPRINT

System Merlin 1983 Film of computer screen. Events from UA1 detector PUBLVIDEOMOVIE

Ortho-normal quaternion frames, Lagrangian evolution equations and the three-dimensional Euler equations Gibbon J D 2006 More than 150 years after their invention by Hamilton, quaternions are now widely used in the aerospace and computer animation industries to track the paths of moving objects undergoing three-axis rotations. It is shown here that they provide a natural way of selecting an appropriate ortho-normal frame -- designated the quaternion-frame -- for a particle in a Lagrangian flow, and of obtaining the equations for its dynamics. How these ideas can be applied to the three-dimensional Euler fluid equations is then considered. This work has a bearing on the issue of whether the Euler equations develop a singularity in a finite time. Some of the literature on this topic is reviewed, which includes both the Beale-Kato-Majda theorem and associated work on the direction of vorticity by both Constantin, Fefferman & Majda and Deng, Hou and Yu. It is then shown how the quaternion formulation provides a further direction of vorticity result using the Hessian of the pressure. PREPRINT

Conditional Expressions for Blind Deconvolution: Derivative form Aogaki S Moritani I Sugai T Takeutchi F Toyama F M 2006 We developed novel conditional expressions (CEs) for Lane and Bates' blind deconvolution. The CEs are given in term of the derivatives of the zero-values of the z-transform of given images. The CEs make it possible to automatically detect multiple blur convolved in the given images all at once without performing any analysis of the zero-sheets of the given images. We illustrate the multiple blur-detection by the CEs for a model image PREPRINT

SPS : the control system 1975 <HTML> English version. Part of the series of films produced by CERN about the SPS. "More than 10.000 things to control, 7,00 things to measure and 30,000 ? to survey, distributed over more than 10 square km. That was the problem which faced the controls group."<BR><BR> Comments: images of control room, computer screens, and computer centre rather dark PUBLVIDEOMOVIE

Some examples of proton-antiproton collisions in the UA1 detector 1983 <HTML>Computer screen representations of some examples of proton-antiproton collisions in the UA1 detector. Creation of matter in a soft collision. A two jets event: a typical quark antiquark hard scattering. Production of the w-boson decaying into electron-neutrino. Production of the z-boson and its decay into electron-positron. Production of the z-boson and its decay into two muons.<BR><BR>Comments : silent well done PUBLVIDEOMOVIE

Fast Jacobian group operations for C_{3,4} curves over a large finite field Salem F K A Khuri-Makdisi K 2006 Let C be an arbitrary smooth algebraic curve of genus g over a large finite field K. We revisit fast addition algorithms in the Jacobian of C due to Khuri-Makdisi (math.NT/0409209, to appear in Math. Comp.). The algorithms, which reduce to linear algebra in vector spaces of dimension O(g) once |K| >> g, and which asymptotically require O(g^{2.376}) field operations using fast linear algebra, are shown to perform efficiently even for certain low genus curves. Specifically, we provide explicit formulae for performing the group law on Jacobians of C_{3,4} curves of genus 3. We show that, typically, the addition of two distinct elements in the Jacobian of a C_{3,4} curve requires 117 multiplications and 2 inversions in K, and an element can be doubled using 129 multiplications and 2 inversions in K. This represents an improvement of approximately 20% over previous methods. PREPRINT

On the zero mass limit of tagged particle diffusion in the 1-d Rayleigh-gas Balint P Tóth B Toth P 2006 We consider the M -> 0 limit for tagged particle diffusion in a 1-dimensional Rayleigh-gas, studied originaly by Sinai and Soloveichik (1986), respectively by Szasz and Toth (1986). In this limit we derive a new type of model for tagged paricle diffusion, with Calogero-Moser-Sutherland (i.e. inverse quadratic) interaction potential between the two central particles. Computer simulations on this new model reproduce exactly the numerical value of the limiting variance obtained by Boldrighini, Frigio and Tognetti (2002). PREPRINT

Hawking Colloquium Packed CERN Auditoriums 2006 BULLETINNEWS

Single electron spin and its coherence in Si quantum computer architecture Calderón M J Koiller B Sarma S D 2006 The possibility of performing single spin measurements in Si-based quantum computers through electric field control of electrons bound to double donors near a barrier interface is assessed. We find that both the required electric fields and the tunneling times involved are probably too large for practical implementations. On the other hand, operations with double donors in their first excited state require smaller fields and faster tunneling times, and are therefore suitable for spin-to-charge conversion measurements. We also propose a measurement scheme that would render statistical (ensemble) estimates of the spin coherence at the Si/SiO2 interface. PREPRINT

On the dynamics of spin systems in the Landau-Lifshitz theory Krey U 2006 In the framework of the Landau-Lifshitz equations without any dissipation (an approximation which may also be helpful for finite, but weak Gilbert damping), with all interactions included (specifically always with exchange and magnetic dipole interactions), for general ground states, geometries and domain structures, and many types of effective fields (including contributions from spin currents etc.) the dynamics of the spin precession around the ground state is considered. At first the precession is treated in the linear approximation. For the (small amplitude) eigenmodes of the precession one has a `rule of geometric mean' for the eigenfrequencies. For the eigenmodes orthogonality relations are obtained, which correspond to those known from the Schrodinger equation of quantum mechanics, but are defined locally. Then also some aspects of the nonlinear mode coupling with emphasis on `confluence' and `splitting' processes of elementary magnetic spin-wave excitations are considered. At the same time these processes contribute to the Gilbert damping. There are essential differences to quantum mechanics, although at a first glance one discovers many similarities. From the results one may also get insights of why these systems are so complex that (although the essential quantities depend only on the local values of the partially long-ranged effective magnetic fields) practically only detailed experiments and computer simulations make sense. PREPRINT

NectaRSS, an RSS feed ranking system that implicitly learns user preferences Samper J J Castillo P A Araujo L Merelo J J 2006 In this paper a new RSS feed ranking method called NectaRSS is introduced. The system recommends information to a user based on his/her past choices. User preferences are automatically acquired, avoiding explicit feedback, and ranking is based on those preferences distilled to a user profile. NectaRSS uses the well-known vector space model for user profiles and new documents, and compares them using information-retrieval techniques, but introduces a novel method for user profile creation and adaptation from users' past choices. The efficiency of the proposed method has been tested by embedding it into an intelligent aggregator (RSS feed reader), which has been used by different and heterogeneous users. Besides, this paper proves that the ranking of newsitems yielded by NectaRSS improves its quality with user's choices, and its superiority over other algorithms that use a different information representation method. PREPRINT

Paper to Screen: Processing Historical Scans in the ADS Thompson D M Accomazzi A Eichhorn G Grant C Henneken E Kurtz M J Bohlen E Murray S S 2006 The NASA Astrophysics Data System in conjunction with the Wolbach Library at the Harvard-Smithsonian Center for Astrophysics is working on a project to microfilm historical observatory publications. The microfilm is then scanned for inclusion in the ADS. The ADS currently contains over 700,000 scanned pages of volumes of historical literature. Many of these volumes lack clear pagination or other bibliographic data that are necessary to take advantage of the searching capabilities of the ADS. This paper will address some of the interesting challenges that needed to be resolved during the processing of the Observatory Reports included in the ADS. PREPRINT

LTL with the Freeze Quantifier and Register Automata Demri S Lazic R 2006 Temporal logics, first-order logics, and automata over data words have recently attracted considerable attention. A data word is a word over a finite alphabet, together with a datum (an element of an infinite domain) at each position. Examples include timed words and XML documents. To refer to the data, temporal logics are extended with the freeze quantifier, first-order logics with predicates over the data domain, and automata with registers or pebbles. We investigate relative expressiveness and complexity of standard decision problems for LTL with the freeze quantifier (LTLfq), 2-variable first-order logic (FO2) over data words, and register automata. The only predicate available on data is equality. Previously undiscovered connections among those formalisms, and to counter automata with incrementing errors, enable us to answer several questions left open in recent literature. We show that the future-time fragment of LTLfq which corresponds to FO2 over finite data words can be extended considerably while preserving decidability, but at the expense of non-primitive recursive complexity, and that most of further extensions are undecidable. We also prove that surprisingly, over infinite data words, LTLfq with the `eventually' operator instead of the `until' operator, as well as nonemptiness of one-way universal register automata, are undecidable even when there is only 1 register. PREPRINT

Network calculus based FDI approach for switched Ethernet architecture Brahimi B Aubrun C Rondeau E 2006 The Networked Control Systems (NCS) are complex systems which integrate information provided by several domians such as automatic control, computer science, communication network. The work presented in this paper concerns fault detection, isolation and compensation of communication network. The proposed method is based on the classical approach of Fault Detection and Isolation and Fault Tolerant Control (FDI/FTC) currently used in diagnosis. The modelling of the network to be supervised is based on both couloured petri nets and network calculus theory often used to represent and analyse the network behaviour. The goal is to implement inside network devices algorithms enabling to detect, isolate and compensate communication faults in an autonomous way. PREPRINT

Phys. Rev. Lett. Phys. Rev. Lett. 0031-9007 Salt-induced collapse and reexpansion of highly charged flexible polyelectrolytes Hsiao P Y Luijten E 2006 97 We study the salt-dependent conformations of dilute flexible polyelectrolytes in solution via computer simulations. Low concentrations of multivalent salt induce the known conformational collapse of individual polyelectrolyte chains, but as the salt concentration is increased further this is followed by a reexpansion. We explicitly demonstrate that multivalent counterions can overcompensate the bare charge of the chain in the reexpansion regime. Both the degree of reexpansion and the occurrence of overcharging sensitively depend on ion size. Our findings are relevant for a wide range of salt-induced complexation phenomena. research-article

Force heterogeneities in particle assemblies: From order to disorder Silbert L E 2006 The effect of increasing structural disorder on the distribution of contact forces P(f), inside three dimensional particle assemblies is systematically studied using computer simulations of model granular packings. Starting from a face-centred cubic array, where all contact forces are identical, an increasing number of defects is introduced into the assembly, after which the system is then allowed to relax into a new mechanically stable state. Three distinct protocols for imposing disorder are compared. A quantitative measure of the disorder is obtained from distributions of the coordination number and three-particle contact angle. The distribution of normal contact forces show dramatic qualitative changes with increasing disorder. In the regime where the disorder is relatively weak, the pressure and the lowest normal mode frequency scale approximately linearly in the coordination number, with distance from the crystalline state. These results for P(f) are discussed in the context of jamming phenomena in glassy and granular materials. PREPRINT

Grant boosts Fermi viability Kunz Tona 2006 Fermilab has received a $5.5 million grant that will help ensure the Batavia physics laboratory's future in workd research (1 page) CUTTING

A kernel for time series based on global alignments Cuturi M Vert J P Birkenes O Matsui T 2006 We propose in this paper a new family of kernels to handle times series, notably speech data, within the framework of kernel methods which includes popular algorithms such as the Support Vector Machine. These kernels elaborate on the well known Dynamic Time Warping (DTW) family of distances by considering the same set of elementary operations, namely substitutions and repetitions of tokens, to map a sequence onto another. Associating to each of these operations a given score, DTW algorithms use dynamic programming techniques to compute an optimal sequence of operations with high overall score. In this paper we consider instead the score spanned by all possible alignments, take a smoothed version of their maximum and derive a kernel out of this formulation. We prove that this kernel is positive definite under favorable conditions and show how it can be tuned effectively for practical applications as we report encouraging results on a speech recognition task. PREPRINT

Postinal Determinacy of Games with Infinitely Many Priorities Graedel E Walukiewicz I 2006 We study two-player games of infinite duration that are played on finite or infinite game graphs. A winning strategy for such a game is positional if it only depends on the current position, and not on the history of the play. A game is positionally determined if, from each position, one of the two players has a positional winning strategy. The theory of such games is well studied for winning conditions that are defined in terms of a mapping that assigns to each position a priority from a finite set. Specifically, in Muller games the winner of a play is determined by the set of those priorities that have been seen infinitely often; an important special case are parity games where the least (or greatest) priority occurring infinitely often determines the winner. It is well-known that parity games are positionally determined whereas Muller games are determined via finite-memory strategies. In this paper, we extend this theory to the case of games with infinitely many priorities. Such games arise in several application areas, for instance in pushdown games with winning conditions depending on stack contents. For parity games there are several generalisations to the case of infinitely many priorities. While max-parity games over omega or min-parity games over larger ordinals than omega require strategies with infinite memory, we can prove that min-parity games with priorities in omega are positionally determined. Indeed, it turns out that the min-parity condition over omega is the only infinitary Muller condition that guarantees positional determinacy on all game graphs. PREPRINT

Positional Determinacy of Games with Infinitely Many Priorities Graedel E Walukiewicz I 2006 We study two-player games of infinite duration that are played on finite or infinite game graphs. A winning strategy for such a game is positional if it only depends on the current position, and not on the history of the play. A game is positionally determined if, from each position, one of the two players has a positional winning strategy. The theory of such games is well studied for winning conditions that are defined in terms of a mapping that assigns to each position a priority from a finite set. Specifically, in Muller games the winner of a play is determined by the set of those priorities that have been seen infinitely often; an important special case are parity games where the least (or greatest) priority occurring infinitely often determines the winner. It is well-known that parity games are positionally determined whereas Muller games are determined via finite-memory strategies. In this paper, we extend this theory to the case of games with infinitely many priorities. Such games arise in several application areas, for instance in pushdown games with winning conditions depending on stack contents. For parity games there are several generalisations to the case of infinitely many priorities. While max-parity games over omega or min-parity games over larger ordinals than omega require strategies with infinite memory, we can prove that min-parity games with priorities in omega are positionally determined. Indeed, it turns out that the min-parity condition over omega is the only infinitary Muller condition that guarantees positional determinacy on all game graphs. PREPRINT

Virtual Laboratories Hut P 2006 At the frontier of most areas in science, computer simulations play a central role. The traditional division of natural science into experimental and theoretical investigations is now completely outdated. Instead, theory, simulation, and experimentation form three equally essential aspects, each with its own unique flavor and challenges. Yet, education in computational science is still lagging far behind, and the number of text books in this area is minuscule compared to the many text books on theoretical and experimental science. As a result, many researchers still carry out simulations in a haphazard way, without properly setting up the computational equivalent of a well equipped laboratory. The art of creating such a virtual laboratory, while providing proper extensibility and documentation, is still in its infancy. A new approach is described here, Open Knowledge, as an extension of the notion of Open Source software. Besides open source code, manuals, and primers, an open knowledge project provides simulated dialogues between code developers, thus sharing not only the code, but also the motivations behind the code. PREPRINT

Spenden mit BOINC Banse Phillip 2006 Software platform organiser computing time from private PCs CUTTING

Gaussian hypergeometric series and extensions of supercongruences Osburn R Schneider C 2006 Let p be an odd prime. The purpose of this paper is to refine methods of Ahlgren and Ono and Kilbourn in order to prove a general mod p^3 congruence for the Gaussian hypergeometric series {}_{n+1}F_{n}(\lambda) where n is an odd positive integer. As a result, we extend three recent supercongruences. The first is a result of Ono and Ahlgren on a supercongruence for Ap{\'e}ry numbers which was conjectured by Beukers in 1987. The second is one of Mortenson which relates truncated hypergeometric series to the number of F_{p} points of some family of Calabi-Yau manifolds. Finally, the third is a result of Loh and Rhodes on congruences between coefficients of modular forms corresponding to a particular class of elliptic curves and combinatorial objects. Additionally, we discuss the non-trivial methods of the computer summation package Sigma which were used to find explicit evaluations of two strange combinatorial identities involving generalized Harmonic sums. PREPRINT

Church's thesis is questioned by new calculation paradigm Hutzelmeyer H 2006 Church's thesis claims that all effecticely calculable functions are recursive. A shortcoming of the various definitions of recursive functions lies in the fact that it is not a matter of a syntactical check to find out if an entity gives rise to a function. Eight new ideas for a precise setup of arithmetical logic and its metalanguage give the proper environment for the construction of a special computer, the ARBACUS computer. Computers do not come to a necessary halt; it is requested that calculators are constructed on the basis of computers in a way that they always come to a halt, then all calculations are effective. The ARBATOR is defined as a calculator with two-layer-computation. It allows for the calculation of all primitive recursive functions, but multi-level-arbation also allows for the calculation of other arbative functions that are not primitive recursive. The new paradigm of calculation does not have the above mentioned shortcoming. The defenders of Church's thesis are challenged to show that exotic arbative functions are recursive and to put forward a recursive function that is not arbative. A construction with three-tier-multi-level-arbation that includes a diagonalisation leads to the extravagant yet calculable Snark-function that is not arbative. As long as it is not shown that all exotic arbative functions and particularily the Snark-function are arithmetically representable Goedel's first incompleteness sentence is in limbo. PREPRINT

PoS PoS Simulating at Realistic Quark Masses: Pseudoscalar Decay Constants and Chiral Logarithms Göckeler M Horsley R Nakamura Y Pleiter D Rakow P E L Schierholz G Schroers W Streuer T Stüben H Zanotti J M 2006 LAT2006 Due to improvements in computer performance and algorithms, the rapidly increasing cost for unquenched Wilson-type fermions with lighter quarks has been ameliorated and new simulations are now possible. Here we present results using two flavours of O(a)-improved Wilson fermions for meson decay constants at pseudoscalar masses down to 320MeV. Results are at several lattice spacings down to about 0.07fm and include a non-perturbative determination of the renormalisation constant. This enables us to attempt contact with (partially quenched) chiral perturbation theory. research-article

Enumeration Problems Related to Ground Horn Theories Dershowitz N Harris M A Huang G S 2006 We investigate the enumeration of varieties of boolean theories related to Horn clauses. We describe a number of combinatorial equivalences among different characterizations and calculate the number of different theories in $n$ variables for slightly different characterizations. The method of counting is via counting models using a satisfiability checker. PREPRINT

Creation and pinning of vortex-antivortex pairs Kim S Hu C R Andrews M J 2006 Computer modeling is reported about the creation and pinning of a magnetic vortex-antivortex (V-AV) pair in a superconducting thin film, due to the magnetic field of a vertical magnetic dipole above the film, and two antidot pins inside the film. For film thickness $= 0.1\xi$, $\kappa = 2$, and no pins, we find the film carries two V-AV pairs at steady state in the imposed flux range $2.10\Phi_0 < \Phi^+ < 3.0\Phi_0$, and no pairs below. With two antidot pins suitably introduced into the film, a single V-AV pair can be stable in the film for $\Phi^+ \ge 1.3\Phi_0$. At pin separation $\ge 17\xi$, we find the V-AV pair remains pinned after the dipole field is removed, and, so can represent a 1 for a nonvolatile memory. PREPRINT

Comparing Typical Opening Move Choices Made by Humans and Chess Engines Levene M Bar-Ilan J 2006 The opening book is an important component of a chess engine, and thus computer chess programmers have been developing automated methods to improve the quality of their books. For chess, which has a very rich opening theory, large databases of high-quality games can be used as the basis of an opening book, from which statistics relating to move choices from given positions can be collected. In order to find out whether the opening books used by modern chess engines in machine versus machine competitions are ``comparable'' to those used by chess players in human versus human competitions, we carried out analysis on 26 test positions using statistics from two opening books one compiled from humans' games and the other from machines' games. Our analysis using several nonparametric measures, shows that, overall, there is a strong association between humans' and machines' choices of opening moves when using a book to guide their choices. PREPRINT

Camera motion estimation through planar deformation determination Jonchery C Koepfler G 2006 In this paper, we propose a global method for estimating the motion of a camera which films a static scene. Our approach is direct, fast and robust, and deals with adjacent frames of a sequence. It is based on a quadratic approximation of the deformation between two images, in the case of a scene with constant depth in the camera coordinate system. This condition is very restrictive but we show that provided translation and depth inverse variations are small enough, the error on optical flow involved by the approximation of depths by a constant is small. In this context, we propose a new model of camera motion, that allows to separate the image deformation in a similarity and a ``purely'' projective application, due to change of optical axis direction. This model leads to a quadratic approximation of image deformation that we estimate with an M-estimator; we can immediatly deduce camera motion parameters. PREPRINT

Extending the Calculus of Constructions with Tarski's fix-point theorem Bertot Y 2006 We propose to use Tarski's least fixpoint theorem as a basis to define recursive functions in the calculus of inductive constructions. This widens the class of functions that can be modeled in type-theory based theorem proving tool to potentially non-terminating functions. This is only possible if we extend the logical framework by adding the axioms that correspond to classical logic. We claim that the extended framework makes it possible to reason about terminating and non-terminating computations and we show that common facilities of the calculus of inductive construction, like program extraction can be extended to also handle the new functions. PREPRINT

A type-based termination criterion for dependently-typed higher-order rewrite systems Blanqui F 2006 Several authors devised type-based termination criteria for ML-like languages allowing non-structural recursive calls. We extend these works to general rewriting and dependent types, hence providing a powerful termination criterion for the combination of rewriting and beta-reduction in the Calculus of Constructions. PREPRINT

The Calculus of Algebraic Constructions Blanqui F Jouannaud J P Okada M 2006 This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalizes inductive types equipped with higher-order primitive recursion, by providing definitions of functions by pattern-matching which capture recursor definitions for arbitrary non-dependent and non-polymorphic inductive types satisfying a strictly positivity condition. CAC also generalizes the first-order framework of abstract data types by providing dependent types and higher-order rewrite rules. PREPRINT

Termination and Confluence of Higher-Order Rewrite Systems Blanqui F 2006 In the last twenty years, several approaches to higher-order rewriting have been proposed, among which Klop's Combinatory Rewrite Systems (CRSs), Nipkow's Higher-order Rewrite Systems (HRSs) and Jouannaud and Okada's higher-order algebraic specification languages, of which only the last one considers typed terms. The later approach has been extended by Jouannaud, Okada and the present author into Inductive Data Type Systems (IDTSs). In this paper, we extend IDTSs with the CRS higher-order pattern-matching mechanism, resulting in simply-typed CRSs. Then, we show how the termination criterion developed for IDTSs with first-order pattern-matching, called the General Schema, can be extended so as to prove the strong normalization of IDTSs with higher-order pattern-matching. Next, we compare the unified approach with HRSs. We first prove that the extended General Schema can also be applied to HRSs. Second, we show how Nipkow's higher-order critical pair analysis technique for proving local confluence can be applied to IDTSs. PREPRINT

Definitions by Rewriting in the Calculus of Constructions Blanqui F 2006 The main novelty of this paper is to consider an extension of the Calculus of Constructions where predicates can be defined with a general form of rewrite rules. We prove the strong normalization of the reduction relation generated by the beta-rule and the user-defined rules under some general syntactic conditions including confluence. As examples, we show that two important systems satisfy these conditions: a sub-system of the Calculus of Inductive Constructions which is the basis of the proof assistant Coq, and the Natural Deduction Modulo a large class of equational theories. PREPRINT

Inductive-data-type Systems Blanqui F Jouannaud J P Okada M 2006 In a previous work (``Abstract Data Type Systems'', TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-calculus enriched by pattern-matching definitions following a certain format, called the ``General Schema'', which generalizes the usual recursor definitions for natural numbers and similar ``basic inductive types''. This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called ``strictly positive'', and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types. PREPRINT

Type theory and rewriting Blanqui F 2006 We study the properties, in particular termination, of dependent types systems for lambda calculus and rewriting. PREPRINT

An Isabelle formalization of protocol-independent secrecy with an application to e-commerce Blanqui F 2006 A protocol-independent secrecy theorem is established and applied to several non-trivial protocols. In particular, it is applied to protocols proposed for protecting the computation results of free-roaming mobile agents doing comparison shopping. All the results presented here have been formally proved in Isabelle by building on Larry Paulson's inductive approach. This therefore provides a library of general theorems that can be applied to other protocols. PREPRINT

Inductive types in the Calculus of Algebraic Constructions Blanqui F 2006 In a previous work, we proved that almost all of the Calculus of Inductive Constructions (CIC), which is the basis of the proof assistant Coq, can be seen as a Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In this paper, we not only prove that CIC as a whole can be seen as a CAC, but also that it can be extended with non-free constructors, pattern-matching on defined symbols, non-strictly positive types and inductive-recursive types. PREPRINT

Rewriting modulo in Deduction modulo Blanqui F 2006 We study the termination of rewriting modulo a set of equations in the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In a previous work, we defined general syntactic conditions based on the notion of computable closure for ensuring the termination of the combination of rewriting and beta-reduction. Here, we show that this result is preserved when considering rewriting modulo a set of equations if the equivalence classes generated by these equations are finite, the equations are linear and satisfy general syntactic conditions also based on the notion of computable closure. This includes equations like associativity and commutativity, and provides an original treatment of termination modulo equations. PREPRINT

Volunteer computing to study malaria's spread Brahic Catherine 2006 "Computer owners around the world are being encouraged to lend some of their PC power to an experiment on the spread of malaria in Africa." (1/2 page) CUTTING

Editing, publishing, and computer technology Butler Sharon Stoneman Wiliam P 2006 BOOK

Napieralski Andrzej Ciota Zygmunt Martinez Augustin De Mey Gilbert Cabestany Joan 1998 BOOK

Are polymer melts "ideal"? Wittmer J P Beckrich P Crevel F Huang C C Cavallo A Kreer T Meyer H 2006 It is commonly accepted that in concentrated solutions or melts high-molecular weight polymers display random-walk conformational properties without long-range correlations between subsequent bonds. This absence of memory means, for instance, that the bond-bond correlation function, $P(s)$, of two bonds separated by $s$ monomers along the chain should exponentially decay with $s$. Presenting numerical results and theoretical arguments for both monodisperse chains and self-assembled (essentially Flory size-distributed) equilibrium polymers we demonstrate that some long-range correlations remain due to self-interactions of the chains caused by the chain connectivity and the incompressibility of the melt. Suggesting a profound analogy with the well-known long-range velocity correlations in liquids we find, for instance, $P(s)$ to decay algebraically as $s^{-3/2}$. Our study suggests a precise method for obtaining the statistical segment length \bstar in a computer experiment. PREPRINT

Light Computing Chalmers G 2006 A configuration of light pulses is generated, together with emitters and receptors, that allows computing. The computing is extraordinarily high in number of flops per second, exceeding the capability of a quantum computer for a given size and coherence region. The emitters and receptors are based on the quantum diode, which can emit and detect individual photons with high accuracy. PREPRINT

Non-Uniform Comparison of Notions for Closed Set Computability of Fixed Cardinality with Applications to Singular Coverings Ziegler M 2006 The empty set of course contains no computable point. On the other hand, surprising results due to Zaslavskii, Tseitin, Kreisel, and Lacombe assert the existence of NON-empty co-r.e. closed sets devoid of computable points: sets which are `large' in the sense of positive Lebesgue measure. We observe that a certain size is in fact necessary: every non-empty co-r.e. closed real set of cardinality less than the continuum does contain a computable point. More generally, the present note exhibits a comparison of different notions of computability for closed real subsets non-uniformly, that is, once their cardinality is fixed. PREPRINT

Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages Birkedal L Torp-Smith N Yang H 2006 We show how to give a coherent semantics to programs that are well-specified in a version of separation logic for a language with higher types: idealized algol extended with heaps (but with immutable stack variables). In particular, we provide simple sound rules for deriving higher-order frame rules, allowing for local reasoning. PREPRINT

Symbolic Simulation-Checking of Dense-Time Systems Wang F 2006 Intuitively, an (implementation) automata is simulated by a (specification) automata if every externally observable transition by the implementation automata can also be made by the specification automata. In this work, we present a symbolic algorithm for the simulation-checking of timed automatas. We first present a simulation-checking procedure that operates on state spaces, representable with convex polyhedra, of timed automatas. We then present techniques to represent those intermediate result convex polyhedra with zones and make the procedure an algorithm. We then discuss how to handle Zeno states in the implementation automata. Finally, we have endeavored to realize the algorithm and report the performance of our algorithm in the experiment. PREPRINT

Investigation of possibility of creation of a superconductor quantum register Burlakov A A Gurtovoi V L Dubonos S V Nikulov A V Tulin V A 2006 Multiple and single measurements of quantum states of mesoscopic superconducting loops are carried out in order to investigate a possibility of macroscopic quantum superposition and of creation of a superconductor quantum register. Asymmetric superconducting rings are used in order to be convinced that single measurement gives result corresponding to one of permitted states and multiple one gives an average value on these states. We have measured magnetic dependencies of resistance, rectified voltage and critical current on these rings. The observed quantum oscillations of the resistance and the rectified voltage, corresponding to multiple measurement of quantum states, give evidence of two permitted states at the magnetic flux inside the ring divisible by half of the flux quantum. But the observed quantum oscillations of the critical current, corresponding to single measurement, not only does not confirm these two quantum states, but are in a direct contradiction with the observed oscillations of the resistance. It is assumed that the observed contradiction between the results of measurements made on the same ring can testify to violation of the principle of realism on the mesoscopic level that is a necessary condition for an opportunity of creation of a quantum computer. PREPRINT

Solution of a Problem of Barendregt on Sensible \lambda-Theories Intrigila B Statman R 2006 H is the theory extending \beta-conversion by identifying all closed unsolvables. H\omega is the closure of this theory under the \omega-rule (and \beta-conversion). A long-standing conjecture of H. Barendregt states that the provable equations of H\omega form a \Pi_{1}^{1}-complete set. Here we prove that conjecture. PREPRINT

Comput. Phys. Commun. Comput. Phys. Commun. PROCRUSTES: A computer algebra package for post-Newtonian calculations in General Relativity Puetzfeld D 2006 175 497 508 We report on a package of routines for the computer algebra system Maple which supports the explicit determination of the geometric quantities, field equations, equations of motion, and conserved quantities of General Relativity in the post-Newtonian approximation. The package structure is modular and allows for an easy modification by the user. The set of routines can be used to verify hand calculations or to generate the input for further numerical investigations. research-article

Macromolecules Macromolecules Field - Driven Translocation of Regular Block Copolymers through a Selective Liquid - Liquid Interface Corsi A Milchev A Rostiashvili V G Vilgis T A 2006 39 7115 7124 We propose a simple scaling theory describing the variation of the mean first passage time (MFPT) $\tau(N,M)$ of a regular block copolymer of chain length $N$ and block size $M$ which is dragged through a selective liquid-liquid interface by an external field $B$. The theory predicts a non-Arrhenian $\tau$ vs. $B$ relationship which depends strongly on the size of the blocks, $M$, and rather weakly on the total polymer length, $N$. The overall behavior is strongly influenced by the degree of selectivity between the two solvents $\chi$. The variation of $\tau(N,M)$ with $N$ and $M$ in the regimes of weak and strong selectivity of the interface is also studied by means of computer simulations using a dynamic Monte Carlo coarse-grained model. Good qualitative agreement with theoretical predictions is found. The MFPT distribution is found to be well described by a $\Gamma$ - distribution. Transition dynamics of ring- and telechelic polymers is also examined and compared to that of the linear chains. The strong sensitivity of the ``capture'' time $\tau(N,M)$ with respect to block length $M$ suggests a possible application as a new type of chromatography designed to separate and purify complex mixtures with different block sizes of the individual macromolecules. research-article

Point Estimation of States of Finite Quantum Systems Petz D Hangos K M Magyar A 2006 The estimation of the density matrix of a $k$-level quantum system is studied when the parametrization is given by the real and imaginary part of the entries and they are estimated by independent measurements. It is established that the properties of the estimation procedure depend very much on the invertibility of the true state. In particular, in case of a pure state the estimation is less efficient. Moreover, several estimation schemes are compared for the unknown state of a qubit when one copy is measured at a time. It is shown that the average mean quadratic error matrix is the smallest if the applied observables are complementary. The results are illustrated by computer simulations. PREPRINT

J. Phys. A J. Phys. A Grover's algorithm on a Feynman computer De Falco D Tamascelli D 2004 37 909 930 We present an implementation of Grover's algorithm in the framework of Feynman's cursor model of a quantum computer. The cursor degrees of freedom act as a quantum clocking mechanism, and allow Grover's algorithm to be performed using a single, time-independent Hamiltonian. We examine issues of locality and resource usage in implementing such a Hamiltonian. In the familiar language of Heisenberg spin-spin coupling, the clocking mechanism appears as an excitation of a basically linear chain of spins, with occasional controlled jumps that allow for motion on a planar graph: in this sense our model implements the idea of "timing" a quantum algorithm using a continuous-time random walk. In this context we examine some consequences of the entanglement between the states of the input/output register and the states of the quantum clock. research-article

On the Behavior of Journal Impact Factor Rank-Order Distribution Mansilla R Cocho G Miramontes P 2006 An empirical law for the rank-order behavior of journal impact factors is found. Unlike Zipf's and Lavalette's laws the result is not based on frequencies, but rather in the original impact factor figures. Using an extensive data base on impact factors including journals on Education, Agrosciences, Geosciences, Biosciences and Environ- mental, Chemical, Computer, Engineering, Material, Mathematical, Medical and Physical Sciences we have found extremely good fits out- performing other rank-order models. Some extensions to other areas of knowledge are discussed. PREPRINT

The logic of ontic and epistemic change van Ditmarsch H P Kooi B P 2006 We propose an epistemic logic incorporating dynamic operators to describe information changing events, both informative actions, where agents become more informed about the non-changing state of the world, as ontic changes, wherein the world and the facts describing it change themselves as well. A complete axiomatisation is provided. There are some independent semantic results, for example that assignments in programs can be restricted to those to false or true only. We apply the logic to model systems for card deals and to model protocols PREPRINT

Characterizing Solution Concepts in Games Using Knowledge-Based Programs Halpern J Y Moses Y 2006 We show how solution concepts in games such as Nash equilibrium, correlated equilibrium, rationalizability, and sequential equilibrium can be given a uniform definition in terms of \emph{knowledge-based programs}. Intuitively, all solution concepts are implementations of two knowledge-based programs, one appropriate for games represented in normal form, the other for games represented in extensive form. These knowledge-based programs can be viewed as embodying rationality. The representation works even if (a) information sets do not capture an agent's knowledge, (b) uncertainty is not represented by probability, or (c) the underlying game is not common knowledge. PREPRINT

Quantum computers based on electron spins controlled by ultra-fast, off-resonant, single optical pulses Clark S M Fu K M C Ladd T D Yamamoto Y 2006 We describe a quantum computer operating at a 100 GHz clock frequency based on optically controlled electron spins in quantum dots. In contrast to ESR quantum computers based on narrow-band resonant microwave/RF control fields, this scheme employs broad-band optical pulses as control signals, and the arrival timing of those pulses provides a clock signal to the system. We demonstrate the feasibility of high fidelity single-qubit gates in charged quantum dots with operation times shorter than the inverse Zeeman frequency. Non-local, two-qubit gates may also be realized with similarly fast optical pulses in this system if each quantum dot is contained in a moderate-Q microcavity which is overcoupled to a common, low-loss waveguide. PREPRINT

Nouveau record pour la plus grande grille de calcul scientifique du monde à Genève Tesnier Gregory 2006 CERN is more than happy: EGEE project, a powerful calculation tool, is still growing. The "computer grid" invades new spaces and perspectives are delightful. (1 page) CUTTING

On measurement-based quantum computation with the toric code states Bravyi S B Raussendorf R 2006 We study measurement-based quantum computation (MQC) using as quantum resource the planar code state on a two-dimensional square lattice (planar analogue of the toric code). It is shown that MQC with the planar code state can be efficiently simulated on a classical computer if at each step of MQC the sets of measured and unmeasured qubits correspond to connected subsets of the lattice. PREPRINT

Instant Computing - A New Computation Paradigm Thomann H R 2006 Voltage peaks on a conventional computer's power lines allow for the well-known dangerous DPA attacks. We show that measurement of a quantum computer's transient state during a computational step reveals information about a complete computation of arbitrary length, which can be extracted by repeated probing, if the computer is suitably programmed. Instant computing, as we name this mode of operation, recognizes for any total or partial recursive function arguments lying in the domain of definition and yields their function value with arbitrary small error probability in probabilistic linear time. This implies recognition of (not necessarily recursively enumerable) complements of recursively enumerable sets and the solution of the halting problem. Future quantum computers are shown to be likely to allow for instant computing, and some consequences are pointed out. PREPRINT

Quantifier elimination for the reals with a predicate for the powers of two Avigad J Yin Y 2006 In 1985, van den Dries showed that the theory of the reals with a predicate for the integer powers of two admits quantifier elimination in an expanded language, and is hence decidable. He gave a model-theoretic argument, which provides no apparent bounds on the complexity of a decision procedure. We provide a syntactic argument that yields a procedure that is primitive recursive, although not elementary. In particular, we show that it is possible to eliminate a single block of existential quantifiers in time $2^0_{O(n)}$, where $n$ is the length of the input formula and $2_k^x$ denotes $k$-fold iterated exponentiation. PREPRINT