OpenRaiser/Intern-Atlas huggingface dataset:
Some Common Mistakes in the Teaching and Textbooks of Modal Logic
Venue: arXiv cs.LO 2020
Year: 2020

We discuss four common mistakes in the teaching and textbooks of modal logic. The first one is missing the axiom $\Diamondφ\leftrightarrow\neg\Box\negφ$, when choosing $\Diamond$ as the primitive modal operator, misunderstanding that $\Box$ and $\Diamond$ are symmetric. The second one is forgetting to make the set of formulas for filtration closed under subformulas, when proving the finite model property through filtration, neglecting that $\Boxφ$ and $\Diamondφ$ may be abbreviations of formulas. The third one is giving wrong definitions of canonical relations in minimal canonical models that are unmatched with the primitive modal operators. The final one is misunderstanding the rule of necessitation, without knowing its distinction from the rule of modus ponens. To better understand the rule of necessitation, we summarize six ways of defining deductive consequence in modal logic: omitted definition, classical definition, ternary definition, reduced definition, bounded definition, and deflationary definition, and show that the last three definitions are equivalent to each other.
NR V2X Communications at Millimeter Waves: An End-to-End Performance Evaluation
Venue: arXiv cs.NI 2020
Year: 2020

3GPP NR V2X represents the new 3GPP standard for next-generation vehicular systems which, among other innovations, supports vehicle-to-vehicle (V2V) operations in the millimeter wave (mmWave) spectrum to address the communication requirements of future intelligent automotive networks. While mmWaves will enable massive data rates and low latency, the propagation characteristics at very high frequencies become very challenging, thereby calling for accurate performance evaluations as a means to properly assess the performance of such systems. Along these lines, in this paper MilliCar, the new ns-3 module based on the latest NR V2X specifications, is used to provide an end-to-end performance evaluation of mmWave V2V networks. We investigate the impact of different propagation scenarios and system parameters, including the inter-vehicle distance, the adopted frame numerology, and the modulation and coding scheme, and provide guidelines towards the most promising V2V deployment configurations.
An Empirical Study of User Support Tools in Open Source Software
Venue: arXiv cs.SE 2020
Year: 2020

End users positive response is essential for the success of any software. This is true for both commercial and Open Source Software (OSS). OSS is popular not only because of its availability, which is usually free but due to the user support it provides, generally through public platforms. The study model of this research establishes a relationship between OSS user support and available support tools. To conduct this research, we used a dataset of 100 OSS projects in different categories and examined five user support tools provided by different OSS projects. The results show that project trackers, user mailing lists, and updated versions have a significant role in gaining user support. However, we were unable to find a significant association between user support and documentation, as well as between user support and the troubleshooting guidelines provided by OSS projects.
Finite-sample Analysis of Greedy-GQ with Linear Function Approximation under Markovian Noise
Venue: arXiv cs.LG 2020
Year: 2020

Greedy-GQ is an off-policy two timescale algorithm for optimal control in reinforcement learning. This paper develops the first finite-sample analysis for the Greedy-GQ algorithm with linear function approximation under Markovian noise. Our finite-sample analysis provides theoretical justification for choosing stepsizes for this two timescale algorithm for faster convergence in practice, and suggests a trade-off between the convergence rate and the quality of the obtained policy. Our paper extends the finite-sample analyses of two timescale reinforcement learning algorithms from policy evaluation to optimal control, which is of more practical interest. Specifically, in contrast to existing finite-sample analyses for two timescale methods, e.g., GTD, GTD2 and TDC, where their objective functions are convex, the objective function of the Greedy-GQ algorithm is non-convex. Moreover, the Greedy-GQ algorithm is also not a linear two-timescale stochastic approximation algorithm. Our techniques in this paper provide a general framework for finite-sample analysis of non-convex value-based reinforcement learning algorithms for optimal control.
Do we need a Contact Tracing App?
Venue: arXiv cs.CY 2020
Year: 2020

The goal of this paper is to shed some light on the usefulness of a contact tracing smartphone app for the containment of the COVID-19 pandemic. We review the basics of contact tracing during the spread of a virus, we contextualize the numbers to the case of COVID-19 and we analyse the state of the art for proximity detection using Bluetooth Low Energy. Our contribution is to assess if there is scientific evidence of the benefit of a contact tracing app in slowing down the spread of the virus using present technologies. Our conclusion is that such evidence is lacking, and we should re-think the introduction of such a privacy-invasive measure.
A refinement checking based strategy for component-based systems evolution
Venue: arXiv cs.SE 2020
Year: 2020

