The analysis of electrocardiogram (ECG) signals are among the key factors in the diagnosis of cardiovascular diseases (CVDs). However, automatic processing of ECG in clinical practice is still restrained by the accuracy of existing algorithms. Deep learning methods have recently achieved striking success in a variety of task including predictive healthcare. Graph neural networks are a class of machine learning algorithms which can learn by directly extracting important information from graph-structured data, and perform prediction on unknown data. Such algorithms are suitable for mining complex graph data, deducing useful predictions. In this work, we present a Graph Neural Network (GNN) model trained in two datasets with more than 107,000 single-lead signal images extracted from laboratories of Boston’s Beth Israel Hospital and of the Massachusetts Institute of Technology (MITBIH), and 1.5 million labeled exams analyzed by the Physikalisch-Technische Bundesanstalt (PTB). Our proposed GNN achieves promising performance, i.e., the results show that ECG classification based on GNNs using either single-lead or 12-lead setup is closer to the human-level in standard clinical practice. By several testing instances, the proposed approach obtains an accuracy of 1.0, thereby outperforming various state-of-the-art baselines by both databases with respect to effectiveness and timing efficiency. We anticipate that the approach can be deployed as a non-invasive pre-screening tool to assist doctors in real-time monitoring and performing their diagnosis activities.

Abstract This paper proposes an approach to the specification and model checking of a large, important class of distributed algorithms called control algorithms (CAs), which are superimposed on underlying distributed systems (UDSs). The approach is based on rewriting logic by moving from its object level to the meta-level. We introduce the idea of specifying CAs as meta-programs that take the specifications of UDSs and automatically generate the specifications of the UDSs on which the CAs are superimposed (UDS-CAs). Due to many options, such as network topologies, even fixing the number of each kind of entities, such as mobile support stations (MSSs) and mobile hosts (MHs) in a mobile checkpointing algorithm, there are many instances of a UDS. To address the problem, we generate all possible initial states of a UDS for a fixed number of each kind of entities such that some constraints, such as MSSs strongly connected with a wired network, are fulfilled and conduct model checking for each of the initial states. We demonstrate the usefulness by reporting on a case study where a counterexample is found for some specific initial states but not for the other initial states, detecting a subtle flaw lurking in a mobile checkpointing algorithm.

The paper proposes a new approach to model checking Chandy-Lamport Distributed Snapshot Algorithm (CLDSA). The essential of the approach is that CLDSA is specified as a meta-program in Maude such that the meta-program takes a specification of an underlying distributed system (UDS) and generates the specification of the UDS on which CLDSA is superimposed (UDS-CLDSA). To model check that a UDS-CLDSA enjoys a desired property, it suffices that human users specify the UDS for the proposed approach, while human users need to specify the UDS-CLDSA for the existing approach for each UDS. Since the proposed approach conducts model checking at meta-level, it produces a counterexample if a UDS-CLDSA does not enjoy the property, while the existing approach does not. Our method specifying CLDSA as a meta-program can be applied to formal specification of the class of distributed algorithms that are superimposed on UDSs.

Recent advances in distributed computing highlight models and algorithms for autonomous mo- bile robots that self-organize and cooperate together in order to solve a global objective. As results, a large number of algorithms have been proposed. These algorithms are given together with proofs to assess their correctness. However, those proofs are informal, which are error prone. This paper presents our study on formal verification of mobile robot algorithms. We first propose a formal model for mobile robot algorithms on anonymous ring shape network under multiplicity and asynchrony assumptions. We specify this formal model in Maude, a specification and pro- gramming language based on rewriting logic. We then use its model checker to formally verify an algorithm for robot gathering problem on ring enjoys some desired properties. As the result of the model checking, counterexamples have been found. We detect the sources of some unforeseen design errors. We, furthermore, give our interpretations of these errors.