A logic $\mathcal{L}$ is said to satisfy the descending chain condition, DCC, if any descending chain of formulas in $\mathcal{L}$ with ordering induced by $\vdash _{\mathcal{L}};$ eventually stops. In this short note, we first establish a general theorem, which states that if a propositional logic $\mathcal{L}$ satisfies both DCC and has the Craig Interpolation Property, CIP, then it satisfies the Uniform Interpolation Property, UIP, as well. As a result, by using the Nishimura lattice, we give a new simply proof of (...) uniform interpolation for $\textbf{IPL}_2$, the two-variable fragment of Intuitionistic Propositional Logic; and one-variable uniform interpolation for $\textbf{IPL}$. Also, we will see that the modal logics $\textbf{S}_4$ and $\textbf{K}_4$ do not satisfy atomic DCC. (shrink)

In this work, we aim at understanding incompleteness in an abstract way via metamathematical properties of formal theories. We systematically examine the relationships between the following twelve important metamathematical properties of arithmetical theories: Rosser, EI (effectively inseparable), RI (recursively inseparable), TP (Turing persistent), EHU (essentially hereditarily undecidable), EU (essentially undecidable), Creative, $\textbf{0}^{\prime }$ (theories with Turing degree $\textbf{0}^{\prime }$), REW (all RE sets are weakly representable), RFD (all recursive functions are definable), RSS (all recursive sets are strongly representable), RSW (all (...) recursive sets are weakly representable). Given any two properties $P$ and $Q$ in the above list, we examine whether $P$ implies $Q$. (shrink)

We devise exact conditions under which a join semilattice with a weak contact relation can be semilattice embedded into a Boolean algebra with an overlap contact relation, equivalently, into a distributive lattice with additive contact relation. A similar characterization is proved with respect to Boolean algebras and distributive lattices with weak contact, not necessarily additive, nor overlap.

We study a propositional probabilistic temporal epistemic logic $\textbf {PTEL}$ with both future and past temporal operators, with non-rigid set of agents and the operators for agents’ knowledge and for common knowledge and with probabilities defined on the sets of runs and on the sets of possible worlds. A semantics is given by a class ${\scriptsize{\rm Mod}}$ of Kripke-like models with possible worlds. We prove decidability of $\textbf {PTEL}$ by showing that checking satisfiability of a formula in ${\scriptsize{\rm Mod}}$ is (...) equivalent to checking its satisfiability in a finite set of finitely representable structures. The same procedure can be applied to the class of all synchronous ${\scriptsize{\rm Mod}}$-models. We give an upper complexity bound for the satisfiability problem for ${\scriptsize{\rm Mod}}$. (shrink)

This paper presents four state-of-art methods for the finite-state automaton inference based on a sample of labeled strings. The first algorithm is Exbar, and the next three are mathematical models based on ASP, SAT and SMT theories. The potentiality of using multiprocessor computers in the context of automata inference was our research’s primary goal. In a series of experiments, we showed that our parallelization of the exbar algorithm is the best choice when a multiprocessor system is available. Furthermore, we obtained (...) a superlinear speedup for some of the prepared datasets, achieving almost a 5-fold speedup on the median, using 12 and 24 processes. (shrink)

In the present paper, we study the correspondence and canonicity theory of modal subordination algebras and their dual Stone space with two relations, generalizing correspondence results for subordination algebras in [13–15, 25]. Due to the fact that the language of modal subordination algebras involves a binary subordination relation, we will find it convenient to use the so-called quasi-inequalities and $\varPi _{2}$-statements. We use an algorithm to transform (restricted) inductive quasi-inequalities and (restricted) inductive $\varPi _{2}$-statements to equivalent first-order correspondents on the (...) dual Stone spaces with two relations with respect to arbitrary (resp. admissible) valuations. (shrink)

Connected vehicle fleets have formed significant component of industrial internet of things scenarios as part of Industry 4.0 worldwide. The number of vehicles in these fleets has grown at a steady pace. The vehicles monitoring with machine learning algorithms has significantly improved maintenance activities. Predictive maintenance potential has increased where machines are controlled through networked smart devices. Here, benefits are accrued considering uptimes optimization. This has resulted in reduction of associated time and labor costs. It has also provided significant increase (...) in cost benefit ratios. Considering vehicle fault trends in this research predictive maintenance problem is addressed through hybrid deep learning-based ensemble method (HDLEM). The ensemble framework which acts as predictive analytics engine comprises of three deep learning algorithms viz modified cox proportional hazard deep learning (MCoxPHDL), modified deep learning embedded semi supervised learning (MDLeSSL) and merged LSTM (MLSTM) networks. Both sensor as well as historical maintenance data are collected and prepared using benchmarking methods for HDLEM training and testing. Here, times between failures (TBF) modeling and prediction on multi-source data are successfully achieved. The results obtained are compared with stated deep learning models. This ensemble framework offers great potential towards achieving more profitable, efficient and sustainable vehicle fleet management solutions. This helps better telematics data implementation which ensures preventative management towards desired solution. The ensemble method's superiority is highlighted through several experimental results. (shrink)

