OpenRaiser/Intern-Atlas huggingface dataset:
Bounded Invariant Checking for Stateflow
Venue: arXiv cs.SE 2022
Year: 2022

Stateflow models are complex software models, often used as part of industrial safety-critical software solutions designed with Matlab Simulink. Being part of safety-critical solutions, these models require the application of rigorous verification techniques for assuring their correctness. In this paper, we propose a refutation-based formal verification approach for analyzing Stateflow models against invariant properties, based on bounded model checking (BMC). The crux of our technique is: i) a representation of the state space of Stateflow models as a symbolic transition system (STS) over the symbolic configurations of the model, and ii) application of incremental BMC, to generate verification results after each unrolling of the next-state relation of the transition system. To this end, we develop a symbolic structural operational semantics (SSOS) for Stateflow, starting from an existing structural operational semantics (SOS), and show the preservation of invariant properties between the two. We define bounded invariant checking for STS over symbolic configurations as a satisfiability problem. We develop an automated procedure for generating the initial and next-state predicates of the STS, and a prototype implementation of the technique in the form of a tool utilising standard, off-the-shelf satisfiability solvers. Finally, we present preliminary performance results by applying our tool on an illustrative example and two industrial models.
Towards Adaptive Planning of Assistive-care Robot Tasks
Venue: arXiv cs.RO 2022
Year: 2022

This 'research preview' paper introduces an adaptive path planning framework for robotic mission execution in assistive-care applications. The framework provides a graph-based environment modelling approach, with dynamic path finding performed using Dijkstra's algorithm. A predictive module that uses probabilistic model checking is applied to estimate the human's movement through the environment, allowing run-time re-planning of the robot's path. We illustrate the use of the framework for a simulated assistive-care case study in which a mobile robot navigates through the environment and monitors an end user with mild physical or cognitive impairments.
Extending Attack-Fault Trees with Runtime Verification
Venue: arXiv cs.SE 2022
Year: 2022

Autonomous systems are often complex and prone to software failures and cyber-attacks. We introduce RVAFTs, an extension of Attack-Fault Trees (AFTs) with runtime events that can be used to construct runtime monitors. These monitors are able to detect when failures, that can be caused either by an attack or by a fault, occur. The safety and security properties monitored are, in turn, derived from the hierarchical decomposition of RVAFTs. Our approach not only provides further use of AFTs, but also improves the process of instrumentation often required in runtime verification. We explain the principles and provide a simple case study demonstrating how RVAFTs can be used in practice. Through this we are also able to evaluate the detection of faults and attacks as well as assessing the computational overhead of the monitors.
Accelerating netty-based applications through transparent InfiniBand support
Venue: arXiv cs.NI 2022
Year: 2022

Many big-data frameworks are written in Java, e.g. Apache Spark, Flink and Cassandra. These systems use the networking framework netty which is based on Java NIO. While this allows for fast networking on traditional Ethernet networks, it cannot fully exploit the whole performance of modern interconnects, like InfiniBand, providing bandwidths of 100 Gbit/s and more. In this paper we propose netty support for hadroNIO, a Java library, providing transparent InfiniBand support for Java applications based on NIO. hadroNIO is based on UCX, which supports several interconnects, including InfiniBand. We present hadroNIO extensions and optimizations for supporting netty. The evaluations with microbenchmarks, covering single- and multi-threaded scenarios, show that it is possible for netty applications to reach round-trip times as low as 5 us and fully utilize the 100 Gbit/s bandwidth of high-speed NICs, without changing the application's source code. We also compare hadroNIO with traditional sockets, as well as libvma and the results show, that hadroNIO offers a substantial improvement over plain sockets and can outperform libvma in several scenarios.
Worst-case Deterministic Fully-Dynamic Planar 2-vertex Connectivity
Venue: arXiv cs.DS 2022
Year: 2022

