This work presents the results of a simulated analysis concerning algorithms of self-coordination of a swarm of Unmanned Surface Vehicles (USV) for the mitigation of plastic pollution in oceans. The analysis is based on real scenarios provided by the Copernicus Marine Service. The scenario includes the localization of plastics on the sea surface and their movement in time based on the sea surface currents. A swarm intelligence algorithm is used for the decentralized coordination of the USV swarm. Results are presented on a study area located in the northern Tyrrhenian sea between Corsica and the Tuscan coast, in the period of July 2016.

This work presents an application of the Perceptually Important Points (PIP) technique for the analysis of VLF time series. The aim of the analysis is to detect anomalies with respect to the normal variations of the data trends. Such anomalies could reveal possible radio precursors of the earthquake. Since 2009, several radio receivers have been installed throughout Europe in order to realize the INFREP European radio network for studying the VLF (10–50 kHz) and LF (150–300 kHz) radio precursors of earthquakes. The time series used for experiments was collected during the Dodecanese islands earthquakes ($\text{MW}=5.6$and$\text{MW}=5.7$) occurred on January 30, 2020.

The analysis of credit card transactions allows gaining new insights into the spending occurrences and mobility behavior of large numbers of individuals at an unprecedented scale. However, unfolding such spatiotemporal patterns at a community level implies a non-trivial system modeling and parametrization, as well as, a proper representation of the temporal dynamic. In this work we address both those issues by means of a novel computational technique, i.e. computational stigmergy. By using computational stigmergy each sample position is associated with a digital pheromone deposit, which aggregates with other deposits according to their spatiotemporal proximity. By processing transactions data with computational stigmergy, it is possible to identify high-density areas (hotspots) occurring in different time and days, as well as, analyze their consistency over time. Indeed, a hotspot can be permanent, i.e. present throughout the period of observation, or intermittent, i.e. present only in certain time and days due to community level occurrences (e.g. nightlife). Such difference is not only spatial (where the hotspot occurs) and temporal (when the hotspot occurs) but affects also which people visit the hotspot. The proposed approach is tested on a real-world dataset containing the credit card transaction of 60k users between 2014 and 2015.

This paper focuses on the problem of coordinating multiple UAVs for distributed targets detection and tracking, in different technological and environmental settings. The proposed approach is founded on the concept of swarm behavior in multi-agent systems, i.e., a self-formed and self-coordinated team of UAVs which adapts itself to mission-specific environmental layouts. The swarm formation and coordination are inspired by biological mechanisms of flocking and stigmergy, respectively. These mechanisms, suitably combined, make it possible to strike the right balance between global search (exploration) and local search (exploitation) in the environment. The swarm adaptation is based on an evolutionary algorithm with the objective of maximizing the number of tracked targets during a mission or minimizing the time for target discovery. A simulation testbed has been developed and publicly released, on the basis of commercially available UAVs technology and real-world scenarios. Experimental results show that the proposed approach extends and sensibly outperforms a similar approach in the literature.

In this paper, a novel architecture of Recurrent Neural Network (RNN) is designed and experimented. The proposed RNN adopts a computational memory based on the concept of stigmergy. The basic principle of a Stigmergic Memory (SM) is that the activity of deposit/removal of a quantity in the SM stimulates the next activities of deposit/removal. Accordingly, subsequent SM activities tend to reinforce/weaken each other, generating a coherent coordination between the SM activities and the input temporal stimulus. We show that, in a problem of supervised classification, the SM encodes the temporal input in an emergent representational model, by coordinating the deposit, removal and classification activities. This study lays down a basic framework for the derivation of a SM-RNN. A formal ontology of SM is discussed, and the SM-RNN architecture is detailed. To appreciate the computational power of an SM-RNN, comparative NNs have been selected and trained to solve the MNIST handwritten digits recognition benchmark in its two variants: spatial (sequences of bitmap rows) and temporal (sequences of pen strokes).