The multi-modal tasks have started to play a significant role in the research on artificial intelligence. A particular example of that domain is visual–linguistic tasks, such as visual question answering. The progress of modern machine learning systems is determined, among other things, by the data on which these systems are trained. Most modern visual question answering data sets contain limited type questions that can be answered either by directly accessing the image itself or by using external data. At the same (...) time, insufficient attention is paid to the issues of social interactions between people, which limits the scope of visual question answering systems. In this paper, we propose criteria by which images suitable for social interaction visual question answering can be selected for composing such questions, based on psychological research. We believe this should serve the progress of visual question answering systems. (shrink)

This paper investigates the Generalized Traveling Salesman Problem (GTSP), which is an extension of the well-known Traveling Salesman Problem (TSP), and it searches for an optimal tour in a clustered graph, such that every cluster is visited exactly once. In this paper, we describe a novel Memetic Algorithm (MA) for solving efficiently the GTSP. Our proposed MA has at its core a genetic algorithm (GA), completed by a Chromosome Enhancement Procedure (CEP), which is based on a TSP solver and the (...) Shortest Path (SP) algorithm and for improving the convergence characteristics of the GA, a Local Search (LS) operation is applied for the best chromosomes in each generation. We tested our algorithm on a set of well-known instances from the literature and the achieved results prove that our novel memetic algorithm is highly competitive against the existing solution approaches from the specialized literature. (shrink)

A new method for evaluating aircraft engine monitoring data is proposed. Commonly, prognostics and health management systems use knowledge of the degradation processes of certain engine components together with professional expert opinion to predict the Remaining Useful Life (RUL). New data-driven approaches have emerged to provide accurate diagnostics without relying on such costly processes. However, most of them lack an explanatory component to understand model learning and/or the nature of the data. A solution based on a novel recurrent version of (...) a VAE is proposed in this paper to overcome this gap. The latent space learned by the model, trained with data from sensors placed in different parts of these engines, is exploited to build a self-explanatory map that can visually evaluate the rate of deterioration of the engines. Besides, a simple regressor model is built on top of the learned features of the encoder in order to numerically predict the RUL. As a result, remarkable prognostic accuracy is achieved, outperforming most of the novel and state-of-the-art approaches on the available modular aero-propulsion system simulation data (C-MAPSS dataset) from NASA. In addition, a practical real-world application is included for Turbofan engine data. This study shows that the proposed prognostic and explainable framework presents a promising new approach. (shrink)

For companies involved in the supply chain, proper warehousing management is crucial. Warehouse layout arrangement and operation play a critical role in a company’s ability to maintain and improve its competitiveness. Reducing costs and increasing efficiency are two of the most crucial warehousing goals. Deciding on the best warehouse layout is a remarkable optimization problem. This paper uses an optimization method to set bin allocations within an automated warehouse with particular characteristics. The warehouse’s initial layout and the automated platforms limit (...) the search and define the time required to move goods within the warehouse. With the help of historical data and the definition of the time needed to move goods, a mathematical model of warehouse operation was created. An optimization procedure based on the well-known Variable Neighbourhood Search algorithm is defined and applied to the problem. Experimental results demonstrate increments in the efficiency of warehousing operations. (shrink)

Content-based authorship identification is an emerging research problem in online social media networks, due to a wide collection of issues ranging from security to privacy preservation, from radicalization to defamation detection, and so forth. Indeed, this research has attracted a relevant amount of attention from the research community during the past years. The general problem becomes harder when we consider the additional constraint of identifying the same false profile over different social media networks, under obvious considerations. Inspired by this emerging (...) research challenge, in this paper we propose and experimentally assess an innovative framework for supporting content-based authorship identification and analysis in social media networks. (shrink)