We propose inheritance and refinement relations for a CSP-based component model (BRIC), which supports a constructive design based on composition rules that preserve classical concurrency properties such as deadlock freedom. The proposed relations allow extension of functionality, whilst preserving behavioural properties. A notion of extensibility is defined on top of a behavioural relation called convergence, which distinguishes inputs from outputs and the context where they are communicated, allowing extensions to reuse existing events with different purposes. We mechanise the strategy for extensibility verification using the FDR4 tool, and illustrate our results with an autonomous healthcare robot case study.
Causality, Responsibility and Blame in Team Plans
Venue: arXiv cs.AI 2020
Year: 2020

Many objectives can be achieved (or may be achieved more effectively) only by a group of agents executing a team plan. If a team plan fails, it is often of interest to determine what caused the failure, the degree of responsibility of each agent for the failure, and the degree of blame attached to each agent. We show how team plans can be represented in terms of structural equations, and then apply the definitions of causality introduced by Halpern [2015] and degree of responsibility and blame introduced by Chockler and Halpern [2004] to determine the agent(s) who caused the failure and what their degree of responsibility/blame is. We also prove new results on the complexity of computing causality and degree of responsibility and blame, showing that they can be determined in polynomial time for many team plans of interest.
Consensus Driven Learning
Venue: arXiv cs.LG 2020
Year: 2020

As the complexity of our neural network models grow, so too do the data and computation requirements for successful training. One proposed solution to this problem is training on a distributed network of computational devices, thus distributing the computational and data storage loads. This strategy has already seen some adoption by the likes of Google and other companies. In this paper we propose a new method of distributed, decentralized learning that allows a network of computation nodes to coordinate their training using asynchronous updates over an unreliable network while only having access to a local dataset. This is achieved by taking inspiration from Distributed Averaging Consensus algorithms to coordinate the various nodes. Sharing the internal model instead of the training data allows the original raw data to remain with the computation node. The asynchronous nature and lack of centralized coordination allows this paradigm to function with limited communication requirements. We demonstrate our method on the MNIST, Fashion MNIST, and CIFAR10 datasets. We show that our coordination method allows models to be learned on highly biased datasets, and in the presence of intermittent communication failure.
Formal Specification and Verification of Solidity Contracts with Events
Venue: arXiv cs.PL 2020
Year: 2020

Events in the Solidity language provide a means of communication between the on-chain services of decentralized applications and the users of those services. Events are commonly used as an abstraction of contract execution that is relevant from the users' perspective. Users must, therefore, be able to understand the meaning and trust the validity of the emitted events. This paper presents a source-level approach for the formal specification and verification of Solidity contracts with the primary focus on events. Our approach allows specification of events in terms of the on-chain data that they track, and predicates that define the correspondence between the blockchain state and the abstract view provided by the events. The approach is implemented in solc-verify, a modular verifier for Solidity, and we demonstrate its applicability with various examples.
Tracking Measurement Obfuscations from SourceURL
Venue: arXiv cs.CR 2020
Year: 2020

Tracking scripts can use the sourceURL directive to mask their origin from developer tools and tools that use the same JS call stack and network stack information. Firefox and Chromium appear to be affected. Firefox 78 now includes a preference to disable this behavior. This short paper describes the effect when using the OpenWPM measurement platform along with details of discovery.
Stance Prediction and Claim Verification: An Arabic Perspective
Venue: arXiv cs.CL 2020
Year: 2020

This work explores the application of textual entailment in news claim verification and stance prediction using a new corpus in Arabic. The publicly available corpus comes in two perspectives: a version consisting of 4,547 true and false claims and a version consisting of 3,786 pairs (claim, evidence). We describe the methodology for creating the corpus and the annotation process. Using the introduced corpus, we also develop two machine learning baselines for two proposed tasks: claim verification and stance prediction. Our best model utilizes pretraining (BERT) and achieves 76.7 F1 on the stance prediction task and 64.3 F1 on the claim verification task. Our preliminary experiments shed some light on the limits of automatic claim verification that relies on claims text only. Results hint that while the linguistic features and world knowledge learned during pretraining are useful for stance prediction, such learned representations from pretraining are insufficient for verifying claims without access to context or evidence.
Analysis of misinformation during the COVID-19 outbreak in China: cultural, social and political entanglements
Venue: arXiv cs.SI 2020
Year: 2020

