OpenRaiser/Intern-Atlas huggingface dataset:
The Cost of Monitoring Alone
Venue: arXiv cs.LO 2019
Year: 2019

We compare the succinctness of two monitoring systems for properties of infinite traces, namely parallel and regular monitors. Although a parallel monitor can be turned into an equivalent regular monitor, the cost of this transformation is a double-exponential blowup in the syntactic size of the monitors, and a triple-exponential blowup when the goal is a deterministic monitor. We show that these bounds are tight and that they also hold for translations between corresponding fragments of Hennessy-Milner logic with recursion over infinite traces.
Multi-Objective Policy Generation for Multi-Robot Systems Using Riemannian Motion Policies
Venue: arXiv cs.RO 2019
Year: 2019

In many applications, multi-robot systems are required to achieve multiple objectives. For these multi-objective tasks, it is oftentimes hard to design a single control policy that fulfills all the objectives simultaneously. In this paper, we focus on multi-objective tasks that can be decomposed into a set of simple subtasks. Controllers for these subtasks are individually designed and then combined into a control policy for the entire team. One significant feature of our work is that the subtask controllers are designed along with their underlying manifolds. When a controller is combined with other controllers, their associated manifolds are also taken into account. This formulation yields a policy generation framework for multi-robot systems that can combine controllers for a variety of objectives while implicitly handling the interaction among robots and subtasks. To describe controllers on manifolds, we adopt Riemannian Motion Policies (RMPs), and propose a collection of RMPs for common multi-robot subtasks. Centralized and decentralized algorithms are designed to combine these RMPs into a final control policy. Theoretical analysis shows that the system under the control policy is stable. Moreover, we prove that many existing multi-robot controllers can be closely approximated by the framework. The proposed algorithms are validated through both simulated tasks and robotic implementations.
Spectre is here to stay: An analysis of side-channels and speculative execution
Venue: arXiv cs.PL 2019
Year: 2019

The recent discovery of the Spectre and Meltdown attacks represents a watershed moment not just for the field of Computer Security, but also of Programming Languages. This paper explores speculative side-channel attacks and their implications for programming languages. These attacks leak information through micro-architectural side-channels which we show are not mere bugs, but in fact lie at the foundation of optimization. We identify three open problems, (1) finding side-channels, (2) understanding speculative vulnerabilities, and (3) mitigating them. For (1) we introduce a mathematical meta-model that clarifies the source of side-channels in simulations and CPUs. For (2) we introduce an architectural model with speculative semantics to study recently-discovered vulnerabilities. For (3) we explore and evaluate software mitigations and prove one correct for this model. Our analysis is informed by extensive offensive research and defensive implementation work for V8, the production JavaScript virtual machine in Chrome. Straightforward extensions to model real hardware suggest these vulnerabilities present formidable challenges for effective, efficient mitigation. As a result of our work, we now believe that speculative vulnerabilities on today's hardware defeat all language-enforced confidentiality with no known comprehensive software mitigations, as we have discovered that untrusted code can construct a universal read gadget to read all memory in the same address space through side-channels. In the face of this reality, we have shifted the security model of the Chrome web browser and V8 to process isolation.
Data Correlation-Aware Resource Management in Wireless Virtual Reality (VR): An Echo State Transfer Learning Approach
Venue: arXiv cs.IT 2019
Year: 2019

In this paper, the problem of wireless virtual reality (VR) resource management is investigated for a wireless VR network in which VR contents are sent by a cloud to cellular small base stations (SBSs). The SBSs will collect tracking data from the VR users, over the uplink, in order to generate the VR content and transmit it to the end-users using downlink cellular links. For this model, the data requested or transmitted by the users can exhibit correlation, since the VR users may engage in the same immersive virtual environment with different locations and orientations. As such, the proposed resource management framework can factor in such spatial data correlation, to better manage uplink and downlink traffic. This potential spatial data correlation can be factored into the resource allocation problem to reduce the traffic load in both uplink and downlink. In the downlink, the cloud can transmit 360 contents or specific visible contents that are extracted from the original 360 contents to the users according to the users' data correlation to reduce the backhaul traffic load. For uplink, each SBS can associate with the users that have similar tracking information so as to reduce the tracking data size. This data correlation-aware resource management problem is formulated as an optimization problem whose goal is to maximize the users' successful transmission probability, defined as the probability that the content transmission delay of each user satisfies an instantaneous VR delay target. To solve this problem, an echo state networks (ESNs) based transfer learning is introduced. By smartly transferring information on the SBS's utility, the proposed transfer-based ESN algorithm can quickly cope with changes in the wireless networking environment.
Box-level Segmentation Supervised Deep Neural Networks for Accurate and Real-time Multispectral Pedestrian Detection
Venue: arXiv cs.CV 2019
Year: 2019

