OpenRaiser/Intern-Atlas huggingface dataset:
On Verification of D-Detectability for Discrete Event Systems
Venue: arXiv cs.FL 2020
Year: 2020

Detectability has been introduced as a generalization of state-estimation properties of discrete event systems studied in the literature. It asks whether the current and subsequent states of a system can be determined based on observations. Since, in some applications, to exactly determine the current and subsequent states may be too strict, a relaxed notion of D-detectability has been introduced, distinguishing only certain pairs of states rather than all states. Four variants of D-detectability have been defined: strong (periodic) D-detectability and weak (periodic) D-detectability. Deciding weak (periodic) D-detectability is PSpace-complete, while deciding strong (periodic) detectability or strong D-detectability is polynomial (and we show that it is actually NL-complete). However, to the best of our knowledge, it is an open problem whether there exists a polynomial-time algorithm deciding strong periodic D-detectability. We solve this problem by showing that deciding strong periodic D-detectability is a PSpace-complete problem, and hence there is no polynomial-time algorithm unless PSpace = P. We further show that there is no polynomial-time algorithm deciding strong periodic D-detectability even for systems with a single observable event, unless P = NP. Finally, we propose a class of systems for which the problem is tractable.
Image-based material characterization of complex microarchitectured additively manufactured structures
Venue: arXiv cs.CE 2020
Year: 2020

Significant developments in the field of additive manufacturing (AM) allowed the fabrication of complex microarchitectured components with varying porosity across different scales. However, due to the high complexity of this process, the final parts can exhibit significant variations in the nominal geometry. Computer tomographic images of 3D printed components provide extensive information about these microstructural variations, such as process-induced porosity, surface roughness, and other undesired morphological discrepancies. Yet, techniques to incorporate these imperfect AM geometries into the numerical material characterization analysis are computationally demanding. In this contribution, an efficient image-to-material-characterization framework using the high-order parallel Finite Cell Method is proposed. In this way, a flexible non-geometry-conforming discretization facilitates mesh generation for very complex microstructures at hand and allows a direct analysis of the images stemming from CT-scans. Numerical examples including a comparison to the experiments illustrate the potential of the proposed framework in the field of additive manufacturing product simulation.
It's easy to fool yourself: Case studies on identifying bias and confounding in bio-medical datasets
Venue: arXiv cs.LG 2020
Year: 2020

Confounding variables are a well known source of nuisance in biomedical studies. They present an even greater challenge when we combine them with black-box machine learning techniques that operate on raw data. This work presents two case studies. In one, we discovered biases arising from systematic errors in the data generation process. In the other, we found a spurious source of signal unrelated to the prediction task at hand. In both cases, our prediction models performed well but under careful examination hidden confounders and biases were revealed. These are cautionary tales on the limits of using machine learning techniques on raw data from scientific experiments.
Optimal Fraction Repetition Codes for Access-Balancing in Distributed Storage
Venue: arXiv cs.IT 2020
Year: 2020

To solve the access-balancing problem in distributed storage systems, we introduce a new combinatorial model, called MinVar model for fractional repetition (FR) codes. Since FR codes are based on graphs or set systems, our MinVar model is characterized by the property that the variance among the sums of block-labels incident to a fixed vertex is minimized. This characterization is different from Dau and Milenkovic's MaxMinSum model, while the minimum sum of labels is maximized. We show that our MinVar model is meaningful by distinguishing labelings with different variances but with the same MaxMin value for some FR codes. By reformulating the MinVar model to an equivalent vertex-labeling problem of graphs, we find several families of optimal FR codes with balanced access frequency, and provide fundamental results for both problems. It is interesting that MinVar model is closely related to the concept of magic-labeling in graph theory.
A Comprehensive Review of Shepherding as a Bio-inspired Swarm-Robotics Guidance Approach
Venue: arXiv cs.RO 2020
Year: 2020

The simultaneous control of multiple coordinated robotic agents represents an elaborate problem. If solved, however, the interaction between the agents can lead to solutions to sophisticated problems. The concept of swarming, inspired by nature, can be described as the emergence of complex system-level behaviors from the interactions of relatively elementary agents. Due to the effectiveness of solutions found in nature, bio-inspired swarming-based control techniques are receiving a lot of attention in robotics. One method, known as swarm shepherding, is founded on the sheep herding behavior exhibited by sheepdogs, where a swarm of relatively simple agents are governed by a shepherd (or shepherds) which is responsible for high-level guidance and planning. Many studies have been conducted on shepherding as a control technique, ranging from the replication of sheep herding via simulation, to the control of uninhabited vehicles and robots for a variety of applications. We present a comprehensive review of the literature on swarm shepherding to reveal the advantages and potential of the approach to be applied to a plethora of robotic systems in the future.
Risk-Sensitive Task Fetching and Offloading for Vehicular Edge Computing
Venue: arXiv cs.NI 2020
Year: 2020

