Benjamin Johnson

Ali Baheri, Hao Ren, Benjamin Johnson et al.

We present a safety verification framework for design-time and run-time assurance of learning-based components in aviation systems. Our proposed framework integrates two novel methodologies. From the design-time assurance perspective, we propose offline mixed-fidelity verification tools that incorporate knowledge from different levels of granularity in simulated environments. From the run-time assurance perspective, we propose reachability- and statistics-based online monitoring and safety guards for a learning-based decision-making model to complement the offline verification methods. This framework is designed to be loosely coupled among modules, allowing the individual modules to be developed using independent methodologies and techniques, under varying circumstances and with different tool access. The proposed framework offers feasible solutions for meeting system safety requirements at different stages throughout the system development and deployment cycle, enabling the continuous learning and assessment of the system product.

Lucas Howard, Aneesh C. Subramanian, Gregory Thompson et al.

The continuous improvement in weather forecast skill over the past several decades is largely due to the increasing quantity of available satellite observations and their assimilation into operational forecast systems. Assimilating these observations requires observation operators in the form of radiative transfer models. Significant efforts have been dedicated to enhancing the computational efficiency of these models. Computational cost remains a bottleneck, and a large fraction of available data goes unused for assimilation. To address this, we used machine learning to build an efficient neural network based probabilistic emulator of the Community Radiative Transfer Model (CRTM), applied to the GOES Advanced Baseline Imager. The trained NN emulator predicts brightness temperatures output by CRTM and the corresponding error with respect to CRTM. RMSE of the predicted brightness temperature is 0.3 K averaged across all channels. For clear sky conditions, the RMSE is less than 0.1 K for 9 out of 10 infrared channels. The error predictions are generally reliable across a wide range of conditions. Explainable AI methods demonstrate that the trained emulator reproduces the relevant physics, increasing confidence that the model will perform well when presented with new data.

Benjamin Johnson, Aron Laszka, Jens Grossklags et al.

Cryptocurrency exchanges are frequently targeted and compromised by cyber-attacks, which may lead to significant losses for the depositors and closure of the affected exchanges. These risks threaten the viability of the entire public blockchain ecosystem since exchanges serve as major gateways for participation in public blockchain technologies. In this paper, we develop an economic model to capture the short-term incentives of cryptocurrency exchanges with respect to making security investments and establishing transaction fees. Using the model, we derive conclusions regarding an exchange's optimal economic decisions, and illustrate key features of these conclusions using graphs based on real-world data. Our security investment model exhibits horizontal scaling properties with respect to reducing exposure to losses, and may be of special interest to exchanges operating in markets with high price volatility.

Yiannis Kantaros, Benjamin Johnson, Sagar Chowdhury et al.

In this paper, we present a control framework that allows magnetic microrobot teams to accomplish complex micromanipulation tasks captured by global Linear Temporal Logic (LTL) formulas. To address this problem, we propose an optimal control synthesis method that constructs discrete plans for the robots that satisfy both the assigned tasks as well as proximity constraints between the robots due to the physics of the problem. Our proposed algorithm relies on an existing optimal control synthesis approach combined with a novel sampling-based technique to reduce the state-space of the product automaton that is associated with the LTL specifications. The synthesized discrete plans are executed by the microrobots independently using local magnetic fields. Simulation studies show that the proposed algorithm can address large-scale planning problems that cannot be solved using existing optimal control synthesis approaches. Moreover, we present experimental results that also illustrate the potential of our method in practice. To the best of our knowledge, this is the first control framework that allows independent control of teams of magnetic microrobots for temporal micromanipulation tasks.