Existing dynamic scene rendering methods often struggle to preserve sharp edges and maintain temporal consistency. To address these challenges, we introduce Edge 4D Gaussian Splatting (Edge4DGS), a real-time rendering framework that renders fine-grained geometry from sparse monocular inputs in dynamic scenes. Edge4DGS proposes a hybrid geometric representation that augments Gaussian primitives with convex hulls, enabling accurate modeling of hard surfaces and complex boundaries. To enhance spatial precision, we introduce edge consistency regularization leveraging optical flow, guiding Gaussian distributions to align with true object contours. To enforce temporal coherence, we extend the regularization from discrete time steps to continuous unit intervals, enabling accurate motion modeling and reducing flickering artifacts. A two-stage coarse-to-fine optimization further improves geometric fidelity while preserving computational efficiency. Extensive experiments on monocular and multi-view motion datasets demonstrate that Edge4DGS achieves real-time, high-resolution rendering and consistently surpasses state-of-the-art methods, reducing LPIPS by 56.25%.

There has been emerging researches on leveraging large language models (LLMs) to improve the automation of theorem proving. However, they are still suffering from low accuracy and efficiency. In this paper, we propose to strengthen the existing approach by enhancing a language agent, which provides automatic explanation of terms and repair of tactics parameters. Term explanation explains terms specific to the proof obligations formally and tactic parameter repair complements the potentially correct proof tactics as much as possible. Similar to the existing approach, the agent uses GPT-4 as query objects in a search policy. During the search, we add term explanation to the prompt, and then the policy selects a proof tactic and repairs it. The repaired tactics interact with the theorem prover (Coq), and the execution result is fed back to build the prompt for the next policy invocation. We evaluate our approach on subsets of the CompCert project implemented using Coq. Our approach proves 8.11% more theorems than the existing language agent COPRA, and demonstrates faster search and proof speed. Besides, when term explanation and tactic parameter repair are applied, the performance of the SOTA method PROVERBOT9001 can be also improved.

Manipulating robots using natural language is the preferred way for non-technical specialists. The challenge lies in reliability and adaptability especially when robots operate in unstructured surroundings. In this paper, we propose a novel framework called Dialogue Generative Behavior Trees (DiaGBT). Natural language instructions from human operators are transformed into behavior trees (BTs) and further executed by robots. Compared to the emerging Large Language Models (LLMs), DiaGBT is comparable in terms of semantic understanding but more lightweight, since the parsing rules are produced by LLM but tailored for task-correlated instructions. Besides, DiaGBT allows multi-round human-robot interaction, where robots learn reusable skills in real time. For evaluation, we generate a dataset with 4k instruction-BT pairs covering 4 different scenarios. On average, DiaGBT reaches over 90% parsability and 80% plausibility. Similar results on the VEIL-500 dataset outperform the current state of the art.

Vision Transformer (ViT) models have recently emerged as powerful and versatile tools for various visual tasks. In this article, we investigate ViT in a more challenging scenario within the context of few-shot conditions. Recent work has achieved promising results in few-shot image classification by utilizing pre-trained vision transformer models. However, this work employs full fine-tuning for the downstream tasks, leading to significant overfitting and storage issues, especially in the remote sensing domain. In order to tackle these issues, we turn to the recently proposed Parameter-Efficient Tuning (PETuning) methods, which update only the newly added parameters while keeping the pre-trained backbone frozen. Inspired by these methods, we propose the Meta Visual Prompt Tuning (MVP) method. Specifically, we integrate the prompt-tuning-based PETuning method into the meta-learning framework and tailor it for remote sensing datasets, resulting in an efficient framework for Few-Shot Remote Sensing Scene Classification (FS-RSSC). Moreover, we introduce a novel data augmentation scheme that exploits patch embedding recombination to enhance the data diversity and quantity. This scheme is generalizable to any network that employs the ViT architecture as its backbone. Experimental results on the FS-RSSC benchmark demonstrate the superior performance of the proposed MVP over existing methods in various settings, including various-way-various-shot, various-way-one-shot, and cross-domain adaptation.