Concern about air-quality in urban areas has led to the implementation of Low Emission Zones as one of many other initiatives to control it. Recently in Spain, the enactment of a law made this mandatory for cities with a population larger than 50k inhabitants. The delimitation of these areas is not without controversy because of possible negative economic and social impacts. Therefore, clear assessments of how these initiatives decrease pollutant concentrations are to be provided. Madrid Central is a major initiative (...) of Madrid city council for reducing motor traffic and the associated air pollution in the city centre. This Low Emission Zone starts at the end of 2018, but the first fully-operational period corresponds to the second quarter of 2019. In this work, a methodology based on the Gaussian Process to analyse the evolution of Nitrogen Dioxide inside Madrid Central is undertaken. A Gaussian Process is a stochastic process suitable for interpretable model selection and predictions. Due to its probabilistic nature it provides error estimation at predictions. After the activation of Madrid Central, a relevant reduction of Nitrogen Dioxide has been observed. However, the role of the meteorology during this period must be ascertained to correctly evaluate the role of the activation of the Low Emission Zone against a prone weather. In this work, a model based on the Gaussian Process is trained with meteorological information to predict the concentration of Nitrogen Dioxide at Madrid Central, $[NO_{2}]$. This probabilistic description allows extracting statistical information on the reduction affected by the meteorological scenario and separately by the Madrid Central activation. (shrink)

Batteries are a fundamental storage component due to its various applications in mobility, renewable energies and consumer electronics among others. Regardless of the battery typology, one key variable from a user’s perspective is the remaining energy in the battery. It is usually presented as the percentage of remaining energy compared to the total energy that can be stored and is labeled State Of Charge (SOC). This work addresses the development of a hybrid model based on a Lithium Iron Phosphate (LiFePO4) (...) power cell, due to its broad implementation. The proposed model calculates the SOC, by means of voltage and electric current as inputs and the latter as the output. Therefore, four models based on k-Means, Agglomerative Clustering, Gaussian Mixture and Spectral Clustering techniques have been tested in order to obtain an optimal solution. (shrink)

Quality standards fulfilment is an essential task in manufacturing processes that involves high costs. One target is to avoid the presence of burrs in the edge of machine workpieces, which reduce the quality of the products. Furthermore, they are not easily removed since the part can even be damaged. In this paper, we propose an optimized Convolutional Neural Network, to detect the presence of burrs in images of milling parts. Its design is focused on the optimization of classification (accuracy) and (...) performance metrics (training time and number of trainable parameters). The proposed architecture identifies burrs with a 91.16% accuracy in the test set, outperforming existing models as EfficientNetB0. It also reduces the number of trainable parameters from other models as AlexNet by 1.5 million. The prediction process just takes 48.39 milliseconds per image. Finally, in order to check if the model gets a high activation in the region of interest, a visual explanation of the model is also carried out by using Gradient-weighted Class Activation Mapping. (shrink)

Multi-Task Learning tries to improve the learning process of different tasks by solving them simultaneously. A popular Multi-Task Learning formulation for SVM is to combine common and task-specific parts. Other approaches rely on using a Graph Laplacian regularizer. Here we propose a combination of these two approaches that can be applied to L1, L2 and LS-SVMs. We also propose an algorithm to iteratively learn the graph adjacency matrix used in the Laplacian regularization. We test our proposal with synthetic and real (...) problems, both in regression and classification settings. When the task structure is present, we show that our model is able to detect it, which leads to better results, and we also show it to be competitive even when this structure is not present. (shrink)

The well-known logic first degree entailment logic (FDE), introduced by Belnap and Dunn, is defined with |$\wedge $|⁠, |$\vee $| and |$\sim $| as the sole primitive connectives. The aim of this paper is to establish the lattice formed by the class of all 4-valued C-extending implicative expansions of FDE verifying the axioms and rules of Routley and Meyer’s basic logic B and its useful disjunctive extension B|$^{\textrm {d}}$|⁠. It is to be noted that Boolean negation (so, classical propositional logic) (...) is definable in the strongest element in the said class. (shrink)

This is a correction to: Gemma Robles, José M. Méndez, A note on functional relations in a certain class of implicative expansions of FDE related to Brady’.

Notwithstanding the potential danger to security and privacy, sharing and publishing data has become usual in Data Science. To preserve privacy, de-identification methodologies guided by risk estimation have been designed. Two issues associated with classical risk metrics are, on the one hand, the adequacy of the metric and, on the other hand, its static nature. In this paper, we present metrics for estimating risk based on the emerging semantics provided by Formal Concept Analysis. The metrics are designed to estimate the (...) a priori risk of compromised data deletion. Furthermore, by applying specialized variable forgetting methods for association rules, it is shown how to reflect the effect of deleting attributes belonging to potentially dangerous quasi-identifier sets. Additionally, a study of the role of the risk metric in confidence-based reasoning for re-identification is presented. (shrink)

