Search

DAG-based consensus protocols are being adoption by blockchain companies to decrease energy footprints and improve security. A DAG-based consensus protocol collaboratively constructs a partial order of blocks of transactions and produces linearly ordered blocks. The ubiquity and strategic importance of blockchains call for formal proof of the correctness of key components, namely, consensus protocols. This paper presents a safety-proven formal specification of two DAG-based protocols. Our specification highlights several dissemination, DAG construction, and ordering variations that can be combined to express the two protocols. The formalization requires a refinement approach for modeling the consensus. In an abstract model, we first show the safety of DAG-based consensus on leader blocks and then further refine the specification to encompass all blocks for all processes. The TLA+ specification for a given protocol consists of 492-732 lines, and the proof system TLAPS verifies 2025-2294 obligations in 6-8 minutes.

In this paper, we analytically study the transient stability of grid-connected converters with grid-forming complex droop control, also known as dispatchable virtual oscillator control. We prove theoretically that complex droop control, as a state-of-the-art grid-forming control, always possesses steady-state equilibria whereas classical droop control does not. We provide quantitative conditions for complex droop control maintaining transient stability (global asymptotic stability) under grid disturbances, which is beyond the well-established local (non-global) stability for classical droop control. For the transient instability of complex droop control, we reveal that the unstable trajectories are bounded, manifesting as limit cycle oscillations. Moreover, we extend our stability results from second-order grid-forming control dynamics to full-order system dynamics that additionally encompass both circuit electromagnetic transients and inner-loop dynamics. Our theoretical results contribute an insightful understanding of the transient stability and instability of complex droop control and offer practical guidelines for parameter tuning and stability guarantees.

We analyze a dual-port grid-forming (GFM) control for power systems containing ac and dc transmission, converter-interfaced generation and energy storage, and legacy generation. To operate such a system and provide standard services, state-of-the-art control architectures i) require assigning grid-following (GFL) and GFM controls to different converters, and ii) result in highly complex system dynamics. In contrast, dual-port GFM control (i) subsumes common functions of GFM and GFL controls in a simple controller, ii) can be applied to a wide range of emerging technologies independently of the network configuration, and iii) significantly reduces system complexity. In this work, we provide i) an end-to-end modeling framework that allows to model complex topologies through composition of reduced-order device models, ii) an in-depth discussion of universal dual-port GFM control for emerging power systems, and iii) end-to-end stability conditions that cover a wide range of network topologies, emerging technologies, and legacy technologies. Finally, we validate our findings in detailed case studies.

Dependency hell is a well-known pain point in the development of large software projects and machine learning (ML) code bases are not immune from it. In fact, ML applications suffer from an additional form, namely, "data source dependency hell". This term refers to the central role played by data and its unique quirks that often lead to unexpected failures of ML models which cannot be explained by code changes. In this paper, we present an automated dependency mapping framework that allows MLOps engineers to monitor the whole dependency map of their models in a fast paced engineering environment and thus mitigate ahead of time the consequences of any data source changes (e.g., re-train model, ignore data, set default data etc.). Our system is based on a unified and generic approach, employing techniques from static analysis, from which data sources can be identified reliably for any type of dependency on a wide range of source languages and artefacts. The dependency mapping framework is exposed as a REST web API where the only input is the path to the Git repository hosting the code base. Currently used by MLOps engineers at Microsoft, we expect such dependency map APIs to be adopted more widely by MLOps engineers in the future.

Data leakage is a well-known problem in machine learning. Data leakage occurs when information from outside the training dataset is used to create a model. This phenomenon renders a model excessively optimistic or even useless in the real world since the model tends to leverage greatly on the unfairly acquired information. To date, detection of data leakages occurs post-mortem using run-time methods. However, due to the insidious nature of data leakage, it may not be apparent to a data scientist that a data leakage has occurred in the first place. For this reason, it is advantageous to detect data leakages as early as possible in the development life cycle. In this paper, we propose a novel static analysis to detect several instances of data leakages during development time. We define our analysis using the framework of abstract interpretation: we define a concrete semantics that is sound and complete, from which we derive a sound and computable abstract semantics. We implement our static analysis inside the open-source NBLyzer static analysis framework and demonstrate its utility by evaluating its performance and precision on over 2000 Kaggle competition notebooks.

In this letter, we study the nonlinear stability problem of converter-based power systems, where the converter dynamics are governed by a complex droop control. This complex droop control augments the well-known power-frequency (p-f) droop control, and it proves to be equivalent to the state-of-the-art dispatchable virtual oscillator control (dVOC). In this regard, it is recognized as a promising grid-forming solution to address the high penetration of converters in future power systems. In previous work, the global stability of dVOC (i.e., complex droop control) has been proven by prespecifying a nominal synchronous steady state. For a general case of non-nominal (i.e., drooped) synchronous steady states, however, the stability problem requires further investigation. In this letter, we provide parametric conditions under which a non-nominal synchronous steady state exists and the system is almost globally asymptotically stable with respect to this non-nominal synchronous steady state.