Few-shot learning has received widespread attention in remote sensing image scene classification. Many existing methods address this challenge by utilizing meta-learning and metric learning, which focus on developing feature extractors that can quickly adapt to novel few-shot scene classification (FSSC) tasks. However, these methods are often insufficient for real-world datasets with class confusion, where there is high inter-class compactness and intra-class diversity. To overcome this issue, we investigate efficient strategies, i.e., meta-learning-based transferable feature representation and contrastive-based prototypical regularization for learning task-adaptive class boundaries for FSSC. Specifically, we designed a combination of Query-vs-Prototype contrastive loss and Prototype-vs-Prototype contrastive loss to normalize the prototypical representation to be more discriminative in a novel FSSC task. Our proposed model is named the Hybrid Contrastive Prototypical Network (HCP-Net). Experiment results on three popular datasets under two standard benchmarks, i.e., general few-shot classification and few-shot domain generalization, indicate the effectiveness of the proposed method.

Optimizing the morphologies and the controllers that adapt to various tasks is a critical issue in the field of robot design, aka. embodied intelligence. Previous works typically model it as a joint optimization problem and use search-based methods to find the optimal solution in the morphology space. However, they ignore the implicit knowledge of task-to-morphology mapping which can directly inspire robot design. For example, flipping heavier boxes tends to require more muscular robot arms. This paper proposes a novel and general differentiable task-inspired framework for contact-aware robot design called Task2Morph. We abstract task features highly related to task performance and use them to build a task-to-morphology mapping. Further, we embed the mapping into a differentiable robot design process, where the gradient information is leveraged for both the mapping learning and the whole optimization. The experiments are conducted on three scenarios, and the results validate that Task2Morph outperforms DiffHand, which lacks a task-inspired morphology module, in terms of efficiency and effectiveness.

Big models, large datasets, and self-supervised learning (SSL) have recently gained substantial research interest due to their potential to alleviate our reliance on annotations. Considering the current high generalization ability of self-supervised models in literature, we explore in the letter how helpful SSL can be for a crucial task in remote sensing (RS), image scene classification, when forced to rely on only a few labeled samples. We proposed a simple prototype-based classification procedure without training and fine-tuning, which uses open self-supervised features from the contrastive language-image pre-training (CLIP). We test our method by exploiting ready-to-use open features on four diversified benchmark datasets, including red-green-blue (RGB) and multispectral (MS) images. Highly competitive accuracy has been obtained compared to work with similar settings, i.e., based on an exceedingly small number of labels. To the best of our knowledge, our model is the first to achieve such high accuracy in austere label conditions. We further analyze our approach from different perspectives, including its advantages and limitations, reasons for its astonishing performance, potential applications, and future improvements.

Object detection models based on feature pyramid networks have made significant progress in general object detection. However, small object detection is still a challenge for the existing models. In this paper, we think that two factors in the existing feature pyramid networks inhibit the performance of small object detection. The first one is that the different feature domains of shallow and deep layer features inhibit the model performance. The second one is that the accumulation of upper layer features leads to feature aliasing effect on the lower layer features, which interferes with the representations of small object features. Therefore, we propose Unified and Enhanced Feature Pyramid Networks (UEFPN) to improve the APs and ARs of small object detection. It has the following three characteristics: (1) Using the deep features of high-resolution image and original image to form the multi-scale features of unified domain. (2) In multi-scale features fusion, we learn the importance of upper layer features with the Channel Attention Fusion module (CAF) , to optimize feature aliasing effect and enhance the context information of shallow layer features. (3) UEFPN can be quickly applied to different models. The results of many experiments show that the models with UEFPN achieve significant performance improvement in small object detection compared with the baseline models.

