Abstract

Abstract
[No abstract available]

Abstract
Capricious data streams, marked by random emergence and disappearance of features, are common in practical scenarios such as sensor networks. In existing research, they are mainly handled based on linear classifiers, feature correlation or ensemble of trees. There exist deficiencies such as limited learning capacity and high time cost. More importantly, the concept drift problem in them receives little attention. Therefore, drifting capricious data streams are focused on in this paper, and a new algorithm DCFHT (online learning from Drifting Capricious data streams with Flexible Hoeffding Tree) is proposed based on a single Hoeffding tree. DCFHT can achieve non-linear modeling and adaptation to drifts. First, DCFHT dynamically reuses and restructures the tree. The reusable information includes the tree structure and the information stored in each node. The restructuring process ensures that the Hoeffding tree dynamically aligns with the latest universal feature space. Second, DCFHT adapts to drifts in an informed way. When a drift is detected, DCFHT starts training a backup learner until it reaches the ability to replace the primary learner. Various experiments on 22 public and 15 synthetic datasets show that it is not only more accurate, but also maintains relatively low runtime on capricious data streams.

Abstract
We propose a hybrid formal verification approach that combines high-level deductive reasoning and circuit-based reasoning and apply it to highly optimized cryptographic assembly code. Our approach permits scaling up formal verification in two complementary directions: 1) it reduces the proof effort required for low-level functions where the computation logics are obfuscated by the intricate use of architecture-specific instructions and 2) it permits amortizing the effort of proving one implementation by using equivalence checking to propagate the guarantees to other implementations of the same computation using different optimizations or targeting different architectures. We demonstrate our approach via an extension to the EasyCrypt proof assistant and by revisiting formally verified implementations of ML-KEM in Jasmin. As a result, we obtain the first formally verified implementation of ML-KEM that offers performance comparable to the fastest non-verified implementation in x86-64 architectures.

Abstract
Capricious data streams make no assumptions on feature space dynamics and are mainly handled based on feature correlation, linear classifier or ensemble of trees. There exist deficiencies such as limited learning capacity, high time cost and low interpretability. To enhance effectiveness and efficiency, capricious data streams are handled through a single tree in this paper, and the proposed algorithm is named OCFHT (Online learning from Capricious data streams with Flexible Hoeffding Tree). OCFHT does not rely on the correlation pattern among features and can achieve non-linear modeling. Its performance is verified by various experiments on 18 public datasets, showing that it is not only more accurate than state-of-the-art algorithms, but also runs faster.

Abstract
This article presents the development of a tethered fixed-wing tail-sitter VTOL (Vertical Take-Off and Landing) Unmanned Aerial Vehicle system. The design focuses on improving energy efficiency by utilizing the wings to harness wind power, similar to a kite, while maintaining VTOL functionality. A distinguishing feature is the purpose-built autopilot system, with custom hardware and software components specifically engineered for this application. The study presents the system identification process for obtaining five MIMO (Multiple-Input Multiple-Output) transfer functions that characterize the dynamics between roll-yaw commands and responses, including the tether angle feedback. To address the inherent coupling effects and uncertainties in the system, robust mixed sensitivity (H-infinity) MIMO controllers are developed. The controllers were validated through both simulations and experimental flights, demonstrating effective performance in handling cross-coupling effects and maintaining stability under various operating conditions. According to flight test findings, the system can precisely manage the tether angle while adjusting for ground effect disturbances. This allows for accurate tethered navigation, a stable attitude, and the maintenance of an adequate yaw heading.