Modern cities are growing ecosystems that face new challenges due to the increasing population demands. One of the many problems they face nowadays is waste management, which has become a pressing issue requiring new solutions. Swarm robotics systems have been attracting an increasing amount of attention in the past years and they are expected to become one of the main driving factors for innovation in the field of robotics. The research presented in this paper explores the feasibility of a swarm robotics system in an urban environment. By using bio-inspired foraging methods such as multi-place foraging and stigmergy-based navigation, a swarm of robots is able to improve the efficiency and autonomy of the urban waste management system in a realistic scenario. To achieve this, a diverse set of simulation experiments was conducted using real-world GIS data and implementing different garbage collection scenarios driven by robot swarms. Results presented in this research show that the proposed system outperforms current approaches. Moreover, results not only show the efficiency of our solution, but also give insights about how to design and customize these systems.

In Turkey, the increasing tension, due to the presence of 3.4 million Syrian refugees, demands the formulation of effective integration policies. Moreover, their design requires tools aimed at understanding the integration of refugees despite the complexity of this phenomenon. In this work, we propose a set of metrics aimed at providing insights and assessing the integration of Syrian refugees, by analyzing a real-world call detail record (CDR) dataset including calls from refugees and locals in Turkey throughout 2017. Specifically, we exploit the similarity between refugees' and locals' spatial and temporal behaviors, in terms of communication and mobility in order to assess integration dynamics. Together with the already known methods for data analysis, we use a novel computational approach to analyze spatio-temporal patterns: computational stigmergy, a bio-inspired scalar and temporal aggregation of samples. Computational stigmergy associates each sample with a virtual pheromone deposit (mark). Marks in spatiotemporal proximity are aggregated into functional structures called trails, which summarize the spatiotemporal patterns in data and allow computing the similarity between different patterns. According to our results, collective mobility and behavioral similarity with locals have great potential as measures of integration, since they are: 1) correlated with the amount of interaction with locals; 2) an effective proxy for refugee's economic capacity, and thus refugee's potential employment; and 3) able to capture events that may disrupt the integration phenomena, such as social tension.

Data breaches usually involve financial information such as credit card or bank details. Automated formal verification of safety critical systems has been mostly focused on analysing high-level abstract models which, however, are significantly different from real implementations written in programming languages. In this paper we propose a technique that links model checking verification closer to real implementations, with particular regard to financial environment, in order to identify possible causes of data breaches. A formal model starting from execution traces is retrieved. Thus, the discovered model can be analysed to verify it respects the defined properties. A real safety critical system has been used as a case study to evaluate the proposed methodology.

A key aspect of a sustainable urban transportation system is the effectiveness of transportation policies. To be effective, a policy has to consider a broad range of elements, such as pollution emission, traffic flow, and human mobility. Due to the complexity and variability of these elements in the urban area, to produce effective policies remains a very challenging task. With the introduction of the smart city paradigm, a widely available amount of data can be generated in urban spaces. Such data can be a fundamental source of knowledge to improve policies because they can reflect the sustainability issues underlying the city. In this context, we propose an approach to exploit urban positioning data based on stigmergy, a bio-inspired mechanism providing scalar and temporal aggregation of samples. By employing stigmergy, samples in proximity with each other are aggregated into a functional structure called trail. The trail summarizes relevant dynamics in data and allows matching them, providing a measure of their similarity. Moreover, this mechanism can be specialized to unfold specific dynamics. Specifically, we identify high-density urban areas (i.e. hotspots), analyze their activity over time, and unfold anomalies. Furthermore, by matching activity patterns, a continuous measure of the dissimilarity with respect to the typical activity pattern is provided. This measure can be used by policy makers to evaluate the effect of policies and change them dynamically. As a case study, we analyze taxi trip data gathered in Manhattan from 2013 to 2015.