As it is well known, mobile phones have become a basic gadget for any individual that usually stores sensitive information. This mainly motivates the increase in the number of attacks aimed at jeopardizing smartphones, being an extreme concern above all on Android OS, which is the most popular platform in the market. Consequently, a strong effort has been devoted for mitigating mentioned incidents in recent years, even though few researchers have addressed the application of visualization techniques for the analysis of (...) malware. Within this field, the present work proposes the extension of a new technique called Hybrid Unsupervised Exploratory Plots to visualize Android malware datasets. More precisely, the novel Beta-Hebbian Learning (BHL) method is applied for the first time and validated under the frame of Hybrid Unsupervised Exploratory Plots, in conjunction with clustering methods. The informative visualization achieved provides a picture of the structure of the malware families, allowing subsequent analysis of their organization. To validate the Hybrid Unsupervised Exploratory Plot extension and its tuning, the popular Android Malware Genome dataset has been used in the experimental setting. Promising results have been obtained, suggesting that BHL applied in combination with clustering techniques in Hybrid Unsupervised Exploratory Plots are a viable resource for the visualization of malware families. (shrink)

Context: Predicting security and trust vulnerabilities and issues is crucial for IoT interconnected systems and ecosystems, especially when integrating new, third-party or open-source components. Objective: One way to ensure timely predictions is by using a smart monitoring framework to continuously verify functional and non-functional property violations during the executions of the systems and their components. Method: This paper presents a set of guidelines for the Smart Monitoring Framework definition and its application process. Results and Conclusion: The paper provides the reference (...) architecture of the Smart Monitoring Framework and its possible implementation to promptly detect suspicious behavior or property violations. The paper also illustrates how the provided implementation satisfies the defined guidelines by design. (shrink)

In this paper we present a set of good practices in the design of a security-centric architecture for a Communication Channel that can be used to secure a Loosely-Coupled distributed platform, over unreliable communication mediums. The proposed practices are derived from designing a complete architecture that is modular and designed to support principles of Service Oriented Architecture (SOA) and the common functional requirements of a wide range of applications, including cybersecurity, smart power grids and industrial Internet of Things (IoT). The (...) architecture was developed and implemented as part of the BIECO project, and is based around open standards such as Open Platform Communications United Architecture (OPC-UA). The key feature of the architecture is that it enables secure asynchronous near-real-time communication between a large number of nodes in a multimodal setup, without the need of any Service to know its place within the tool-chain. Based on our experience with building this system and based on the good results obtained, we are presenting a list of lessons learnt, recommendations for better communication channel modules within loosely coupled distributed systems. (shrink)

An essential requirement for increasing human confidence in computer systems is knowing an event’s origin. Therefore, it is necessary to have an efficient method to record such information. It is especially challenging in robotics, where unexpected behaviours can have unpredictable consequences, endangering the interests of people or even their safety. Furthermore, to analyse an incident’s cause or anticipate future behaviours, we must identify the events that cause a specific action. Although it is common to use logging systems for such purposes, (...) issues such as partial recording of events, unhelpful data or the impact on robot performance suggest conceiving new accountability solutions that assist when determining the responsible entities or the provenance of specific information. This paper presents a general-purpose approach to developing an accountability system for autonomous robots. It consists of four main components: a system event logger, a message producer, a distributed event streaming platform and a database. Our proposal is completely decoupled from the monitored system and allows real-time analysis, improving flexibility, besides system protection and transparency. Finally, the need to reduce the impact of the audit process and logging tasks on robot performance has promoted the development of different assessment scenarios to determine the best strategy for providing accounting services. (shrink)

This paper proposes an innovative approach to achieving real-time polymorphic behavior detection, and its direct application to blockchain-focused smart-contracts. We devise a method based on a non-deterministic finite state machine to perform approximate pattern-matching, using a look-ahead mechanism implemented through a concept similar to that of a sliding window, and using threshold-based similarity checking at every state in the automaton. We introduce and formalize our approach, discuss the challenges we faced and then test it in a real-world environment. The experimental (...) results obtained showed a significant speed-up of our approach, as compared to the classic similarity measures used commonly in such scenarios. (shrink)