COVID-19 resulted in an infodemic, which could erode public trust, impede virus containment, and outlive the pandemic itself. The evolving and fragmented media landscape is a key driver of the spread of misinformation. Using misinformation identified by the fact-checking platform by Tencent and posts on Weibo, our results showed that the evolution of misinformation follows an issue-attention cycle, pertaining to topics such as city lockdown, cures, and preventions, and school reopening. Sources of authority weigh in on these topics, but their influence is complicated by peoples' pre-existing beliefs and cultural practices. Finally, social media has a complicated relationship with established or legacy media systems. Sometimes they reinforce each other, but in general, social media may have a topic cycle of its own making. Our findings shed light on the distinct characteristics of misinformation during the COVID-19 and offer insights into combating misinformation in China and across the world at large.
Deep Learning-Based Automated Image Segmentation for Concrete Petrographic Analysis
Venue: arXiv cs.CV 2020
Year: 2020

The standard petrography test method for measuring air voids in concrete (ASTM C457) requires a meticulous and long examination of sample phase composition under a stereomicroscope. The high expertise and specialized equipment discourage this test for routine concrete quality control. Though the task can be alleviated with the aid of color-based image segmentation, additional surface color treatment is required. Recently, deep learning algorithms using convolutional neural networks (CNN) have achieved unprecedented segmentation performance on image testing benchmarks. In this study, we investigated the feasibility of using CNN to conduct concrete segmentation without the use of color treatment. The CNN demonstrated a strong potential to process a wide range of concretes, including those not involved in model training. The experimental results showed that CNN outperforms the color-based segmentation by a considerable margin, and has comparable accuracy to human experts. Furthermore, the segmentation time is reduced to mere seconds.
Unsupposable Test-data Generation for Machine-learned Software
Venue: arXiv cs.SE 2020
Year: 2020

As for software development by machine learning, a trained model is evaluated by using part of an existing dataset as test data. However, if data with characteristics that differ from the existing data is input, the model does not always behave as expected. Accordingly, to confirm the behavior of the model more strictly, it is necessary to create data that differs from the existing data and test the model with that different data. The data to be tested includes not only data that developers can suppose (supposable data) but also data they cannot suppose (unsupposable data). To confirm the behavior of the model strictly, it is important to create as much unsupposable data as possible. In this study, therefore, a method called "unsupposable test-data generation" (UTG)---for giving suggestions for unsupposable data to model developers and testers---is proposed. UTG uses a variational autoencoder (VAE) to generate unsupposable data. The unsupposable data is generated by acquiring latent values with low occurrence probability in the prior distribution of the VAE and inputting the acquired latent values into the decoder. If unsupposable data is included in the data generated by the decoder, the developer can recognize new unsupposable features by referring to the data. On the basis of those unsupposable features, the developer will be able to create other unsupposable data with the same features. The proposed UTG was applied to the MNIST dataset and the House Sales Price dataset. The results demonstrate the feasibility of UTG.
Symptom extraction from the narratives of personal experiences with COVID-19 on Reddit
Venue: arXiv cs.CL 2020
Year: 2020

Social media discussion of COVID-19 provides a rich source of information into how the virus affects people's lives that is qualitatively different from traditional public health datasets. In particular, when individuals self-report their experiences over the course of the virus on social media, it can allow for identification of the emotions each stage of symptoms engenders in the patient. Posts to the Reddit forum r/COVID19Positive contain first-hand accounts from COVID-19 positive patients, giving insight into personal struggles with the virus. These posts often feature a temporal structure indicating the number of days after developing symptoms the text refers to. Using topic modelling and sentiment analysis, we quantify the change in discussion of COVID-19 throughout individuals' experiences for the first 14 days since symptom onset. Discourse on early symptoms such as fever, cough, and sore throat was concentrated towards the beginning of the posts, while language indicating breathing issues peaked around ten days. Some conversation around critical cases was also identified and appeared at a roughly constant rate. We identified two clear clusters of positive and negative emotions associated with the evolution of these symptoms and mapped their relationships. Our results provide a perspective on the patient experience of COVID-19 that complements other medical data streams and can potentially reveal when mental health issues might appear.
Application Management in Fog Computing Environments: A Taxonomy, Review and Future Directions
Venue: arXiv cs.DC 2020
Year: 2020

The Internet of Things (IoT) paradigm is being rapidly adopted for the creation of smart environments in various domains. The IoT-enabled Cyber-Physical Systems (CPSs) associated with smart city, healthcare, Industry 4.0 and Agtech handle a huge volume of data and require data processing services from different types of applications in real-time. The Cloud-centric execution of IoT applications barely meets such requirements as the Cloud datacentres reside at a multi-hop distance from the IoT devices. \textit{Fog computing}, an extension of Cloud at the edge network, can execute these applications closer to data sources. Thus, Fog computing can improve application service delivery time and resist network congestion. However, the Fog nodes are highly distributed, heterogeneous and most of them are constrained in resources and spatial sharing. Therefore, efficient management of applications is necessary to fully exploit the capabilities of Fog nodes. In this work, we investigate the existing application management strategies in Fog computing and review them in terms of architecture, placement and maintenance. Additionally, we propose a comprehensive taxonomy and highlight the research gaps in Fog-based application management. We also discuss a perspective model and provide future research directions for further improvement of application management in Fog computing.
Simplified Self-Attention for Transformer-based End-to-End Speech Recognition
Venue: arXiv cs.SD 2020
Year: 2020

