Search

This paper tackles the challenges of implementing few-shot learning on embedded systems, specifically FPGA SoCs, a vital approach for adapting to diverse classification tasks, especially when the costs of data acquisition or labeling prove to be prohibitively high. Our contributions encompass the development of an end-to-end open-source pipeline for a few-shot learning platform for object classification on a FPGA SoCs. The pipeline is built on top of the Tensil open-source framework, facilitating the design, training, evaluation, and deployment of DNN backbones tailored for few-shot learning. Additionally, we showcase our work's potential by building and deploying a low-power, low-latency demonstrator trained on the MiniImageNet dataset with a dataflow architecture. The proposed system has a latency of 30 ms while consuming 6.2 W on the PYNQ-Z1 board.

Cosmological parameters encoding our understanding of the expansion history of the Universe can be constrained by the accurate estimation of time delays arising in gravitationally lensed systems. We propose TD-CARMA, a Bayesian method to estimate cosmological time delays by modelling the observed and irregularly sampled light curves as realizations of a Continuous Auto-Regressive Moving Average (CARMA) process. Our model accounts for heteroskedastic measurement errors and microlensing, an additional source of independent extrinsic long-term variability in the source brightness. The semi-separable structure of the CARMA covariance matrix allows for fast and scalable likelihood computation using Gaussian Process modeling. We obtain a sample from the joint posterior distribution of the model parameters using a nested sampling approach. This allows for ``painless'' Bayesian Computation, dealing with the expected multi-modality of the posterior distribution in a straightforward manner and not requiring the specification of starting values or an initial guess for the time delay, unlike existing methods. In addition, the proposed sampling procedure automatically evaluates the Bayesian evidence, allowing us to perform principled Bayesian model selection. TD-CARMA is parsimonious, and typically includes no more than a dozen unknown parameters. We apply TD-CARMA to six doubly lensed quasars HS 2209+1914, SDSS J1001+5027, SDSS J1206+4332, SDSS J1515+1511, SDSS J1455+1447, SDSS J1349+1227, estimating their time delays as $-21.96 \pm 1.448$, $120.93 \pm 1.015$, $111.51 \pm 1.452$, $210.80 \pm 2.18$, $45.36 \pm 1.93$ and $432.05 \pm 1.950$ respectively. These estimates are consistent with those derived in the relevant literature, but are typically two to four times more precise.

The analysis of individual X-ray sources that appear in a crowded field can easily be compromised by the misallocation of recorded events to their originating sources. Even with a small number of sources, that nonetheless have overlapping point spread functions, the allocation of events to sources is a complex task that is subject to uncertainty. We develop a Bayesian method designed to sift high-energy photon events from multiple sources with overlapping point spread functions, leveraging the differences in their spatial, spectral, and temporal signatures. The method probabilistically assigns each event to a given source. Such a disentanglement allows more detailed spectral or temporal analysis to focus on the individual component in isolation, free of contamination from other sources or the background. We are also able to compute source parameters of interest like their locations, relative brightness, and background contamination, while accounting for the uncertainty in event assignments. Simulation studies that include event arrival time information demonstrate that the temporal component improves event disambiguation beyond using only spatial and spectral information. The proposed methods correctly allocate up to 65% more events than the corresponding algorithms that ignore event arrival time information. We apply our methods to two stellar X-ray binaries, UV Cet and HBC515 A, observed with Chandra. We demonstrate that our methods are capable of removing the contamination due to a strong flare on UV Cet B in its companion approximately 40 times weaker during that event, and that evidence for spectral variability at timescales of a few ks can be determined in HBC515 Aa and HBC515 Ab.