Effective fusion of complementary information captured by multi-modal sensors (visible and infrared cameras) enables robust pedestrian detection under various surveillance situations (e.g. daytime and nighttime). In this paper, we present a novel box-level segmentation supervised learning framework for accurate and real-time multispectral pedestrian detection by incorporating features extracted in visible and infrared channels. Specifically, our method takes pairs of aligned visible and infrared images with easily obtained bounding box annotations as input and estimates accurate prediction maps to highlight the existence of pedestrians. It offers two major advantages over the existing anchor box based multispectral detection methods. Firstly, it overcomes the hyperparameter setting problem occurred during the training phase of anchor box based detectors and can obtain more accurate detection results, especially for small and occluded pedestrian instances. Secondly, it is capable of generating accurate detection results using small-size input images, leading to improvement of computational efficiency for real-time autonomous driving applications. Experimental results on KAIST multispectral dataset show that our proposed method outperforms state-of-the-art approaches in terms of both accuracy and speed.
On instabilities of deep learning in image reconstruction - Does AI come at a cost?
Venue: arXiv cs.CV 2019
Year: 2019

Deep learning, due to its unprecedented success in tasks such as image classification, has emerged as a new tool in image reconstruction with potential to change the field. In this paper we demonstrate a crucial phenomenon: deep learning typically yields unstablemethods for image reconstruction. The instabilities usually occur in several forms: (1) tiny, almost undetectable perturbations, both in the image and sampling domain, may result in severe artefacts in the reconstruction, (2) a small structural change, for example a tumour, may not be captured in the reconstructed image and (3) (a counterintuitive type of instability) more samples may yield poorer performance. Our new stability test with algorithms and easy to use software detects the instability phenomena. The test is aimed at researchers to test their networks for instabilities and for government agencies, such as the Food and Drug Administration (FDA), to secure safe use of deep learning methods.
Breast Cancer: Model Reconstruction and Image Registration from Segmented Deformed Image using Visual and Force based Analysis
Venue: arXiv cs.CV 2019
Year: 2019

Breast lesion localization using tactile imaging is a new and developing direction in medical science. To achieve the goal, proper image reconstruction and image registration can be a valuable asset. In this paper, a new approach of the segmentation-based image surface reconstruction algorithm is used to reconstruct the surface of a breast phantom. In breast tissue, the sub-dermal vein network is used as a distinguishable pattern for reconstruction. The proposed image capturing device contacts the surface of the phantom, and surface deformation will occur due to applied force at the time of scanning. A novel force based surface rectification system is used to reconstruct a deformed surface image to its original structure. For the construction of the full surface from rectified images, advanced affine scale-invariant feature transform (A-SIFT) is proposed to reduce the affine effect in time when data capturing. Camera position based image stitching approach is applied to construct the final original non-rigid surface. The proposed model is validated in theoretical models and real scenarios, to demonstrate its advantages with respect to competing methods. The result of the proposed method, applied to path reconstruction, ends with a positioning accuracy of 99.7%
Multimodal music information processing and retrieval: survey and future challenges
Venue: arXiv cs.MM 2019
Year: 2019

Towards improving the performance in various music information processing tasks, recent studies exploit different modalities able to capture diverse aspects of music. Such modalities include audio recordings, symbolic music scores, mid-level representations, motion, and gestural data, video recordings, editorial or cultural tags, lyrics and album cover arts. This paper critically reviews the various approaches adopted in Music Information Processing and Retrieval and highlights how multimodal algorithms can help Music Computing applications. First, we categorize the related literature based on the application they address. Subsequently, we analyze existing information fusion approaches, and we conclude with the set of challenges that Music Information Retrieval and Sound and Music Computing research communities should focus in the next years.
Direct Automatic Coronary Calcium Scoring in Cardiac and Chest CT
Venue: arXiv cs.CV 2019
Year: 2019