We study dynamic planar graphs with $n$ vertices, subject to edge deletion, edge contraction, edge insertion across a face, and the splitting of a vertex in specified corners. We dynamically maintain a combinatorial embedding of such a planar graph, subject to connectivity and $2$-vertex-connectivity (biconnectivity) queries between pairs of vertices. Whenever a query pair is connected and not biconnected, we find the first and last cutvertex separating them. Additionally, we allow local changes to the embedding by flipping the embedding of a subgraph that is connected by at most two vertices to the rest of the graph. We support all queries and updates in deterministic, worst-case, $O(\log^2 n)$ time, using an $O(n)$-sized data structure. Previously, the best bound for fully-dynamic planar biconnectivity (subject to our set of operations) was an amortised $\tilde{O}(\log^3 n)$ for general graphs, and algorithms with worst-case polylogarithmic update times were known only in the partially dynamic (insertion-only or deletion-only) setting.
How unitizing affects annotation of cohesion
Venue: arXiv cs.HC 2022
Year: 2022

This paper investigates how unitizing affects external observers' annotation of group cohesion. We compared unitizing techniques belonging to these categories: interval coding, continuous coding, and a technique inspired by a cognitive theory on event perception. We applied such techniques for sampling coding units from a set of recordings of social interactions rich in behaviors related to cohesion. Then, we compared the cohesion scores the observers assigned to each coding unit. Results show that the three techniques can lead to suitable ratings and that the technique inspired to cognitive theories leads to scores reflecting variability in cohesion better than the other ones.
Secure Indoor Location for Airport Environments
Venue: arXiv cs.CR 2022
Year: 2022

This work presents a secure novel solution based on inertial measurement units to provide indoor location and positioning in airports. The use of different technologies allows to locate people with precision in this kind of indoor places where the use of the GPS is not possible. The system has been developed thinking in the low cost and in a possible future expansion of this kind of systems to improve the Quality of Service of the users in airports. The use of QR codes and low cost IMU devices through the use of people smartphones ensure this premise. An Android application has been developed to show the applicability and performance of the system. The security in this kind of systems is essential. This kind of systems needs to avoid the traceability of the IMU devices when users are using it. To solve this problem, the FourQ elliptic curve has been used to generate a shared key using the elliptic curve Diffie-Hellman protocol. The key generated with the FourQ is used then to cipher all communications through the use of the SNOW 3G stream cipher. The developed system offers promising results.
Road Rutting Detection using Deep Learning on Images
Venue: arXiv cs.CV 2022
Year: 2022

Road rutting is a severe road distress that can cause premature failure of road incurring early and costly maintenance costs. Research on road damage detection using image processing techniques and deep learning are being actively conducted in the past few years. However, these researches are mostly focused on detection of cracks, potholes, and their variants. Very few research has been done on the detection of road rutting. This paper proposes a novel road rutting dataset comprising of 949 images and provides both object level and pixel level annotations. Object detection models and semantic segmentation models were deployed to detect road rutting on the proposed dataset, and quantitative and qualitative analysis of model predictions were done to evaluate model performance and identify challenges faced in the detection of road rutting using the proposed method. Object detection model YOLOX-s achieves mAP@IoU=0.5 of 61.6% and semantic segmentation model PSPNet (Resnet-50) achieves IoU of 54.69 and accuracy of 72.67, thus providing a benchmark accuracy for similar work in future. The proposed road rutting dataset and the results of our research study will help accelerate the research on detection of road rutting using deep learning.
A Closer Look at Evaluating the Bit-Flip Attack Against Deep Neural Networks
Venue: arXiv cs.CR 2022
Year: 2022