Physical activity level (PAL) in older adults can enhance healthy aging, improve functional capacity, and prevent diseases. It is known that human annotations of PAL can be affected by subjectivity and inaccuracy. Recently developed smart devices can allow a non-invasive, analytic, and continuous gathering of physiological signals. We present an innovative computational system fed by signals of heartbeat rate, wrist motion and pedometer sensed by a smartwatch. More specifically, samples of each signal are aggregated by functional structures called trails. The trailing process is inspired by stigmergy, an insects’ coordination mechanism, and is managed by computational units called stigmergic receptive fields (SRFs). SRFs, which compute the similarity between trails, are arranged in a stigmergic perceptron to detect a collection of micro-behaviours of the raw signal, called archetypes. A SRF is adaptive to subjects: its structural parameters are tuned by a differential evolution algorithm. SRFs are used in a multilayer architecture, providing further levels of processing to realize macro analyses in the application domain. As a result, the architecture provides a daily PAL, useful to detect behavioural shift indicating initial signs of disease or deviations in performance. As a proof of concept, the approach has been experimented on three subjects.

A significant phenomenon in microblogging is that certain occurrences of terms self-produce increasing mentions in the unfolding event. In contrast, other terms manifest a spike for each moment of interest, resulting in a wake-up-and-sleep dynamic. Since spike morphology and background vary widely between events, to detect spikes in microblogs is a challenge. Another way is to detect the spikiness feature rather than spikes. We present an approach which detects and aggregates spikiness contributions by combination of spike patterns, called archetypes. The soft similarity between each archetype and the time series of term occurrences is based on computational stigmergy, a bio-inspired scalar and temporal aggregation of samples. Archetypes are arranged into an architectural module called Stigmergic Receptive Field (SRF). The final spikiness indicator is computed through linear combination of SRFs, whose weights are determined with the Least Square Error minimization on a spikiness training set. The structural parameters of the SRFs are instead determined with the Differential Evolution algorithm, minimizing the error on a training set of archetypal series. Experimental studies have generated a spikiness indicator in a real-world scenario. The indicator has enhanced a cloud representation of social discussion topics, where the more spiky cloud terms are more blurred.

Regional innovation is more and more considered an important enabler of welfare. It is no coincidence that the European Commission has started looking at regional peculiarities and dynamics, in order to focus Research and Innovation Strategies for Smart Specialization towards effective investment policies. In this context, this work aims to support policy makers in the analysis of innovation-relevant trends. We exploit a European database of the regional patent application to determine the dynamics of a set of technological innovation indicators. For this purpose, we design and develop a software system for assessing unfolding trends in such indicators. In contrast with conventional knowledge-based design, our approach is biologically-inspired and based on self-organization of information. This means that a functional structure, called track, appears and stays spontaneous at runtime when local dynamism in data occurs. A further prototyping of tracks allows a better distinction of the critical phenomena during unfolding events, with a better assessment of the progressing levels. The proposed mechanism works if structural parameters are correctly tuned for the given historical context. Determining such correct parameters is not a simple task since different indicators may have different dynamics. For this purpose, we adopt an adaptation mechanism based on differential evolution. The study includes the problem statement and its characterization in the literature, as well as the proposed solving approach, experimental setting and results.

In this paper we propose a novel algorithm for adaptive coordination of drones, which performs collaborative target detection in unstructured environments. Coordination is based on digital pheromones released by drones when detecting targets, and maintained in a virtual environment. Adaptation is based on the Differential Evolution (DE) and involves the parametric behaviour of both drones and environment. More precisely, attractive/repulsive pheromones allow indirect communication between drones in a flock, concerning the availability/unavailability of recently found targets. The algorithm is effective if structural parameters are properly tuned. For this purpose DE combines different parametric solutions to increase the swarm performance. We focus first on the study of the principal parameters of the DE, i.e., the crossover rate and the differential weight. Then, we compare the performance of our algorithm with three different strategies on six simulated scenarios. Experimental results show the effectiveness of the approach.