This letter studies an ultra-reliable low latency communication problem focusing on a vehicular edge computing network in which vehicles either fetch and synthesize images recorded by surveillance cameras or acquire the synthesized image from an edge computing server. The notion of risk-sensitive in financial mathematics is leveraged to define a reliability measure, and the studied problem is formulated as a risk minimization problem for each vehicle's end-to-end (E2E) task fetching and offloading delays. Specifically, by resorting to a joint utility and policy estimation-based learning algorithm, a distributed risk-sensitive solution for task fetching and offloading is proposed. Simulation results show that our proposed solution achieves performance improvements up to 40% variance reduction and steeper distribution tail of the E2E delay over an averaged-based baseline.
Fast, Composable Rescue Mission Planning for UAVs using Metric Temporal Logic
Venue: arXiv cs.RO 2020
Year: 2020

We present a hybrid compositional approach for real-time mission planning for multi-rotor unmanned aerial vehicles (UAVs) in a time critical search and rescue scenario. Starting with a known environment, we specify the mission using Metric Temporal Logic (MTL) and use a hybrid dynamical model to capture the various modes of UAV operation. We then divide the mission into several sub-tasks by exploiting the invariant nature of safety and timing constraints along the way, and the different modes (i.e., dynamics) of the UAV. For each sub-task, we translate the MTL specifications into linear constraints and solve the associated optimal control problem for desired path, using a Mixed Integer Linear Program (MILP) solver. The complete path for the mission is constructed recursively by composing the individual optimal sub-paths. We show by simulations that the resulting suboptimal trajectories satisfy the mission specifications, and the proposed approach leads to significant reduction in computational complexity of the problem, making it possible to implement in real-time. Our proposed method ensures the safety of UAVs at all times and guarantees finite time mission completion. It is also shown that our approach scales up nicely for a large number of UAVs.
Nanoscale Microscopy Images Colorization Using Neural Networks
Venue: arXiv cs.CV 2020
Year: 2020

Microscopy images are powerful tools and widely used in the majority of research areas, such as biology, chemistry, physics and materials fields by various microscopies (scanning electron microscope (SEM), atomic force microscope (AFM) and the optical microscope, et al.). However, most of the microscopy images are colorless due to the unique imaging mechanism. Though investigating on some popular solutions proposed recently about colorizing images, we notice the process of those methods are usually tedious, complicated, and time-consuming. In this paper, inspired by the achievement of machine learning algorithms on different science fields, we introduce two artificial neural networks for gray microscopy image colorization: An end-to-end convolutional neural network (CNN) with a pre-trained model for feature extraction and a pixel-to-pixel neural style transfer convolutional neural network (NST-CNN), which can colorize gray microscopy images with semantic information learned from a user-provided colorful image at inference time. The results demonstrate that our algorithm not only can colorize the microscopy images under complex circumstances precisely but also make the color naturally according to the training of a massive number of nature images with proper hue and saturation.
LEO Small-Satellite Constellations for 5G and Beyond-5G Communications
Venue: arXiv cs.NI 2020
Year: 2020

The next frontier towards truly ubiquitous connectivity is the use of Low Earth Orbit (LEO) small-satellite constellations to support 5G and Beyond-5G (B5G) networks. Besides enhanced mobile broadband (eMBB) and massive machine-type communications (mMTC), LEO constellations can support ultra-reliable communications (URC) with relaxed latency requirements of a few tens of milliseconds. Small-satellite impairments and the use of low orbits pose major challenges to the design and performance of these networks, but also open new innovation opportunities. This paper provides a comprehensive overview of the physical and logical links, along with the essential architectural and technological components that enable the full integration of LEO constellations into 5G and B5G systems. Furthermore, we characterize and compare each physical link category and explore novel techniques to maximize the achievable data rates.
Direction Concentration Learning: Enhancing Congruency in Machine Learning
Venue: arXiv cs.LG 2020
Year: 2020

One of the well-known challenges in computer vision tasks is the visual diversity of images, which could result in an agreement or disagreement between the learned knowledge and the visual content exhibited by the current observation. In this work, we first define such an agreement in a concepts learning process as congruency. Formally, given a particular task and sufficiently large dataset, the congruency issue occurs in the learning process whereby the task-specific semantics in the training data are highly varying. We propose a Direction Concentration Learning (DCL) method to improve congruency in the learning process, where enhancing congruency influences the convergence path to be less circuitous. The experimental results show that the proposed DCL method generalizes to state-of-the-art models and optimizers, as well as improves the performances of saliency prediction task, continual learning task, and classification task. Moreover, it helps mitigate the catastrophic forgetting problem in the continual learning task. The code is publicly available at https://github.com/luoyan407/congruency.
Hardness of Network Satisfaction for Relation Algebras with Normal Representations
Venue: arXiv cs.LO 2020
Year: 2020

