Search

The half-life of $^{19}$Ne has been measured using a real-time digital multiparametric acquisition system providing an accurate time-stamp and relevant information on the detectors signals for each decay event. An exhaustive offline analysis of the data gave unique access to experimental effects potentially biasing the measurement. After establishing the influence factors impacting the measurement such as after-pulses, pile-up, gain and base line fluctuations, their effects were accurately estimated and the event selection optimized. The resulting half-life, $17.2569\pm0.0019_{(stat)}\pm0.0009_{(syst)}$~s, is the most precise up to now for $^{19}$Ne. It is found in agreement with two recent precise measurements and not consistent with the most recent one [L.J. Broussard {\it et al.}, Phys. Rev. Lett. {\bf112}, 212301 (2014)] by 3.0 standard deviations. The full potential of the technique for nuclei with half-lives of a few seconds is discussed., Comment: 11 pages, 16 figures

In monocular vision systems, lack of knowledge about metric distances caused by the inherent scale ambiguity can be a strong limitation for some applications. We offer a method for fusing inertial measurements with monocular odometry or tracking to estimate metric distances in inertial-monocular systems and to increase the rate of pose estimates. As we performed the fusion in a loosely-coupled manner, each input block can be easily replaced with one's preference, which makes our method quite flexible. We experimented our method using the ORB-SLAM algorithm for the monocular tracking input and Euler forward integration to process the inertial measurements. We chose sets of data recorded on UAVs to design a suitable system for flying robots.

The Relative Pose based Redundancy Removal(RPRR) scheme is presented, which has been designed for mobile RGB-D sensor networks operating under bandwidth-constrained operational scenarios. Participating sensor nodes detect the redundant visual and depth information to prevent their transmission leading to a significant improvement in wireless channel usage efficiency and power savings. Experimental results show that wireless channel utilization is improved by 250% and battery consumption is halved when the RPRR scheme is used instead of sending the sensor images independently.

We formalize and analyze a new problem in formal language theory termed control improvisation. Given a specification language, the problem is to produce an improviser, a probabilistic algorithm that randomly generates words in the language, subject to two additional constraints: the satisfaction of a quantitative soft constraint, and the exhibition of a specified amount of randomness. Control improvisation has many applications, including for example systematically generating random test vectors satisfying format constraints or preconditions while being similar to a library of seed inputs. Other applications include robotic surveillance, machine improvisation of music, and randomized variants of the supervisory control problem. We describe a general framework for solving the control improvisation problem, and use it to give efficient algorithms for several practical classes of instances with finite automaton and context-free grammar specifications. We also provide a detailed complexity analysis, establishing #P-hardness of the problem in many other cases. For these intractable cases, we show how symbolic techniques based on Boolean satisfiability (SAT) solvers can be used to find approximate solutions. Finally, we discuss an extension of control improvisation to multiple soft constraints that is useful in some applications., Comment: 25 pages. Submitted to JACM. This article supersedes arXiv:1411.0698

Recent attempts to explain the effectiveness of Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) on large industrial benchmarks have focused on the concept of community structure. Specifically, industrial benchmarks have been empirically found to have good community structure, and experiments seem to show a correlation between such structure and the efficiency of CDCL. However, in this paper we establish hardness results suggesting that community structure is not sufficient to explain the success of CDCL in practice. First, we formally characterize a property shared by a wide class of metrics capturing community structure, including "modularity". Next, we show that the SAT instances with good community structure according to any metric with this property are still NP-hard. Finally, we study a class of random instances generated from the "pseudo-industrial" community attachment model of Gir\'aldez-Cru and Levy. We prove that, with high probability, instances from this model that have relatively few communities but are still highly modular require exponentially long resolution proofs and so are hard for CDCL. We also present experimental evidence that our result continues to hold for instances with many more communities. This indicates that actual industrial instances easily solved by CDCL may have some other relevant structure not captured by the community attachment model., Comment: 23 pages. Full version of a SAT 2016 paper