Deep neural network models are massively deployed on a wide variety of hardware platforms. This results in the appearance of new attack vectors that significantly extend the standard attack surface, extensively studied by the adversarial machine learning community. One of the first attack that aims at drastically dropping the performance of a model, by targeting its parameters (weights) stored in memory, is the Bit-Flip Attack (BFA). In this work, we point out several evaluation challenges related to the BFA. First of all, the lack of an adversary's budget in the standard threat model is problematic, especially when dealing with physical attacks. Moreover, since the BFA presents critical variability, we discuss the influence of some training parameters and the importance of the model architecture. This work is the first to present the impact of the BFA against fully-connected architectures that present different behaviors compared to convolutional neural networks. These results highlight the importance of defining robust and sound evaluation methodologies to properly evaluate the dangers of parameter-based attacks as well as measure the real level of robustness offered by a defense.
Physics-aware Differentiable Discrete Codesign for Diffractive Optical Neural Networks
Venue: arXiv cs.AI 2022
Year: 2022

Diffractive optical neural networks (DONNs) have attracted lots of attention as they bring significant advantages in terms of power efficiency, parallelism, and computational speed compared with conventional deep neural networks (DNNs), which have intrinsic limitations when implemented on digital platforms. However, inversely mapping algorithm-trained physical model parameters onto real-world optical devices with discrete values is a non-trivial task as existing optical devices have non-unified discrete levels and non-monotonic properties. This work proposes a novel device-to-system hardware-software codesign framework, which enables efficient physics-aware training of DONNs w.r.t arbitrary experimental measured optical devices across layers. Specifically, Gumbel-Softmax is employed to enable differentiable discrete mapping from real-world device parameters into the forward function of DONNs, where the physical parameters in DONNs can be trained by simply minimizing the loss function of the ML task. The results have demonstrated that our proposed framework offers significant advantages over conventional quantization-based methods, especially with low-precision optical devices. Finally, the proposed algorithm is fully verified with physical experimental optical systems in low-precision settings.
Happy or grumpy? A Machine Learning Approach to Analyze the Sentiment of Airline Passengers' Tweets
Venue: arXiv cs.CL 2022
Year: 2022

As one of the most extensive social networking services, Twitter has more than 300 million active users as of 2022. Among its many functions, Twitter is now one of the go-to platforms for consumers to share their opinions about products or experiences, including flight services provided by commercial airlines. This study aims to measure customer satisfaction by analyzing sentiments of Tweets that mention airlines using a machine learning approach. Relevant Tweets are retrieved from Twitter's API and processed through tokenization and vectorization. After that, these processed vectors are passed into a pre-trained machine learning classifier to predict the sentiments. In addition to sentiment analysis, we also perform lexical analysis on the collected Tweets to model keywords' frequencies, which provide meaningful contexts to facilitate the interpretation of sentiments. We then apply time series methods such as Bollinger Bands to detect abnormalities in sentiment data. Using historical records from January to July 2022, our approach is proven to be capable of capturing sudden and significant changes in passengers' sentiment. This study has the potential to be developed into an application that can help airlines, along with several other customer-facing businesses, efficiently detect abrupt changes in customers' sentiments and take adequate measures to counteract them.
Feature Decoupling in Self-supervised Representation Learning for Open Set Recognition
Venue: arXiv cs.CV 2022
Year: 2022

Assuming unknown classes could be present during classification, the open set recognition (OSR) task aims to classify an instance into a known class or reject it as unknown. In this paper, we use a two-stage training strategy for the OSR problems. In the first stage, we introduce a self-supervised feature decoupling method that finds the content features of the input samples from the known classes. Specifically, our feature decoupling approach learns a representation that can be split into content features and transformation features. In the second stage, we fine-tune the content features with the class labels. The fine-tuned content features are then used for the OSR problems. Moreover, we consider an unsupervised OSR scenario, where we cluster the content features learned from the first stage. To measure representation quality, we introduce intra-inter ratio (IIR). Our experimental results indicate that our proposed self-supervised approach outperforms others in image and malware OSR problems. Also, our analyses indicate that IIR is correlated with OSR performance.
Efficient parameterized algorithms on graphs with heterogeneous structure: Combining tree-depth and modular-width
Venue: arXiv cs.DS 2022
Year: 2022