In this paper, we evaluate the schedulability of traffic with arbitrary end-to-end deadline constraints in Wireless Mesh Networks (WMNs). We formulate the problem as a mixed integer linear optimization problem, and show that, depending on the flow aggregation policy used in the network, the problem can be either convex or non-convex. We optimally solve the problem in both cases, and prove that the schedulability does depend on the aggregation policy. This allows us to derive rules of thumb to identify which policy improves the schedulability with a given traffic. Furthermore, we propose a heuristic solution strategy that allows good suboptimal solutions to the scheduling problem to be computed in relatively small times, comparable to those required for online admission control in relatively large WMNs.

Equivalence checking plays a crucial role in formal verification to ensure the correctness of concurrent systems. However, this method cannot be scaled as easily with the increasing complexity of systems due to the state explosion problem. This article presents an efficient procedure, based on heuristic search, for checking Milner's strong and weak equivalence; to achieve higher efficiency, we actually search for a difference between two processes to be discovered as soon as possible, thus the heuristics aims to find a counterexample, even if not the minimum one, to prove nonequivalence. The presented algorithm builds the system state graph on-the-fly, during the checking, and the heuristics promotes the construction of the more promising subgraph. The heuristic function is syntax based, but the approach can be applied to different specification languages such as CCS, LOTOS, and CSP, provided that the language semantics is based on the concept of transition. The algorithm to explore the search space of the problem is based on a greedy technique; GreASE (Greedy Algorithm for System Equivalence), the tool supporting the approach, is used to evaluate the achieved reduction of both state-space size and time with respect to other verification environments.

Ensuring deadlock freedom is one of the most critical requirements in the design and validation of concurrent systems. The biggest challenge toward the development of effective deadlock detection schemes remains the state-space explosion problem when model checking is used for proving the correctness of a system with respect to a desired behavior. In this paper we propose the use of the Ant Colony Optimization (ACO) to reduce the state explosion problem arising when finding deadlocks in complex networks described using Calculus of Communicating Systems (CCS). Moreover, ACO is used to provide minimal counterexamples. In fact, although one of the strongest advantages of model checking is the generation of counterexamples when verification fails, traditional model checkers may return very long counterexamples. We present an implementation of our technique and encouraging experimental results on several benchmarks. These results are then compared with other heuristic-based search strategies, retaining the advantages of our approach.

In this paper we investigate link scheduling for Wireless Mesh Networks (WMNs) carrying real-time (i.e., delay-constrained) traffic. We show that the problem of computing a conflict-free link schedule with end-to-end delay constraints can be formulated as a mixed-integer non linear problem that can be optimally solved in reasonable time (i.e., minutes) for relatively large WMNs (up to 20-30 nodes). We use the above result to explore the schedulability region of a WMN with a given routing and input traffic, assessing whether and when aggregating flows which traverse the same path makes a given input flow set schedulable. Furthermore, we devise a heuristic solution strategy, which computes good suboptimal solutions within up to few seconds, thus being amenable for online admission control.

Link scheduling is used in wireless mesh networks (WMNs) to guarantee interference-free transmission on the shared wireless medium in a time division multiple access approach. Several papers in the literature address the problem of link scheduling guaranteeing a minimum throughput to the flows traversing the WMN. However, none of the existing works address the problem of computing a schedule that guarantees that prespecified end-to-end delay constraints are met. In this paper, we make a first step forward in this direction by defining a link scheduling algorithm that works in sinktree WMNs, i.e. those whose traffic is routed towards a common sink (i.e., the Internet gateway). Our iterative algorithm exploits a delay-based admission control procedure, devised through network calculus, which tests the feasibility of a schedule from the point of view of delay guarantees. Preliminary analyses reported in this paper show that the algorithm finds feasible solutions in few iterations.

