Articles
Permanent URI for this collection
Browse
Recent Submissions
Item Open Access A FORMAL MODEL FOR THE SIMULATION AND ANALYSIS OF EARLY BIOFILM FORMATION(From Data to Models and Back, 2021-03-05) Cerone, Antonio; Marsili, EnricoBiofilms are structured communities of bacterial cells adherent to a surface. This bacterial state is called sessile. This paper focuses on the modelling of the transition between planktonic and sessile state using Real-time Maude as the modelling language. With more and more bacteria joining the sessile community, the likelihood of producing a biofilm increases. Once the percentage of bacterial cells that adheres to the surface reaches a threshold, which is specific for the considered bacterium species, a permanent biofilm is formed. An important challenge is to predict the time needed for the formation of a biofilm on a specific surface, in order to plan when the material infrastructure that comprises such a surface needs to be cleaned or replaced. We exploit the model-checking features of Real-time Maude to formally prove that a regular cleaning or replacement of the infrastructure prevents the biofilm formation.Item Open Access A FORMAL MODEL FOR EMULATING THE GENERATION OF HUMAN KNOWLEDGE IN SEMANTIC MEMORY(From Data to Models and Back, 2021-03) Cerone, Antonio; Pluck, GrahamThe transfer of information processed by human beings from their short-term memory (STM) to their semantic memory creates two kinds of knowledge: a semantic network of associations and a structured set of rules to govern human deliberate behaviour under explicit attention. This paper focuses on the memory processes that create the first of these two kinds of knowledge. Human memory storage and processing are modeled using the Real-time Maude rewrite language. Maude’s capability of specifying complex data structures as many sorted algebras and the time features of Real-Time Maude are exploited for (1) providing a means for formalising alternative memory models, (2) modelling in silico experiments to compare and validate such models. We aim at using our model for the comparison of alternative cognitive hypothesis and theories and the analysis of interactive systems.Item Open Access BEHAVIOUR AND REASONING DESCRIPTION LANGUAGE (BRDL)(Software Engineering and Formal Methods, 2020) Cerone, AntonioIn this paper we present a basic language for describing human behaviour and reasoning and present the cognitive architecture underlying the semantics of the language. The language is illustrated through a number of examples showing its ability to model human reasoning, problem solving, deliberate behaviour and automatic behaviour. We expect that the simple notation and its intuitive semantics may address the needs of practitioners from non matematical backgrounds, in particular psychologists, linguists and other social scientists. The language usage is twofold, aiming at the formal modelling and analysis of interactive systems and the comparison and validation of alternative models of memory and cognition.Item Open Access SUBJECT-INDEPENDENT BRAIN–COMPUTER INTERFACES BASED ON DEEP CONVOLUTIONAL NEURAL NETWORKS(IEEE Transactions on Neural Networks and Learning Systems, 2020-10) Kwon, O-Yeon; Lee, Min-Ho; Guan, Cuntai; Lee, Seong-WhanFor a brain-computer interface (BCI) system, a calibration procedure is required for each individual user before he/she can use the BCI. This procedure requires approximately 20-30 min to collect enough data to build a reliable decoder. It is, therefore, an interesting topic to build a calibration-free, or subject-independent, BCI. In this article, we construct a large motor imagery (MI)-based electroencephalography (EEG) database and propose a subject-independent framework based on deep convolutional neural networks (CNNs). The database is composed of 54 subjects performing the left- and right-hand MI on two different days, resulting in 21 600 trials for the MI task. In our framework, we formulated the discriminative feature representation as a combination of the spectral-spatial input embedding the diversity of the EEG signals, as well as a feature representation learned from the CNN through a fusion technique that integrates a variety of discriminative brain signal patterns. To generate spectral-spatial inputs, we first consider the discriminative frequency bands in an information-theoretic observation model that measures the power of the features in two classes. From discriminative frequency bands, spectral-spatial inputs that include the unique characteristics of brain signal patterns are generated and then transformed into a covariance matrix as the input to the CNN. In the process of feature representations, spectral-spatial inputs are individually trained through the CNN and then combined by a concatenation fusion technique. In this article, we demonstrate that the classification accuracy of our subject-independent (or calibration-free) model outperforms that of subject-dependent models using various methods [common spatial pattern (CSP), common spatiospectral pattern (CSSP), filter bank CSP (FBCSP), and Bayesian spatio-spectral filter optimization (BSSFO)].Item Restricted Automated Theorem Proving in a Chat Environment(Nazarbayev University School of Science and Technology, 2018) Zhumagambetov, Rustam; Sterling, MarkWe present a chat bot interface for the Coq proof assistant system. The bot provides a new modality of interaction with Coq that functions across multiple devices and platforms. Our system is particularly suitable for mobile platforms, Android and iOS. The basic architecture of the bot software is reviewed as are the outcomes of several rounds of beta-testing. Potential implications of the system are discussed, such as the possibility of a seamless collaborative proof environment.