The characteristics and performance of a Dual Position Sensitive Multi-Wire Proportional Counter (DPS-MWPC) used to measure the scattering angle, interaction position on the target and the velocity of reaction products, detected in the VAMOS++ magnetic spectrometer, are reported. The detector consists of a pair of position sensitive low pressure MWPCs and provides both fast timing signals, along with the two-dimensional position coordinates required to define the trajectory of the reaction products. A time-of-flight resolution of 305(11) ps (FWHM) was measured. The measured resolutions (FWHM) were 2.5(3) mrad and 560(70) {\mu}m for the scattering angle and the interaction point at the target respectively. The subsequent improvement of the Doppler correction of the energy of the gamma-rays, detected in the gamma-ray tracking array AGATA in coincidence with isotopically identified ions in VAMOS++, is also discussed., Comment: Accepted for publication in Nuclear Inst. and Methods in Physics Research, A

Constrained sampling and counting are two fundamental problems in artificial intelligence with a diverse range of applications, spanning probabilistic reasoning and planning to constrained-random verification. While the theory of these problems was thoroughly investigated in the 1980s, prior work either did not scale to industrial size instances or gave up correctness guarantees to achieve scalability. Recently, we proposed a novel approach that combines universal hashing and SAT solving and scales to formulas with hundreds of thousands of variables without giving up correctness guarantees. This paper provides an overview of the key ingredients of the approach and discusses challenges that need to be overcome to handle larger real-world instances., Comment: Appears in proceedings of AAAI-16 Workshop on Beyond NP