Cardiovascular disease (CVD) is the global leading cause of death. A strong risk factor for CVD events is the amount of coronary artery calcium (CAC). To meet demands of the increasing interest in quantification of CAC, i.e. coronary calcium scoring, especially as an unrequested finding for screening and research, automatic methods have been proposed. Current automatic calcium scoring methods are relatively computationally expensive and only provide scores for one type of CT. To address this, we propose a computationally efficient method that employs two ConvNets: the first performs registration to align the fields of view of input CTs and the second performs direct regression of the calcium score, thereby circumventing time-consuming intermediate CAC segmentation. Optional decision feedback provides insight in the regions that contributed to the calcium score. Experiments were performed using 903 cardiac CT and 1,687 chest CT scans. The method predicted calcium scores in less than 0.3 s. Intra-class correlation coefficient between predicted and manual calcium scores was 0.98 for both cardiac and chest CT. The method showed almost perfect agreement between automatic and manual CVD risk categorization in both datasets, with a linearly weighted Cohen's kappa of 0.95 in cardiac CT and 0.93 in chest CT. Performance is similar to that of state-of-the-art methods, but the proposed method is hundreds of times faster. By providing visual feedback, insight is given in the decision process, making it readily implementable in clinical and research settings.
Improving Facial Emotion Recognition Systems Using Gradient and Laplacian Images
Venue: arXiv cs.CV 2019
Year: 2019

In this work, we have proposed several enhancements to improve the performance of any facial emotion recognition (FER) system. We believe that the changes in the positions of the fiducial points and the intensities capture the crucial information regarding the emotion of a face image. We propose the use of the gradient and the Laplacian of the input image together with the original input into a convolutional neural network (CNN). These modifications help the network learn additional information from the gradient and Laplacian of the images. However, the plain CNN is not able to extract this information from the raw images. We have performed a number of experiments on two well known datasets KDEF and FERplus. Our approach enhances the already high performance of state-of-the-art FER systems by 3 to 5%.
Highly Efficient Follicular Segmentation in Thyroid Cytopathological Whole Slide Image
Venue: arXiv cs.CV 2019
Year: 2019

In this paper, we propose a novel method for highly efficient follicular segmentation of thyroid cytopathological WSIs. Firstly, we propose a hybrid segmentation architecture, which integrates a classifier into Deeplab V3 by adding a branch. A large amount of the WSI segmentation time is saved by skipping the irrelevant areas using the classification branch. Secondly, we merge the low scale fine features into the original atrous spatial pyramid pooling (ASPP) in Deeplab V3 to accurately represent the details in cytopathological images. Thirdly, our hybrid model is trained by a criterion-oriented adaptive loss function, which leads the model converging much faster. Experimental results on a collection of thyroid patches demonstrate that the proposed model reaches 80.9% on the segmentation accuracy. Besides, 93% time is reduced for the WSI segmentation by using our proposed method, and the WSI-level accuracy achieves 53.4%.
Checking Observational Purity of Procedures
Venue: arXiv cs.SE 2019
Year: 2019

Verifying whether a procedure is observationally pure is useful in many software engineering scenarios. An observationally pure procedure always returns the same value for the same argument, and thus mimics a mathematical function. The problem is challenging when procedures use private mutable global variables, e.g., for memoization of frequently returned answers, and when they involve recursion. We present a novel verification approach for this problem. Our approach involves encoding the procedure's code as a formula that is a disjunction of path constraints, with the recursive calls being replaced in the formula with references to a mathematical function symbol. Then, a theorem prover is invoked to check whether the formula that has been constructed agrees with the function symbol referred to above in terms of input-output behavior for all arguments. We evaluate our approach on a set of realistic examples, using the Boogie intermediate language and theorem prover. Our evaluation shows that the invariants are easy to construct manually, and that our approach is effective at verifying observationally pure procedures.
Situation-Aware Pedestrian Trajectory Prediction with Spatio-Temporal Attention Model
Venue: arXiv cs.CV 2019
Year: 2019

Pedestrian trajectory prediction is essential for collision avoidance in autonomous driving and robot navigation. However, predicting a pedestrian's trajectory in crowded environments is non-trivial as it is influenced by other pedestrians' motion and static structures that are present in the scene. Such human-human and human-space interactions lead to non-linearities in the trajectories. In this paper, we present a new spatio-temporal graph based Long Short-Term Memory (LSTM) network for predicting pedestrian trajectory in crowded environments, which takes into account the interaction with static (physical objects) and dynamic (other pedestrians) elements in the scene. Our results are based on two widely-used datasets to demonstrate that the proposed method outperforms the state-of-the-art approaches in human trajectory prediction. In particular, our method leads to a reduction in Average Displacement Error (ADE) and Final Displacement Error (FDE) of up to 55% and 61% respectively over state-of-the-art approaches.
A Broad Class of Discrete-Time Hypercomplex-Valued Hopfield Neural Networks
Venue: arXiv cs.LG 2019
Year: 2019

