-
EEG-Based Epileptic Seizure Prediction Using Temporal Multi-Channel Transformers
Authors:
Ricardo V. Godoy,
Tharik J. S. Reis,
Paulo H. Polegato,
Gustavo J. G. Lahr,
Ricardo L. Saute,
Frederico N. Nakano,
Helio R. Machado,
Americo C. Sakamoto,
Marcelo Becker,
Glauco A. P. Caurin
Abstract:
Epilepsy is one of the most common neurological diseases, characterized by transient and unprovoked events called epileptic seizures. Electroencephalogram (EEG) is an auxiliary method used to perform both the diagnosis and the monitoring of epilepsy. Given the unexpected nature of an epileptic seizure, its prediction would improve patient care, optimizing the quality of life and the treatment of e…
▽ More
Epilepsy is one of the most common neurological diseases, characterized by transient and unprovoked events called epileptic seizures. Electroencephalogram (EEG) is an auxiliary method used to perform both the diagnosis and the monitoring of epilepsy. Given the unexpected nature of an epileptic seizure, its prediction would improve patient care, optimizing the quality of life and the treatment of epilepsy. Predicting an epileptic seizure implies the identification of two distinct states of EEG in a patient with epilepsy: the preictal and the interictal. In this paper, we developed two deep learning models called Temporal Multi-Channel Transformer (TMC-T) and Vision Transformer (TMC-ViT), adaptations of Transformer-based architectures for multi-channel temporal signals. Moreover, we accessed the impact of choosing different preictal duration, since its length is not a consensus among experts, and also evaluated how the sample size benefits each model. Our models are compared with fully connected, convolutional, and recurrent networks. The algorithms were patient-specific trained and evaluated on raw EEG signals from the CHB-MIT database. Experimental results and statistical validation demonstrated that our TMC-ViT model surpassed the CNN architecture, state-of-the-art in seizure prediction.
△ Less
Submitted 17 September, 2022;
originally announced September 2022.
-
WhylSon: Proving your Michelson Smart Contracts in Why3
Authors:
Luís Pedro Arrojado da Horta,
João Santos Reis,
Mário Pereira,
Simão Melo de Sousa
Abstract:
This paper introduces WhylSon, a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain. WhylSon accepts a formally specified Michelson contract and automatically translates it to an equivalent program written in WhyML, the programming and specification language of the Why3 framework. Smart contract instructions are mapped into…
▽ More
This paper introduces WhylSon, a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain. WhylSon accepts a formally specified Michelson contract and automatically translates it to an equivalent program written in WhyML, the programming and specification language of the Why3 framework. Smart contract instructions are mapped into a corresponding WhyML shallow-embedding of the their axiomatic semantics, which we also developed in the context of this work. One major advantage of this approach is that it allows an out-of-the-box integration with the Why3 framework, namely its VCGen and the backend support for several automated theorem provers. We also discuss the use of WhylSon to automatically prove the correctness of diverse annotated smart contracts.
△ Less
Submitted 29 May, 2020;
originally announced May 2020.
-
Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts
Authors:
João Santos Reis,
Paul Crocker,
Simão Melo de Sousa
Abstract:
This paper introduces Tezla, an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and preserves the semantics, ow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified. We provide an automated decompiler of Michelson smar…
▽ More
This paper introduces Tezla, an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and preserves the semantics, ow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified. We provide an automated decompiler of Michelson smart contracts to Tezla. In order to support our claim about the adequacy of Tezla, we develop a static analyser that takes advantage of the Tezla representation of Michelson smart contracts to prove simple but non-trivial properties.
△ Less
Submitted 24 May, 2020;
originally announced May 2020.
-
Critical dynamics of gene networks is a mechanism behind ageing and Gompertz law
Authors:
D. Podolskiy,
I. Molodtcov,
A. Zenin,
V. Kogan,
L. I. Menshikov,
Vadim N. Gladyshev,
Robert J. Shmookler Reis,
P. O. Fedichev
Abstract:
Although accumulation of molecular damage is suggested to be an important molecular mechanism of aging, a quantitative link between the dynamics of damage accumulation and mortality of species has so far remained elusive. To address this question, we examine stability properties of a generic gene regulatory network (GRN) and demonstrate that many characteristics of aging and the associated populat…
▽ More
Although accumulation of molecular damage is suggested to be an important molecular mechanism of aging, a quantitative link between the dynamics of damage accumulation and mortality of species has so far remained elusive. To address this question, we examine stability properties of a generic gene regulatory network (GRN) and demonstrate that many characteristics of aging and the associated population mortality rate emerge as inherent properties of the critical dynamics of gene regulation and metabolic levels. Based on the analysis of age-dependent changes in gene-expression and metabolic profiles in Drosophila melanogaster, we explicitly show that the underlying GRNs are nearly critical and inherently unstable. This instability manifests itself as aging in the form of distortion of gene expression and metabolic profiles with age, and causes the characteristic increase in mortality rate with age as described by a form of the Gompertz law. In addition, we explain late-life mortality deceleration observed at very late ages for large populations. We show that aging contains a stochastic component, related to accumulation of regulatory errors in transcription/translation/metabolic pathways due to imperfection of signaling cascades in the network and of responses to environmental factors. We also establish that there is a strong deterministic component, suggesting genetic control. Since mortality in humans, where it is characterized best, is strongly associated with the incidence of age-related diseases, our findings support the idea that aging is the driving force behind the development of chronic human diseases.
△ Less
Submitted 23 November, 2016; v1 submitted 15 February, 2015;
originally announced February 2015.
-
Stability analysis of a model gene network links aging, stress resistance, and negligible senescence
Authors:
Valeria Kogan,
Ivan Molodtcov,
Leonid I. Menshikov,
Robert J. Shmookler Reis,
Peter Fedichev
Abstract:
Several animal species are considered to exhibit what is called negligible senescence, i.e. they do not show signs of functional decline or any increase of mortality with age, and do not have measurable reductions in reproductive capacity with age. Recent studies in Naked Mole Rat (NMR) and long- lived sea urchin showed that the level of gene expression changes with age is lower than in other orga…
▽ More
Several animal species are considered to exhibit what is called negligible senescence, i.e. they do not show signs of functional decline or any increase of mortality with age, and do not have measurable reductions in reproductive capacity with age. Recent studies in Naked Mole Rat (NMR) and long- lived sea urchin showed that the level of gene expression changes with age is lower than in other organisms. These phenotypic observations correlate well with exceptional endurance of NMR tissues to various genotoxic stresses. Therefore, the lifelong transcriptional stability of an organism may be a key determinant of longevity. However, the exact relation between genetic network stability, stress-resistance and aging has not been defined. We analyze the stability of a simple genetic- network model of a living organism under the influence of external and endogenous factors. We demonstrate that under most common circumstances a gene network is inherently unstable and suffers from exponential accumulation of gene-regulation deviations leading to death. However, should the repair systems be sufficiently effective, the gene network can stabilize so that gene damage remains constrained along with mortality of the organism, which may then enjoy a remarkable degree of stability over very long times. We clarify the relation between stress-resistance and aging and suggest that stabilization of the genetic network may provide a mathematical explanation of the Gompertz equation describing the relationship between age and mortality in many species, and of the apparently negligible senescence observed in exceptionally long-lived animals. The model may support a range of applications, such as systematic searches for therapeutics to extend lifespan and healthspan.
△ Less
Submitted 3 August, 2014;
originally announced August 2014.