Many computational problems admit fast algorithms on special inputs, however, the required properties might be quite restrictive. E.g., many graph problems can be solved much faster on interval or cographs, or on graphs of small modular-width or small tree-width, than on general graphs. One challenge is to attain the greatest generality of such results, i.e., being applicable to less restrictive input classes, without losing much in terms of running time. Building on the use of algebraic expressions we present a clean and robust way of combining such homogeneous structure into more complex heterogeneous structure, and we show-case this for the combination of modular-width, tree-depth, and a natural notion of modular tree-depth. We give a generic framework for designing efficient parameterized algorithms on the created graph classes, aimed at getting competitive running times that match the homogeneous cases. To show the applicability we give efficient parameterized algorithms for Negative Cycle Detection, Vertex-Weighted All-Pairs Shortest Paths, and Triangle Counting.
Lazy Probabilistic Roadmaps Revisited
Venue: arXiv cs.RO 2022
Year: 2022

This paper describes a revision of the classic Lazy Probabilistic Roadmaps algorithm (Lazy PRM), that results from pairing PRM and a novel Branch-and-Cut (BC) algorithm. Cuts are dynamically generated constraints that are imposed on minimum cost paths over the geometric graphs selected by PRM. Cuts eliminate paths that cannot be mapped into smooth plans that satisfy suitably defined kinematic constraints. We generate candidate smooth plans by fitting splines to vertices in minimum-cost path. Plans are validated with a recently proposed algorithm that maps them into finite traces, without need to choose a fixed discretization step. Trace elements exactly describe when plans cross constraint boundaries modulo arithmetic precision. We evaluate several planners using our methods over the recently proposed BARN benchmark, and we report evidence of the scalability of our approach.
Re-Imagen: Retrieval-Augmented Text-to-Image Generator
Venue: arXiv cs.CV 2022
Year: 2022

Research on text-to-image generation has witnessed significant progress in generating diverse and photo-realistic images, driven by diffusion and auto-regressive models trained on large-scale image-text data. Though state-of-the-art models can generate high-quality images of common entities, they often have difficulty generating images of uncommon entities, such as `Chortai (dog)' or `Picarones (food)'. To tackle this issue, we present the Retrieval-Augmented Text-to-Image Generator (Re-Imagen), a generative model that uses retrieved information to produce high-fidelity and faithful images, even for rare or unseen entities. Given a text prompt, Re-Imagen accesses an external multi-modal knowledge base to retrieve relevant (image, text) pairs and uses them as references to generate the image. With this retrieval step, Re-Imagen is augmented with the knowledge of high-level semantics and low-level visual details of the mentioned entities, and thus improves its accuracy in generating the entities' visual appearances. We train Re-Imagen on a constructed dataset containing (image, text, retrieval) triples to teach the model to ground on both text prompt and retrieval. Furthermore, we develop a new sampling strategy to interleave the classifier-free guidance for text and retrieval conditions to balance the text and retrieval alignment. Re-Imagen achieves significant gain on FID score over COCO and WikiImage. To further evaluate the capabilities of the model, we introduce EntityDrawBench, a new benchmark that evaluates image generation for diverse entities, from frequent to rare, across multiple object categories including dogs, foods, landmarks, birds, and characters. Human evaluation on EntityDrawBench shows that Re-Imagen can significantly improve the fidelity of generated images, especially on less frequent entities.
Tourism's trend Ranking on Social Media Data Using Fuzzy-AHP vs. AHP
Venue: arXiv cs.SI 2022
Year: 2022