We consider the problem of generating randomized control sequences for complex networked systems typically actuated by human agents. Our approach leverages a concept known as control improvisation, which is based on a combination of data-driven learning and controller synthesis from formal specifications. We learn from existing data a generative model (for instance, an explicit-duration hidden Markov model, or EDHMM) and then supervise this model in order to guarantee that the generated sequences satisfy some desirable specifications given in Probabilistic Computation Tree Logic (PCTL). We present an implementation of our approach and apply it to the problem of mimicking the use of lighting appliances in a residential unit, with potential applications to home security and resource management. We present experimental results showing that our approach produces realistic control sequences, similar to recorded data based on human actuation, while satisfying suitable formal requirements., Comment: to appear in Proceedings of the 1st IEEE Conference on Internet-of-Things Design and Implementation (IoTDI'16)

Road detection is a fundamental task in autonomous navigation systems. In this paper, we consider the case of monocular road detection, where images are segmented into road and non-road regions. Our starting point is the well-known machine learning approach, in which a classifier is trained to distinguish road and non-road regions based on hand-labeled images. We proceed by introducing the use of "contextual blocks" as an efficient way of providing contextual information to the classifier. Overall, the proposed methodology, including its image feature selection and classifier, was conceived with computational cost in mind, leaving room for optimized implementations. Regarding experiments, we perform a sensible evaluation of each phase and feature subset that composes our system. The results show a great benefit from using contextual blocks and demonstrate their computational efficiency. Finally, we submit our results to the KITTI road detection benchmark achieving scores comparable with state of the art methods.

We demonstrate that the formation of negative hydrogen ions (H-) occurs in a wide class of atomic and molecular collisions. In our experiments, H- emission from hydroxyl cations and acetone molecules was observed in keV-energy collisions. We show that hydride (H-) anions are formed via direct collisional fragmentation of molecules, followed by electron grabbing by fast hydrogen fragments. Such general mechanism in hydrogen-containing molecules may significantly influence reaction networks in planetary atmospheres and astrophysical media and new reaction pathways may have to be added in radiolysis studies.

We formalize and analyze a new automata-theoretic problem termed control improvisation. Given an automaton, the problem is to produce an improviser, a probabilistic algorithm that randomly generates words in its language, subject to two additional constraints: the satisfaction of an admissibility predicate, and the exhibition of a specified amount of randomness. Control improvisation has multiple applications, including, for example, generating musical improvisations that satisfy rhythmic and melodic constraints, where admissibility is determined by some bounded divergence from a reference melody. We analyze the complexity of the control improvisation problem, giving cases where it is efficiently solvable and cases where it is #P-hard or undecidable. We also show how symbolic techniques based on Boolean satisfiability (SAT) solvers can be used to approximately solve some of the intractable cases., Comment: 16 pages. Full version of an FSTTCS 2015 paper. This article is superseded by arXiv:1704.06319

Quantitative program analysis involves computing numerical quantities about individual or collections of program executions. An example of such a computation is quantitative information flow analysis, where one estimates the amount of information leaked about secret data through a program's output channels. Such information can be quantified in several ways, including channel capacity and (Shannon) entropy. In this paper, we formalize a class of quantitative analysis problems defined over a weighted control flow graph of a loop-free program. These problems can be solved using a combination of path enumeration, SMT solving, and model counting. However, existing methods can only handle very small programs, primarily because the number of execution paths can be exponential in the program size. We show how path explosion can be mitigated in some practical cases by taking advantage of special branching structure and by novel algorithm design. We demonstrate our techniques by computing the channel capacities of the timing side-channels of two programs with extremely large numbers of paths., Comment: Full version of an SMT 2014 paper

Given a CNF formula and a weight for each assignment of values to variables, two natural problems are weighted model counting and distribution-aware sampling of satisfying assignments. Both problems have a wide variety of important applications. Due to the inherent complexity of the exact versions of the problems, interest has focused on solving them approximately. Prior work in this area scaled only to small problems in practice, or failed to provide strong theoretical guarantees, or employed a computationally-expensive maximum a posteriori probability (MAP) oracle that assumes prior knowledge of a factored representation of the weight distribution. We present a novel approach that works with a black-box oracle for weights of assignments and requires only an {\NP}-oracle (in practice, a SAT-solver) to solve both the counting and sampling problems. Our approach works under mild assumptions on the distribution of weights of satisfying assignments, provides strong theoretical guarantees, and scales to problems involving several thousand variables. We also show that the assumptions can be significantly relaxed while improving computational efficiency if a factored representation of the weights is known., Comment: This is a full version of AAAI 2014 paper

We consider the problem of determining, given x, y in Z^k and a finite set F of affine functions on Z^k, whether y is reachable from x by applying the functions F. We also consider the analogous problem over N^k. These problems are known to be undecidable for k >= 2. We give 2-EXPTIME algorithms for both problems in the remaining case k = 1. The exact complexities remain open, although we show a simple NP lower bound., Comment: 13 pages

We report on direct time-of-flight based mass measurements of 16 light neutron-rich nuclei. These include the first determination of the masses of the Borromean drip-line nuclei $^{19}$B, $^{22}$C and $^{29}$F as well as that of $^{34}$Na. In addition, the most precise determinations to date for $^{23}$N and $^{31}$Ne are reported. Coupled with recent interaction cross-section measurements, the present results support the occurrence of a two-neutron halo in $^{22}$C, with a dominant $\nu2s_{1/2}^2$ configuration, and a single-neutron halo in $^{31}$Ne with the valence neutron occupying predominantly the 2$p_{3/2}$ orbital. Despite a very low two-neutron separation energy the development of a halo in $^{19}$B is hindered by the 1$d_{5/2}^2$ character of the valence neutrons., Comment: 5 pages

Taking into account the drivers' state is a major challenge for designing new advanced driver assistance systems. In this paper we present a driver assistance system strongly coupled to the user. DAARIA 1 stands for Driver Assistance by Augmented Reality for Intelligent Automobile. It is an augmented reality interface powered by several sensors. The detection has two goals: one is the position of obstacles and the quantification of the danger represented by them. The other is the driver's behavior. A suitable visualization metaphor allows the driver to perceive at any time the location of the relevant hazards while keeping his eyes on the road. First results show that our method could be applied to a vehicle but also to aerospace, fluvial or maritime navigation.