In this paper, we address the stability of a broad class of discrete-time hypercomplex-valued Hopfield-type neural networks. To ensure the neural networks belonging to this class always settle down at a stationary state, we introduce novel hypercomplex number systems referred to as real-part associative hypercomplex number systems. Real-part associative hypercomplex number systems generalize the well-known Cayley-Dickson algebras and real Clifford algebras and include the systems of real numbers, complex numbers, dual numbers, hyperbolic numbers, quaternions, tessarines, and octonions as particular instances. Apart from the novel hypercomplex number systems, we introduce a family of hypercomplex-valued activation functions called $\mathcal{B}$-projection functions. Broadly speaking, a $\mathcal{B}$-projection function projects the activation potential onto the set of all possible states of a hypercomplex-valued neuron. Using the theory presented in this paper, we confirm the stability analysis of several discrete-time hypercomplex-valued Hopfield-type neural networks from the literature. Moreover, we introduce and provide the stability analysis of a general class of Hopfield-type neural networks on Cayley-Dickson algebras.
Engineered Self-Organization for Resilient Robot Self-Assembly with Minimal Surprise
Venue: arXiv cs.NE 2019
Year: 2019

In collective robotic systems, the automatic generation of controllers for complex tasks is still a challenging problem. Open-ended evolution of complex robot behaviors can be a possible solution whereby an intrinsic driver for pattern formation and self-organization may prove to be important. We implement such a driver in collective robot systems by evolving prediction networks as world models in pair with action-selection networks. Fitness is given for good predictions which causes a bias towards easily predictable environments and behaviors in the form of emergent patterns, that is, environments of minimal surprise. There is no task-dependent bias or any other explicit predetermination for the different qualities of the emerging patterns. A careful configuration of actions, sensor models, and the environment is required to stimulate the emergence of complex behaviors. We study self-assembly to increase the scenario's complexity for our minimal surprise approach and, at the same time, limit the complexity of our simulations to a grid world to manage the feasibility of this approach. We investigate the impact of different swarm densities and the shape of the environment on the emergent patterns. Furthermore, we study how evolution can be biased towards the emergence of desired patterns. We analyze the resilience of the resulting self-assembly behaviors by causing damages to the assembled pattern and observe the self-organized reassembly of the structure. In summary, we evolved swarm behaviors for resilient self-assembly and successfully engineered self-organization in simulation. In future work, we plan to transfer our approach to a swarm of real robots.
Off-Policy Actor-Critic in an Ensemble: Achieving Maximum General Entropy and Effective Environment Exploration in Deep Reinforcement Learning
Venue: arXiv cs.LG 2019
Year: 2019

We propose a new policy iteration theory as an important extension of soft policy iteration and Soft Actor-Critic (SAC), one of the most efficient model free algorithms for deep reinforcement learning. Supported by the new theory, arbitrary entropy measures that generalize Shannon entropy, such as Tsallis entropy and Renyi entropy, can be utilized to properly randomize action selection while fulfilling the goal of maximizing expected long-term rewards. Our theory gives birth to two new algorithms, i.e., Tsallis entropy Actor-Critic (TAC) and Renyi entropy Actor-Critic (RAC). Theoretical analysis shows that these algorithms can be more effective than SAC. Moreover, they pave the way for us to develop a new Ensemble Actor-Critic (EAC) algorithm in this paper that features the use of a bootstrap mechanism for deep environment exploration as well as a new value-function based mechanism for high-level action selection. Empirically we show that TAC, RAC and EAC can achieve state-of-the-art performance on a range of benchmark control tasks, outperforming SAC and several cutting-edge learning algorithms in terms of both sample efficiency and effectiveness.
Improving Catheter Segmentation & Localization in 3D Cardiac Ultrasound Using Direction-Fused FCN
Venue: arXiv cs.CV 2019
Year: 2019

Fast and accurate catheter detection in cardiac catheterization using harmless 3D ultrasound (US) can improve the efficiency and outcome of the intervention. However, the low image quality of US requires extra training for sonographers to localize the catheter. In this paper, we propose a catheter detection method based on a pre-trained VGG network, which exploits 3D information through re-organized cross-sections to segment the catheter by a shared fully convolutional network (FCN), which is called a Direction-Fused FCN (DF-FCN). Based on the segmented image of DF-FCN, the catheter can be localized by model fitting. Our experiments show that the proposed method can successfully detect an ablation catheter in a challenging ex-vivo 3D US dataset, which was collected on the porcine heart. Extensive analysis shows that the proposed method achieves a Dice score of 57.7%, which offers at least an 11.8 % improvement when compared to state-of-the-art instrument detection methods. Due to the improved segmentation performance by the DF-FCN, the catheter can be localized with an error of only 1.4 mm.