We study the computational complexity of the general network satisfaction problem for a finite relation algebra $A$ with a normal representation $B$. If $B$ contains a non-trivial equivalence relation with a finite number of equivalence classes, then the network satisfaction problem for $A$ is NP-hard. As a second result, we prove hardness if $B$ has domain size at least three and contains no non-trivial equivalence relations but a symmetric atom $a$ with a forbidden triple $(a,a,a)$, that is, $a \not\leq a \circ a$. We illustrate how to apply our conditions on two small relation algebras.
How India Censors the Web
Venue: arXiv cs.NI 2020
Year: 2020

One of the primary ways in which India engages in online censorship is by ordering Internet Service Providers (ISPs) operating in its jurisdiction to block access to certain websites for its users. This paper reports the different techniques Indian ISPs are using to censor websites, and investigates whether website blocklists are consistent across ISPs. We propose a suite of tests that prove more robust than previous work in detecting DNS and HTTP based censorship. Our tests also discern the use of SNI inspection for blocking websites, which is previously undocumented in the Indian context. Using information from court orders, user reports, and public and leaked government orders, we compile the largest known list of potentially blocked websites in India. We pass this list to our tests and run them from connections of six different ISPs, which together serve more than 98% of Internet users in India. Our findings not only confirm that ISPs are using different techniques to block websites, but also demonstrate that different ISPs are not blocking the same websites.
Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level
Venue: arXiv cs.CR 2020
Year: 2020

The constant-time programming discipline (CT) is an efficient countermeasure against timing side-channel attacks, requiring the control flow and the memory accesses to be independent from the secrets. Yet, writing CT code is challenging as it demands to reason about pairs of execution traces (2- hypersafety property) and it is generally not preserved by the compiler, requiring binary-level analysis. Unfortunately, current verification tools for CT either reason at higher level (C or LLVM), or sacrifice bug-finding or bounded-verification, or do not scale. We tackle the problem of designing an efficient binary-level verification tool for CT providing both bug-finding and bounded-verification. The technique builds on relational symbolic execution enhanced with new optimizations dedicated to information flow and binary-level analysis, yielding a dramatic improvement over prior work based on symbolic execution. We implement a prototype, Binsec/Rel, and perform extensive experiments on a set of 338 cryptographic implementations, demonstrating the benefits of our approach in both bug-finding and bounded-verification. Using Binsec/Rel, we also automate a previous manual study of CT preservation by compilers. Interestingly, we discovered that gcc -O0 and backend passes of clang introduce violations of CT in implementations that were previously deemed secure by a state-of-the-art CT verification tool operating at LLVM level, showing the importance of reasoning at binary-level.
Matrix-Calibration-Based Cascaded Channel Estimation for Reconfigurable Intelligent Surface Assisted Multiuser MIMO
Venue: arXiv cs.IT 2020
Year: 2020

Reconfigurable intelligent surface (RIS) is envisioned to be an essential component of the paradigm for beyond 5G networks as it can potentially provide similar or higher array gains with much lower hardware cost and energy consumption compared with the massive multiple-input multiple-output (MIMO) technology. In this paper, we focus on one of the fundamental challenges, namely the channel acquisition, in an RIS-assisted multiuser MIMO system. The state-of-the-art channel acquisition approach in such a system with fully passive RIS elements estimates the cascaded transmitter-to-RIS and RIS-to-receiver channels by adopting excessively long training sequences. To estimate the cascaded channels with an affordable training overhead, we formulate the channel estimation problem in the RIS-assisted multiuser MIMO system as a matrix-calibration based matrix factorization task. By exploiting the information on the slow-varying channel components and the hidden channel sparsity, we propose a novel message-passing based algorithm to factorize the cascaded channels. Furthermore, we present an analytical framework to characterize the theoretical performance bound of the proposed estimator in the large-system limit. Finally, we conduct simulations to verify the high accuracy and efficiency of the proposed algorithm.
LS-Net: Fast Single-Shot Line-Segment Detector
Venue: arXiv cs.CV 2020
Year: 2020