Context: A radial temperature gradient together with an inhomogeneous radial electric field gradient is applied to a dielectric fluid confined in a vertical cylindrical annulus inducing thermal electro-hydrodynamic convection. Aims: Identification of the stability of the flow and hence of the line of marginal stability separating stable laminar free (natural) convection from thermal electro-hydrodynamic convection, its flow structures, pattern formation and critical parameters. Methods: Combination of different measurement techniques, namely the shadowgraph method and particle image velocimetry, as well as numerical simulation are used to qualify/quantify the flow. Results: We identify the transition from stable laminar free convection to thermal electro-hydrodynamic convective flow in a wide range of Rayleigh number and electric potential. The line of marginal stability found confirms results from linear stability analysis. The flow after first transition forms a structure of vertically aligned stationary columnar modes. We experimentally confirm critical parameters resulting from linear stability analysis and we show numerically an enhancement of heat transfer., Comment: 14 pages, 11 figures

This paper presents a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along paths. By selecting the combinations of Boolean and arithmetic operations allowed in constraints, one obtains several distinct logics generalizing CTL. We provide a thorough analysis of their expressiveness and succinctness, and of the complexity of their model-checking and satisfiability problems (ranging from P-complete to undecidable). Finally, we present two alternative logics with similar features and provide a comparative study of the properties of both variants., Comment: 34 pages

We consider the problem of symbolic reachability analysis of higher-order context-free processes. These models are generalizations of the context-free processes (also called BPA processes) where each process manipulates a data structure which can be seen as a nested stack of stacks. Our main result is that, for any higher-order context-free process, the set of all predecessors of a given regular set of configurations is regular and effectively constructible. This result generalizes the analogous result which is known for level 1 context-free processes. We show that this result holds also in the case of backward reachability analysis under a regular constraint on configurations. As a corollary, we obtain a symbolic model checking algorithm for the temporal logic E(U,X) with regular atomic predicates, i.e., the fragment of CTL restricted to the EU and EX modalities.

Several types of term rewriting systems can be distinguished by the way their rules overlap. In particular, we define the classes of prefix, suffix, bottom-up and top-down systems, which generalize similar classes on words. Our aim is to study the derivation relation of such systems (i.e. the reflexive and transitive closure of their rewriting relation) and, if possible, to provide a finite mechanism characterizing it. Using a notion of rational relations based on finite graph grammars, we show that the derivation of any bottom-up, top-down or suffix systems is rational, while it can be non recursive for prefix systems.

We define a new decidable logic for expressing and checking invariants of programs that manipulate dynamically-allocated objects via pointers and destructive pointer updates. The main feature of this logic is the ability to limit the neighborhood of a node that is reachable via a regular expression from a designated node. The logic is closed under boolean operations (entailment, negation) and has a finite model property. The key technical result is the proof of decidability. We show how to express precondition, postconditions, and loop invariants for some interesting programs. It is also possible to express properties such as disjointness of data-structures, and low-level heap mutations. Moreover, our logic can express properties of arbitrary data-structures and of an arbitrary number of pointer fields. The latter provides a way to naturally specify postconditions that relate the fields on entry to a procedure to the fields on exit. Therefore, it is possible to use the logic to automatically prove partial correctness of programs performing low-level heap mutations.

Linearly bounded Turing machines have been mainly studied as acceptors for context-sensitive languages. We define a natural class of infinite automata representing their observable computational behavior, called linearly bounded graphs. These automata naturally accept the same languages as the linearly bounded machines defining them. We present some of their structural properties as well as alternative characterizations in terms of rewriting systems and context-sensitive transductions. Finally, we compare these graphs to rational graphs, which are another class of automata accepting the context-sensitive languages, and prove that in the bounded-degree case, rational graphs are a strict sub-class of linearly bounded graphs.

We investigate families of infinite automata for context-sensitive languages. An infinite automaton is an infinite labeled graph with two sets of initial and final vertices. Its language is the set of all words labelling a path from an initial vertex to a final vertex. In 2001, Morvan and Stirling proved that rational graphs accept the context-sensitive languages between rational sets of initial and final vertices. This result was later extended to sub-families of rational graphs defined by more restricted classes of transducers. languages. Our contribution is to provide syntactical and self-contained proofs of the above results, when earlier constructions relied on a non-trivial normal form of context-sensitive grammars defined by Penttonen in the 1970's. These new proof techniques enable us to summarize and refine these results by considering several sub-families defined by restrictions on the type of transducers, the degree of the graph or the size of the set of initial vertices.