In this work we present a novel dual-port grid-forming control strategy, for permanent magnet synchronous generator wind turbines with back-to-back voltage source converters, that unifies the entire range of functions from maximum power point tracking (MPPT) to providing inertia and fast frequency response without explicit mode switching between grid-following and grid-forming control. The controls impose a well-defined AC voltage at the grid-side converter (GSC) and the machine-side converter (MSC) AC terminals and explicitly stabilize the DC-link capacitor voltage through both GSC and MSC. The wind turbine's kinetic energy storage and curtailment are adjusted through a combination of implicit rotor speed control and pitch angle control and directly determine the operating mode and level of grid support. Moreover, we provide analytical small-signal stability conditions for a simplified system and explicitly characterize the relationship between control gains, curtailment, and the wind turbines steady-state response. Finally, a detailed simulation study is used to validate the results and compared the proposed control with state-of-the-art MPPT control., Comment: In proceedings of the 11th Bulk Power Systems Dynamics and Control Symposium (IREP 2022), July 25-30, 2022, Banff, Canada

The nature of dark matter and properties of neutrinos are among the most pressing issues in contemporary particle physics. The dual-phase xenon time-projection chamber is the leading technology to cover the available parameter space for Weakly Interacting Massive Particles (WIMPs), while featuring extensive sensitivity to many alternative dark matter candidates. These detectors can also study neutrinos through neutrinoless double-beta decay and through a variety of astrophysical sources. A next-generation xenon-based detector will therefore be a true multi-purpose observatory to significantly advance particle physics, nuclear physics, astrophysics, solar physics, and cosmology. This review article presents the science cases for such a detector., Comment: 77 pages, 40 figures, 1262 references

Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency environments, where many useful contracts are impractical to codify as DFAs and/or the size of their associated DFAs leads to sub-par performance. To address this bottleneck, we present a lightweight typestate analyzer, based on an expressive specification language that can succinctly specify code contracts. By implementing it in the static analyzer Infer, we demonstrate considerable performance and usability benefits when compared to existing techniques. A central insight is to rely on a sub-class of DFAs with efficient bit-vector operations.

Notebooks provide an interactive environment for programmers to develop code, analyse data and inject interleaved visualizations in a single environment. Despite their flexibility, a major pitfall that data scientists encounter is unexpected behaviour caused by the unique out-of-order execution model of notebooks. As a result, data scientists face various challenges ranging from notebook correctness, reproducibility and cleaning. In this paper, we propose a framework that performs static analysis on notebooks, incorporating their unique execution semantics. Our framework is general in the sense that it accommodate for a wide range of analyses, useful for various notebook use cases. We have instantiated our framework on a diverse set of analyses and have evaluated them on 2211 real world notebooks. Our evaluation demonstrates that the vast majority (98.7%) of notebooks can be analysed in less than a second, well within the time frame required by interactive notebook clients

In this work, we investigate grid-forming (GFM) control for dc/ac power converters in emerging power systems that contain ac and dc networks, renewable generation, and conventional generation. We propose a novel power-balancing GFM control strategy that simultaneously forms the converter ac and dc voltage (i.e., dual-port GFM), unifies standard grid-following (GFL) and GFM functions, and is backwards compatible with conventional machine-based generation. Notably, in contrast to state-of-the-art control architectures that use a mix of grid-forming and grid-following control, dual-port GFM control can be used independently of the converter power source or network configuration. Our main contribution are stability conditions that cover emerging hybrid ac/dc networks as well as machines and converters with and without controlled power source, that only require knowledge of the system topology. Finally, a detailed case study is used to illustrate and validate the results.

The unbound proton-rich nuclei $^{16}$F and $^{15}$F are investigated experimentally and theoretically. Several experiments using the resonant elastic scattering method were performed at GANIL with radioactive beams to determine the properties of the low lying states of these nuclei. Strong asymmetry between $^{16}$F-$^{16}$N and $^{15}$F-$^{15}$C mirror nuclei is observed. The strength of the $nucleon-nucleon$ effective interaction involving the loosely bound proton in the $s_{1/2}$ orbit is significantly modified with respect to their mirror nuclei $^{16}$N and $^{15}$C. The reduction of the effective interaction is estimated by calculating the interaction energies with a schematic zero-range force. It is found that, after correcting for the effects due to changes in the radial distribution of the single-particle wave functions, the mirror symmetry of the $n-p$ interaction is preserved between $^{16}$F and $^{16}$N, while a difference of 63\% is measured between the $p-p$ versus $n-n$ interactions in the second excited state of $^{15}$F and $^{15}$C nuclei. Several explanations are proposed.