Digitization of every daily procedure requires trustworthy verification schemes. People tend to overlook the security of the passwords they use, i.e. they use the same password on different occasions, they neglect to change them periodically or they often forget them. This raises a major security issue, especially for elderly people who are not familiar with modern technology and its risks and challenges. To overcome these drawbacks, biometric factors were utilized, and nowadays, they have been widely adopted due to their convenience (...) of use and ease of hardware installation. Many biometric-based authentication schemes were proposed, but despite the advantages that they offer, recent research has shown that biometrics by itself cannot be considered as an inviolable technique. Recently, we have proposed StegoPass, a novel method that obtains the 68 facial points of a user and utilizes them as a stego message to an image. This produced stego image was the password. Although the experiments conducted showed maximum security, it would be challenging to enhance the robustness of the proposed model for even more attacks. This paper examines the utilization of multimodal biometrics as the secret message embedded in the image. More specifically, besides the extraction of the facial points, we extract the unique minutiae moments and combine them in a feature vector. This feature vector is then embedded in the image. Two different datasets were used, and the security of the method was tested against state-of-the-art deep learning models, i.e. generative adversarial networks, to test whether the image could be digitally synthesized and fool the proposed verification scheme. The results proved that the new enhanced version of StegoPass offers an extremely secure method as its predecessor. (shrink)

Software vulnerabilities are the root cause for a multitude of security problems in computer systems. Owing to their efficiency and tight control over low-level system resources, the C and C++ programming languages are extensively used for a myriad of purposes, from implementing operating system kernels to user-space applications. However, insufficient or improper memory management frequently leads to invalid memory accesses, eventually resulting in memory corruption vulnerabilities. These vulnerabilities are used as a foothold for elaborated attacks that bypass existing defense methods. (...) In this paper, we summarise the main memory safety violation types (i.e. memory errors), and analyse how they are exploited by attackers and the main mitigation methods proposed in the research community. We further systematise the most relevant techniques with regards to memory corruption identification in current programs. (shrink)

There is much effort nowadays to protect communication networks against different cybersecurity attacks (which are more and more sophisticated) that look for systems’ vulnerabilities they could exploit for malicious purposes. Network Intrusion Detection Systems (NIDSs) are popular tools to detect and classify such attacks, most of them based on ML models. However, ML-based NIDSs cannot be trained by feeding them with network traffic data as it is. Thus, a Feature Engineering (FE) process plays a crucial role transforming network traffic raw (...) data onto derived one suitable for ML models. In this work, we study the effects of applying one such FE technique in different ways on the performance of two ML models (linear and non-linear) and their selected features. This the Feature as a Counter approach. The derived observations are computed from either with the same number of raw samples, (batch-based approaches) or by aggregating them by time intervals (timestamp-based approach). Results show that there is no significant differences between the proposed approaches neither in the performance of the models nor in the selected features that validate our proposal making it feasible to be widely used as a standard FE method. (shrink)

This paper aims to enhance security in IoT device networks through a visual tool that utilizes three projection techniques, including Beta Hebbian Learning (BHL), t-distributed Stochastic Neighbor Embedding (t-SNE) and ISOMAP, in order to facilitate the identification of network attacks by human experts. This work research begins with the creation of a testing environment with IoT devices and web clients, simulating attacks over Message Queuing Telemetry Transport (MQTT) for recording all relevant traffic information. The unsupervised algorithms chosen provide a set (...) of projections that enable human experts to visually identify most attacks in real-time, making it a powerful tool that can be implemented in IoT environments easily. (shrink)

The paper offers a formalization of reasoning about distributed multi-agent systems. The presented propositional probabilistic temporal epistemic logic $\textbf {PTEL}$ is developed in full detail: syntax, semantics, soundness and strong completeness theorems. As an example, we prove consistency of the blockchain protocol with respect to the given set of axioms expressed in the formal language of the logic. We explain how to extend $\textbf {PTEL}$ to axiomatize the corresponding first-order logic.

For the modal logic $\textsf {S4}^{C}_{I}$, we identify the class of completable $\textsf {S4}^{C}_{I}$-algebras and prove for them a Stone-type representation theorem. As a consequence, we obtain strong algebraic and topological completeness of the logic $\textsf {S4}^{C}_{I}$ in the case of local semantic consequence relations. In addition, we consider an extension of the logic $\textsf {S4}^{C}_{I}$ with certain infinitary derivations and establish the corresponding strong completeness results for the enriched system in the case of global semantic consequence relations.

We give a new and elementary construction of primitive positive decomposition of higher arity relations into binary relations on finite domains. Such decompositions come up in applications to constraint satisfaction problems, clone theory and relational databases. The construction exploits functional completeness of 2-input functions in many-valued logic by interpreting relations as graphs of partially defined multivalued ‘functions’. The ‘functions’ are then composed from ordinary functions in the usual sense. The construction is computationally effective and relies on well-developed methods of functional (...) decomposition, but reduces relations only to ternary relations. An additional construction then decomposes ternary into binary relations, also effectively, by converting certain disjunctions into existential quantifications. The result gives a uniform proof of Peirce’s reduction thesis on finite domains, and shows that the graph of any Sheffer function composes all relations there. (shrink)