In low-altitude Unmanned Aerial Vehicle (UAV) flights, power lines are considered as one of the most threatening hazards and one of the most difficult obstacles to avoid. In recent years, many vision-based techniques have been proposed to detect power lines to facilitate self-driving UAVs and automatic obstacle avoidance. However, most of the proposed methods are typically based on a common three-step approach: (i) edge detection, (ii) the Hough transform, and (iii) spurious line elimination based on power line constrains. These approaches not only are slow and inaccurate but also require a huge amount of effort in post-processing to distinguish between power lines and spurious lines. In this paper, we introduce LS-Net, a fast single-shot line-segment detector, and apply it to power line detection. The LS-Net is by design fully convolutional and consists of three modules: (i) a fully convolutional feature extractor, (ii) a classifier, and (iii) a line segment regressor. Due to the unavailability of large datasets with annotations of power lines, we render synthetic images of power lines using the Physically Based Rendering (PBR) approach and propose a series of effective data augmentation techniques to generate more training data. With a customized version of the VGG-16 network as the backbone, the proposed approach outperforms existing state-of-the-art approaches. In addition, the LS-Net can detect power lines in near real-time (20.4 FPS). This suggests that our proposed approach has a promising role in automatic obstacle avoidance and as a valuable component of self-driving UAVs, especially for automatic autonomous power line inspection.
Probabilistic process algebra and strategic interleaving
Venue: arXiv cs.LO 2020
Year: 2020

We first present a probabilistic version of ACP that rests on the principle that probabilistic choices are always resolved before choices involved in alternative composition and parallel composition are resolved and then extend this probabilistic version of ACP with a form of interleaving in which parallel processes are interleaved according to what is known as a process-scheduling policy in the field of operating systems. We use the term strategic interleaving for this more constrained form of interleaving. The extension covers probabilistic process-scheduling policies.
Assessing Practitioner Beliefs about Software Defect Prediction
Venue: arXiv cs.SE 2020
Year: 2020

Just because software developers say they believe in "X", that does not necessarily mean that "X" is true. As shown here, there exist numerous beliefs listed in the recent Software Engineering literature which are only supported by small portions of the available data. Hence we ask what is the source of this disconnect between beliefs and evidence?. To answer this question we look for evidence for ten beliefs within 300,000+ changes seen in dozens of open-source projects. Some of those beliefs had strong support across all the projects; specifically, "A commit that involves more added and removed lines is more bug-prone" and "Files with fewer lines contributed by their owners (who contribute most changes) are bug-prone". Most of the widely-held beliefs studied are only sporadically supported in the data; i.e. large effects can appear in project data and then disappear in subsequent releases. Such sporadic support explains why developers believe things that were relevant to their prior work, but not necessarily their current work. Our conclusion will be that we need to change the nature of the debate with Software Engineering. Specifically, while it is important to report the effects that hold right now, it is also important to report on what effects change over time.
Exploiting Style and Attention in Real-World Super-Resolution
Venue: arXiv cs.CV 2020
Year: 2020

Real-world image super-resolution (SR) is a challenging image translation problem. Low-resolution (LR) images are often generated by various unknown transformations rather than by applying simple bilinear down-sampling on high-resolution (HR) images. To address this issue, this paper proposes a novel pipeline which exploits style and attention mechanism in real-world SR. Our pipeline consists of a style Variational Autoencoder (styleVAE) and a SR network incorporated with attention mechanism. To get real-world-like low-quality images paired with the HR images, we design the styleVAE to transfer the complex nuisance factors in real-world LR images to the generated LR images. We also use mutual information estimation (MI) to get better style information. For our SR network, we firstly propose a global attention residual block to learn long-range dependencies in images. Then another local attention residual block is proposed to enforce the attention of SR network moving to local areas of images in which texture detail will be filled. It is worth noticing that styleVAE can be presented in a plug-and-play manner and thus can help to improve the generalization and robustness of our SR method as well as other SR methods. Extensive experiments demonstrate that our method surpasses the state-of-the-art work, both quantitatively and qualitatively.
Latent Variables on Spheres for Autoencoders in High Dimensions
Venue: arXiv cs.LG 2020
Year: 2020

Variational Auto-Encoder (VAE) has been widely applied as a fundamental generative model in machine learning. For complex samples like imagery objects or scenes, however, VAE suffers from the dimensional dilemma between reconstruction precision that needs high-dimensional latent codes and probabilistic inference that favors a low-dimensional latent space. By virtue of high-dimensional geometry, we propose a very simple algorithm, called Spherical Auto-Encoder (SAE), completely different from existing VAEs to address the issue. SAE is in essence the vanilla autoencoder with spherical normalization on the latent space. We analyze the unique characteristics of random variables on spheres in high dimensions and argue that random variables on spheres are agnostic to various prior distributions and data modes when the dimension is sufficiently high. Therefore, SAE can harness a high-dimensional latent space to improve the inference precision of latent codes while maintain the property of stochastic sampling from priors. The experiments on sampling and inference validate our theoretical analysis and the superiority of SAE.