Abstract In this paper, we propose a bottom‐up approach for the verification of systems with modular structure: we prove that when the modules are composed in specific ways, the complete software system verifies a composition of the properties each component does. We focus on the process of upgrading systems with new functionalities, where the validity of old requirements needs to be ensured, but also an understanding of the new properties the upgraded system would enjoy is useful. In this work, we assume each component to be specified by a CCS process, and the properties to be expressed by selective mu‐calculus formulae. Copyright © 2007 John Wiley & Sons, Ltd.

When verifying applications that require a high level of reliability, testing fails to assure an adequate level of correctness. Thus we apply model checking, an automatic verification technique: the programs are written in a simple sequential language and properties are specified by a suitable temporal logic. We obtain a finite state representation of the system by applying abstraction techniques. The abstraction is derived from the logic formula representing the property to be checked. A tableau-based method is developed to prove satisfaction.

We present a model checking procedure to verify a subset of the Java Virtual Machine Language. The procedure works on a finite tractable state representation of the program: in fact, abstraction techniques are employed, driven by the temporal logic formula representing the property to be checked. A tableau-based method is developed to proof the satisfaction of the formulae: thus not all the program computations are checked, but only those ones interested in the goal of the property verification.

Abstract A system supporting video on demand is modeled in the process calculus CCS (Calculus of Communicating Systems), while some properties are expressed in a temporal logic and verified by means of the model checkers of the North Carolina Concurrency Workbench. This application was chosen as a case study to evaluate the usefulness of a methodology, by means of which a property is checked on reduced models obtained issuing abstractions of the system on the basis of the formula. Experimental results are shown and discussed. Copyright © 2001 John Wiley & Sons, Ltd.

LOTOS is a formal specification language for concurrent and distributed systems. Basic LOTOS is the version of LOTOS without value-passing. A widely used approach to the verification of temporal properties is model checking. Often, in this approach the formal specification is translated into a labeled transition system on which formulae expressing properties are checked. A problem with this verification technique is state explosion: concurrent systems are often represented by automata with a prohibitive number of states. In this paper we show how, given a set ρ of actions, it is possible to automatically obtain for a Basic LOTOS program a reduced transition system to which only the arcs labeled by actions in ρ belong. The set ρ of actions plays a fundamental role in conjunction with a temporal logic defined by the authors in a previous paper: selective mu-calculus. The reduced system with respect to ρ preserves the truth value of all selective mu-calculus formulae with actions from the set ρ. We act at both syntactic and semantic levels. From a syntactic point of view, we define a set of transformation rules obtaining a smaller program. On the semantic side, we define a non-standard semantics which dynamically reduces the transition system during generation. We present a tool implementing both the syntactic and the semantic reduction. Copyright © 1999 John Wiley & Sons, Ltd.

A specification language is introduced, able to define the behavior of concurrent programs. The language is particularly devoted to describing distributed applications, mainly with respect to scheduling problems. For this purpose, the language allows visibility of the past history of a computation and such history may be explicitly used to derive the choices on the future behavior of the computation itself and to define the values exchanged at each communication. A behavior is a partial order on events (communications) accomplished by processes, while the values of the communications are specified by a functional language. The most noticeable characteristic of specifications written in this language is the capability to be easily translated into executable concurrent programs (written into a CSP-like concurrent language), so obtaining an early prototype for these programs. An algorithm is described to accomplish the translation. An environment is provided to support static semantics checks on specifications, while dynamic testing and debugging are accomplished using interactive tools of the concurrent language environment.>

The authors discuss issues related to the debugging of concurrent programs. A set of desirable characteristics for a debugger for concurrent languages is deduced from a review of the differences between the debugging of concurrent programs and that of sequential ones. A debugger for concurrent language based upon CSP is then described. The debugger makes it possible to compare a description of the expected program behavior to the actual behaviour. The description of the behavior is given in terms of expressions composed by events and/or assertions on the process state. The developed formalism is able to describe behaviors at various levels of abstraction. Lastly, some guidelines for the implementation of the debugger are given and a detailed example of program debugging is analyzed.