Zero-shot learning (ZSL), with the assistance of the seen class image and additional semantic knowledge, generalizes its classification ability to the unseen class by aligning the visual-semantic space embeddings. Few previous methods have researched whether discriminative visual features are helpful to recognize different classes while neglecting the rich semantic information from the surrounding background. This paper proposes a channel-wise mix-fusion ZSL model (CMFZ) to contextualize the ZSL classifier's discriminative information by incorporating much richer visual semantic information from both objects and their semantic surrounding environments. In particular, the channel-wise connection module (CCM) learns to construct the relationship between the object and its surroundings. A collaborative channel-wise activation module (CAM) is adopted to learn from a more delicate scale image attained from the cropping module. It highlights the most distinct channels representing the object’s discriminative regions to eliminate inadvertently introduced background noise. Furthermore, the representation ability of the learned mapping is enhanced by integrating the visual semantic features processed by CCM and CAM. Experimental results show that CMFZ outperforms the state-of-the-art ZSL methods and verifies the effectiveness of incorporating visual semantic information.

In this paper, we propose micROS.BT, an event-driven behavior tree (BT) framework aiming at supporting swarm-robot coordination. Compared with other BT frame-works, micROS.BT implements the event-driven way under the multi-thread mode, which can effectively save computing resources. Moreover, in order to ensure swarm-robot coordination, we optimize the implementation of the traditional blackboard and propose the multi-mode blackboard, which supports inner-tree, inter-tree, and inter-robot data sharing. Furthermore, considering the limited modularity of a single tree, micROS.BT realizes a mechanism called hierarchical tree management which involves inter-tree notifying and waiting functionalities, while ensuring that each tree is independent and self-scheduled. The effectiveness of micROS.BT is verified by simulation and real-robot experiments for different system settings, showing that a substantial improvement is achieved in comparison with the traditional BT implementations.