Tourism is an exciting thing to be visited by people in the world. Search for attractive and popular places can be done through social media. Data from social media or websites can be used as a reference to find current travel trends and get information about reviews, stories, likes, forums, blogs, and feedback from a place. However, if the search is done manually one by one, it takes a long time, and it becomes interesting to do research. So, searching based on current trends will be easier and faster. For this reason, this study uses a computer base to search by ranking tourist facilities from social media data or websites using the multi-criteria decision-making (MCDM) method. The implementation of the method used in finding the trend is the Fuzzy-AHP method in comparison with the AHP. The data used is data reviews, stories, likes, forums, blogs, and feedback from the web or social media. Because with these components, tourism can be developed according to visitors\'' wishes. The research aims to rank facilities\'' tourism attractions (trends) and development priorities. The priority and ranking used the fuzzy-AHP and AHP method to determine weight criteria and the ranking process. The highest ranking is on the Parks/Picnic Spots attraction, and make it a priority to develop. The methods have an average value MSE of all data is \approx 0.0002, which can be used for this ranking.
Spatial Moment Pooling Improves Neural Image Assessment
Venue: arXiv cs.CV 2022
Year: 2022

In recent years, there has been widespread attention drawn to convolutional neural network (CNN) based blind image quality assessment (IQA). A large number of works start by extracting deep features from CNN. Then, those features are processed through spatial average pooling (SAP) and fully connected layers to predict quality. Inspired by full reference IQA and texture features, in this paper, we extend SAP ($1^{st}$ moment) into spatial moment pooling (SMP) by incorporating higher order moments (such as variance, skewness). Moreover, we provide learning friendly normalization to circumvent numerical issue when computing gradients of higher moments. Experimental results suggest that simply upgrading SAP to SMP significantly enhances CNN-based blind IQA methods and achieves state of the art performance.
Bayesian Neural Network Versus Ex-Post Calibration For Prediction Uncertainty
Venue: arXiv cs.LG 2022
Year: 2022

Probabilistic predictions from neural networks which account for predictive uncertainty during classification is crucial in many real-world and high-impact decision making settings. However, in practice most datasets are trained on non-probabilistic neural networks which by default do not capture this inherent uncertainty. This well-known problem has led to the development of post-hoc calibration procedures, such as Platt scaling (logistic), isotonic and beta calibration, which transforms the scores into well calibrated empirical probabilities. A plausible alternative to the calibration approach is to use Bayesian neural networks, which directly models a predictive distribution. Although they have been applied to images and text datasets, they have seen limited adoption in the tabular and small data regime. In this paper, we demonstrate that Bayesian neural networks yields competitive performance when compared to calibrated neural networks and conduct experiments across a wide array of datasets.
Dataset Distillation for Medical Dataset Sharing
Venue: arXiv cs.CR 2022
Year: 2022

Sharing medical datasets between hospitals is challenging because of the privacy-protection problem and the massive cost of transmitting and storing many high-resolution medical images. However, dataset distillation can synthesize a small dataset such that models trained on it achieve comparable performance with the original large dataset, which shows potential for solving the existing medical sharing problems. Hence, this paper proposes a novel dataset distillation-based method for medical dataset sharing. Experimental results on a COVID-19 chest X-ray image dataset show that our method can achieve high detection performance even using scarce anonymized chest X-ray images.
Tensor-Based Sketching Method for the Low-Rank Approximation of Data Streams
Venue: arXiv cs.DS 2022
Year: 2022

Low-rank approximation in data streams is a fundamental and significant task in computing science, machine learning and statistics. Multiple streaming algorithms have emerged over years and most of them are inspired by randomized algorithms, more specifically, sketching methods. However, many algorithms are not able to leverage information of data streams and consequently suffer from low accuracy. Existing data-driven methods improve accuracy but the training cost is expensive in practice. In this paper, from a subspace perspective, we propose a tensor-based sketching method for low-rank approximation of data streams. The proposed algorithm fully exploits the structure of data streams and obtains quasi-optimal sketching matrices by performing tensor decomposition on training data. A series of experiments are carried out and show that the proposed tensor-based method can be more accurate and much faster than the previous work.