Inspired by classical sensitivity results for nonlinear optimization, we derive and discuss new quantitative bounds to characterize the solution map and dual variables of a parametrized nonlinear program. In particular, we derive explicit expressions for the local and global Lipschitz constants of the solution map of non-convex or convex optimization problems, respectively. Our results are geared towards the study of time-varying optimization problems which are commonplace in various applications of online optimization, including power systems, robotics, signal processing and more. In this context, our results can be used to bound the rate of change of the optimizer. To illustrate the use of our sensitivity bounds we generalize existing arguments to quantify the tracking performance of continuous-time, monotone running algorithms. Further, we introduce a new continuous-time running algorithm for time-varying constrained optimization which we model as a so-called perturbed sweeping process. For this discontinuous scheme, we establish an explicit bound on the asymptotic solution tracking for a class of convex problems.

Single neutron- and proton-removal cross sections have been systematically measured for 72 medium-mass neutron-rich nuclei around Z=50 and energies around 900A MeV using the FRagment Separator (FRS) at GSI. Neutron-removal cross sections are described by considering the knock-out process together with initial- and final-state interactions. Proton-removal cross sections are, however, significantly smaller than predicted by the same calculations. The observed difference can be explained as due to the knockout of short-correlated protons in neutron-proton dominating pairs.

We detail the sensitivity of the liquid xenon (LXe) DARWIN observatory to solar neutrinos via elastic electron scattering. We find that DARWIN will have the potential to measure the fluxes of five solar neutrino components: $pp$, $^7$Be, $^{13}$N, $^{15}$O and $pep$. The precision of the $^{13}$N, $^{15}$O and $pep$ components is hindered by the double-beta decay of $^{136}$Xe and, thus, would benefit from a depleted target. A high-statistics observation of $pp$ neutrinos would allow us to infer the values of the weak mixing angle, $\sin^2\theta_w$, and the electron-type neutrino survival probability, $P_e$, in the electron recoil energy region from a few keV up to 200 keV for the first time, with relative precision of 5% and 4%, respectively, at an exposure of 300 ty. An observation of $pp$ and $^7$Be neutrinos would constrain the neutrino-inferred solar luminosity down to 0.2%. A combination of all flux measurements would distinguish between the high (GS98) and low metallicity (AGS09) solar models with 2.1-2.5$\sigma$ significance, independent of external measurements from other experiments or a measurement of $^8$B neutrinos through coherent elastic neutrino-nucleus scattering in DARWIN. Finally, we demonstrate that with a depleted target DARWIN may be sensitive to the neutrino capture process of $^{131}$Xe., Comment: 9 pages, 4 figures; for associated data files, see https://github.com/Physik-Institut-UZH/DARWIN-Sensitivity-Studies/tree/master/solar_neutrinos_electron_scattering

In this work, we present a Lyapunov framework for establishing stability with respect to a compact set for a nested interconnection of nonlinear dynamical systems ordered from slow to fast according to their convergence rates, where each of the dynamics are influenced only by the slower dynamics and the successive fastest one. The proposed approach explicitly considers more than two time scales, it does not require modeling multiple time scales via scalar time constants, and provides analytic bounds that make ad-hoc time-scale separation arguments rigorous. Motivated by the technical results, we develop a novel control strategy for a grid-forming power converter that consists of an inner cascaded two-degree of freedom controller and dispatchable virtual oscillator control as a reference model. The resulting closed-loop converter-based AC power system is in the form of a nested system with multiple time scales. We apply our technical results to obtain explicit bounds on the controller set-points, branch powers, and control gains that guarantee almost global asymptotic stability of the multi-converter AC power system with respect to a pre-specified solution of the AC power-flow equations. Finally, we validate the performance of the proposed control structure in a case study using a high-fidelity simulation with detailed hardware validated converter models.

Logic programming languages such as Datalog have become popular as Domain Specific Languages (DSLs) for solving large-scale, real-world problems, in particular, static program analysis and network analysis. The logic specifications which model analysis problems, process millions of tuples of data and contain hundreds of highly recursive rules. As a result, they are notoriously difficult to debug. While the database community has proposed several data-provenance techniques that address the Declarative Debugging Challenge for Databases, in the cases of analysis problems, these state-of-the-art techniques do not scale. In this paper, we introduce a novel bottom-up Datalog evaluation strategy for debugging: our provenance evaluation strategy relies on a new provenance lattice that includes proof annotations, and a new fixed-point semantics for semi-naive evaluation. A debugging query mechanism allows arbitrary provenance queries, constructing partial proof trees of tuples with minimal height. We integrate our technique into Souffle, a Datalog engine that synthesizes C++ code, and achieve high performance by using specialized parallel data structures. Experiments are conducted with DOOP/DaCapo, producing proof annotations for tens of millions of output tuples. We show that our method has a runtime overhead of 1.27x on average while being more flexible than existing state-of-the-art techniques., Comment: 28 pages, 18 figures, technical report