Programming cooperative tasks for autonomous swarm robotic systems has always been challenging. In this paper, we introduce a concept `Actor', as a virtualization for robot platforms. Every robot platform in the swarm robotic system carries out the task and interacts with others as an Actor. We designed an Actor-based framework for the management of autonomous swarm robotic systems including modules and interfaces for the Actor, the collective Actor, and task management. The Actor-based framework enables task developers to explicitly model cooperative tasks without intricacies about the detailed robotic algorithms or the specific robot brands, and eases the burden on robotic algorithm developers by providing common functionalities. The proposed framework is implemented in C++ and validated quantitatively and qualitatively with a swarm of thirty drones by simulations and a swarm of ten drones by in-field tests.

The one-on-one target tracking problem is important in robot vision. Previous studies mainly focused on locating, depth information and control mechanism. In this study, we construct an autonomously visual tracking system called learn-to-track (LtT) by using a novel approach. This system only depends on a monocular camera. The main component is a deep convolutional neural network called the LtT, which trains a supervised image classifier by using images captured by the monocular camera in the follower robot. By operating merely on two adjacent frames, the network can predict the estimated velocity of the target, i.e., the velocity control for the follower. To verify the effectiveness of the LtT system, we construct a large-scale dataset that supports download l in the simulator, in which the LtT network is trained and the LtT system performance is evaluated. Furthermore, a remarkable tracking performance is achieved.

Abstract Multirobot systems have been studied extensively in the recent years. Maintaining connectivity has significant impacts on the stability and convergence of the multirobot systems. In this work, we design a three‐layer framework for multirobot coordination. Furthermore, a novel distributed algorithm is proposed to achieve the navigation objective while satisfying connectivity maintenance and collision avoidance constraints. The algorithm is a hybrid of an rapidly exploring random tree‐based planner and an extended distributed navigation function‐based controller. The coordination framework and the distributed algorithm are demonstrated to be effective through a series of illustrative simulations. They outperform the current state‐of‐the‐art method in terms of efficiency and applicability.

Subsequent to publication, the affiliation and citation of the article by Huang et al.1 have been modified. The correct order is presented above.

In this paper, we consider a surveillance scenario where a team of sensing robots survey a sensitive area and transmit the monitored data to a remote base station through a mobile relay. In this scenario, it is challenging to autonomously adjust the position of the mobile relay for the sake of minimizing the total communication-motion energy consumption of the system, while maintaining the communication quality of the mobile sensing robots. We first derive the asymptotically optimal transmit powers of the mobile relay and of the sensing robots according to the predefined end-to-end packet error rate (PER) requirement. Then, we propose a joint communication-motion planning (JCMP) method for minimizing the total communication-motion energy consumption in both: single- and multi-sensing-robot scenarios, where the trajectories of the sensing robots are rigorously defined. We further consider the scenario where the sensing robots' trajectories are not fixed but can be optimized in restrained areas. The effectiveness of the proposed JCMP is verified by analysis and numerical results for different system configurations, showing that a substantial energy-efficiency improvement may be achieved in comparison with the benchmark that only optimizes the communication energy consumption.

Abstract In this paper, we propose a distributed control approach for flocking and group maneuvering of nonholonomic agents, with constrained kinematic properties commonly found in practical systems, such as fixed‐wing unmanned aerial vehicles. Flocking of agents with differential drive kinematics is addressed by introducing a virtual leader–follower mechanism into the Olfati‐Saber's algorithm, which is originally proposed for holonomic agents with double integrator kinematics. Then, group maneuverability of the flock is achieved by superimposing a group motion onto each agent's flocking motion. Moreover, it is proven that speed limits are intrinsically guaranteed by the approach, which renders it more applicable in practical systems. Experimental results in MATLAB and Gazebo, a popular robotic simulator, are presented to evaluate the performance and demonstrate the effectiveness of the proposed approach.

Large and sparse are the prominent characteristics of small-world graph. In many scientific domains, such as biomedical science and scientific computing, as small-word graph grows in scale, processing small-world graph poses severe challenges to address mapping in Massive Parallel Processing. Data driven computation, unstructured data organization, which are poor in spatial and temporal locality, which are high frequency of memory access, leads to large RAM footprint on address mapping management. This paper proposes a novel approach with special Implementation for massive parallel processors. In our technique, The block level address mapping table is stored in large pages in DDR3 memory. Considering the highly frequency in accessing memory, we maintain a big cache in RAM to store address mapping entries of data array recently searching. The search algorithm in searching the cache is binary search. The goal is to reduce address mapping overhead without excessively compromising system response time. This scheme is designed for our massive parallel coprocessor system. For reducing power consumption, we have an attempt to implement address mapping of each massive parallel coprocessor in Field-Programmable Gate Array(FPGA). The experiment have been conducted on a real System on chip(Soc). The result shows that when the number of processor node is 4096 and its frequency is 233MHz, The RAM cost is 2.4 MB in each processor, when there is missing, the largest response time is 160us, which is less than the mainstream software implementation in address translation. In the case of making full use of available storage resources, The hit ratio in graph problem could be achieve 100%.

This paper considers a surveillance scenario where a mobile robot monitors an indoor environment and transmits the monitored data to a base station. Considering the indoor radio environment is complex, we first build the radio environment map (REM) with two different interpolation methods. Then, we combine REM with the structural blueprint of the building to build an integrated map called radio-structural map (RSM). Based on RSM, we propose an optimal surveillance path search (OSPS) method which minimizes the data transmission delay of the patrol robot under a communication reliability constraint. In OSPS, two optimization methods are adopted, which may sharply reduce the computation cost. Besides the numerical simulations, we further discuss the relationship between the communication reliability and data transmission delay. Finally, we test the applicability of OSPS in the stage simulator of ROS.

Abstract This paper proposes an efficient and stable numerical method for modeling catheterization during endovascular surgeries. The guidewire‐catheter combination is treated as an elastic rod, which has very large resistance against twisting about its medial axis. A torsion free assumption is made, and the physical behavior of the rod is predominately governed by stretching and bending energies. This simplification greatly reduces the computational complexity and makes the model more stable, while the simulation results are still realistic enough for its application in endovascular surgeries. A contact handling algorithm that directly makes use of the volume data of the relevant tissues is proposed to simulate the interaction between the guidewire‐catheter combination and the aortic wall. During each simulation step, the penetration depth of each vertex in contact with the aortic wall is calculated using moving least squares surfaces, and the contact is then resolved in a position‐based manner. A comprehensive quantitative evaluation of the rod model is performed to validate its accuracy. Finally, the proposed approach is applied in a prototype system for simulation of endovascular aneurysm repair surgeries. Its efficiency and effectiveness are demonstrated in a real‐time interactive catheterization simulation. Copyright © 2016 John Wiley & Sons, Ltd.

Abstract This paper presents an interactive simulation system for surgical procedures of endovascular aneurysm repair. It extracts anatomical structure of clinic interest from patient‐specific X‐ray computed tomography or magnetic resonance imaging data by image segmentation techniques, and then reconstructs surface triangular meshes of these anatomical structures from the volumetric data. The core of the system is an interactive computer‐based simulation module. It consists of a physical modeling unit, a collision detection unit, a visualization unit, and a control unit. The integration of these units together makes it possible for users to interact with the system in real time, performing virtual catheterization, angiography, and stent graft deployment under a user‐specified rendering mode. The prototype system can be used as a cost‐efficient tool for surgical planning with patient‐specific anatomical geometry and for practice of surgical procedures before actual operation. Copyright © 2016 John Wiley & Sons, Ltd.

Model abstraction plays an important role in model checking of source codes of programs. Slicing execution is a lightweight symbolic execution procedure to extract the models of C programs in an over-approximated way. In this paper, we present an approach to improving slicing execution with a novel concept called partial weakest precondition (PWP) to alleviate the space explosion problem. PWPs specify the corresponding weakest precondition conservatively by only considering part of program variables. We present how to integrate PWP with slicing execution, which leads to a compact model with much smaller state space compared with the one obtained by the original slicing execution. A new PWP implementation is also presented to avoid possible exponential PWP formula size and support pointers and aliases as well. The distinguished features of the implementation are that it does not need to translate the program to the passive form beforehand, and it supports loops very well. Comparing with slicing execution without PWP, the experimentation on SSL protocol based on the C source code openssl-0.9.6c shows that the state space may be reduced to only 1/10 after applying PWP.

When constructing a Virtual Machine Monitor(VMM), there are two different trends. The first one is trying to make the VMM be self-inclusive, while the second one is to make the VMM part of the host operating system. The former is prefered by independent virtualization provider(IVP) or BIOS manufacturer, and the later is advocated by OS vendors. In this article, after analyzing the implementation of three prevail VMMs, it is argued that: 1) unless the VMM is used as part of the BIOS, being self-inclusive is not a wise decision; 2) overly utilizing the existing functions that the underlying host operating system provides can not produce good solution to the problem of computer system virtualization. The design philosophy, architecture and implementation of Luvalley-lite is introduced to show our efforts to make a balance between reusing commodity OS functions and fitting the virtualization environment well. The approach of avoiding being restricted by the GPL license is also described. Due to the lack of publicly acknowledged performance benchmark, only preliminary experiments are conducted.

The paper presents a novel framework for scalable model checking of concurrent C programs. With the idea of verification reuse, it shows an integrated approach to efficient reduction of state space by abstraction, symbolic representation and dynamic partial-order reduction (DPOR) techniques. The framework is founded on an over-approximated model of the concurrent program by variable abstraction, and combines DPOR with lightweight symbolic execution to generate the symbolic conditions for all locations, called -conditions, which are intended for verification reuse. The -conditions of a location are weak approximation of the conditions that must be satisfied at that location so as to guarantee the temporal safety properties to be verified. These conditions will be checked for reusing the previous exploration in verification, and will be iteratively refined under the guidance of spurious counterexamples. The presented framework is demonstrated by several experiments including a concurrent software system whose server and client processes are derived from openssl-0.9.6c C source codes implementing the SSL protocol.

This paper presents a novel method, namely slicing execution, for model checking C programs with respect to temporal safety properties. The distinguished feature is that it shows a nice approach to the efficient reduction of state space by abstraction and symbolic representation. Slicing execution is founded on an over-approximated semantics of C programs by variable abstraction, and executes symbolically only the relevant statements under abstraction criteria to construct over-approximated finite models of programs, which may be model checked. The variable abstraction criterion begins with a proper initial set of program variables and may be iteratively refined according to spurious counterexamples generated during model checking. In general, the properties to be verified often involve only a few variables in practical programs. In these cases, significant state space reduction, as well as considerable improvement of the scalability, may be achieved. The presented method has been used to verify the initial handshake process of SSL protocol based on the C source code of openssl-0.9.6c. The experiment results confirm that slicing execution is not only practical but also effective.