Transformer models have been introduced into end-to-end speech recognition with state-of-the-art performance on various tasks owing to their superiority in modeling long-term dependencies. However, such improvements are usually obtained through the use of very large neural networks. Transformer models mainly include two submodules - position-wise feedforward layers and self-attention (SAN) layers. In this paper, to reduce the model complexity while maintaining good performance, we propose a simplified self-attention (SSAN) layer which employs FSMN memory block instead of projection layers to form query and key vectors for transformer-based end-to-end speech recognition. We evaluate the SSAN-based and the conventional SAN-based transformers on the public AISHELL-1, internal 1000-hour and 20,000-hour large-scale Mandarin tasks. Results show that our proposed SSAN-based transformer model can achieve over 20% relative reduction in model parameters and 6.7% relative CER reduction on the AISHELL-1 task. With impressively 20% parameter reduction, our model shows no loss of recognition performance on the 20,000-hour large-scale task.
Pairwise Supervised Hashing with Bernoulli Variational Auto-Encoder and Self-Control Gradient Estimator
Venue: arXiv cs.LG 2020
Year: 2020

Semantic hashing has become a crucial component of fast similarity search in many large-scale information retrieval systems, in particular, for text data. Variational auto-encoders (VAEs) with binary latent variables as hashing codes provide state-of-the-art performance in terms of precision for document retrieval. We propose a pairwise loss function with discrete latent VAE to reward within-class similarity and between-class dissimilarity for supervised hashing. Instead of solving the optimization relying on existing biased gradient estimators, an unbiased low-variance gradient estimator is adopted to optimize the hashing function by evaluating the non-differentiable loss function over two correlated sets of binary hashing codes to control the variance of gradient estimates. This new semantic hashing framework achieves superior performance compared to the state-of-the-arts, as demonstrated by our comprehensive experiments.
A Robust Interpretable Deep Learning Classifier for Heart Anomaly Detection Without Segmentation
Venue: arXiv cs.SD 2020
Year: 2020

Traditionally, abnormal heart sound classification is framed as a three-stage process. The first stage involves segmenting the phonocardiogram to detect fundamental heart sounds; after which features are extracted and classification is performed. Some researchers in the field argue the segmentation step is an unwanted computational burden, whereas others embrace it as a prior step to feature extraction. When comparing accuracies achieved by studies that have segmented heart sounds before analysis with those who have overlooked that step, the question of whether to segment heart sounds before feature extraction is still open. In this study, we explicitly examine the importance of heart sound segmentation as a prior step for heart sound classification, and then seek to apply the obtained insights to propose a robust classifier for abnormal heart sound detection. Furthermore, recognizing the pressing need for explainable Artificial Intelligence (AI) models in the medical domain, we also unveil hidden representations learned by the classifier using model interpretation techniques. Experimental results demonstrate that the segmentation plays an essential role in abnormal heart sound classification. Our new classifier is also shown to be robust, stable and most importantly, explainable, with an accuracy of almost 100% on the widely used PhysioNet dataset.
Privacy Preserving Face Recognition Utilizing Differential Privacy
Venue: arXiv cs.CR 2020
Year: 2020

Facial recognition technologies are implemented in many areas, including but not limited to, citizen surveillance, crime control, activity monitoring, and facial expression evaluation. However, processing biometric information is a resource-intensive task that often involves third-party servers, which can be accessed by adversaries with malicious intent. Biometric information delivered to untrusted third-party servers in an uncontrolled manner can be considered a significant privacy leak (i.e. uncontrolled information release) as biometrics can be correlated with sensitive data such as healthcare or financial records. In this paper, we propose a privacy-preserving technique for "controlled information release", where we disguise an original face image and prevent leakage of the biometric features while identifying a person. We introduce a new privacy-preserving face recognition protocol named PEEP (Privacy using EigEnface Perturbation) that utilizes local differential privacy. PEEP applies perturbation to Eigenfaces utilizing differential privacy and stores only the perturbed data in the third-party servers to run a standard Eigenface recognition algorithm. As a result, the trained model will not be vulnerable to privacy attacks such as membership inference and model memorization attacks. Our experiments show that PEEP exhibits a classification accuracy of around 70% - 90% under standard privacy settings.