arXiv:1804.08091v2 [cs.PL] 8 May 2018  Towards formal models and languages for verifiable Multi-Robot Systems  Rocco De Nicola   1 , Luca Di Stefano   2 , ∗   and Omar Inverso   2 1 IMT School for Advanced Studies, Lucca, Italy  2 Gran Sasso Science Institute (GSSI), L’Aquila, Italy  Correspondence*: Luca Di Stefano luca.distefano@gssi.it  ABSTRACT  Incorrect operations of a Multi-Robot System (MRS) may not only lead to unsatisfactory results, but can also cause economic losses and threats to safety. These threats may not always be apparent, since they may arise as unforeseen consequences of the interactions between elements of the system. This call for tools and techniques that can help in providing guarantees about MRSs behaviour. We think that, whenever possible, these guarantees should be backed up by formal proofs to complement traditional approaches based on testing and simulation. We believe that tailored linguistic support to specify MRSs is a major step towards this goal. In particular, reducing the gap between typical features of an MRS and the level of abstraction of the linguistic primitives would simplify both the specification of these systems and the verification of their properties. In this work, we review different agent-oriented languages and their features; we then consider a selection of case studies of interest and implement them useing the surveyed languages. We also evaluate and compare effectiveness of the proposed solution, considering, in particular, easiness of expressing non-trivial behaviour.  Keywords: multi-robot systems, languages, communication, collective behaviour, automated reasoning  1   INTRODUCTION  Multi-robot systems (MRSs) are an increasingly popular topic in robotics research. Their broad range of activities have been categorised in several different ways (Brambilla et al., 2013; Arai et al., 2002; Bayındır, 2016). Typical tasks include exploration or patrolling, object transport and manipulation (e.g. foraging), deployment (e.g. pattern formation), collective decision making (e.g. flocking), task allocation, and many others. Cooperation is the real power of a MRS: by working together, the robots can globally achieve goals that would be “difficult, if not impossible, to be accomplished by an individual robot” (Arai et al., 2002). On the other hand, the concerns that typically arise with any robotic system (Vasic and Billard, 2013) are largely exacerbated in the presence of multiple cooperating units. In particular, the risk of incorrect operation, whence possible economic losses and even threats to safety, is much greater. Such concerns are related to the inherent features of MRSs rather than the specific kind of task of a MRS. A first source of trouble is   open-endedness   of MRSs, i.e. the fact that robots can dynamically enter or leave the system. This happens when decommissioning faulty units, or deploying extra units to  1
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  increase the throughput or system’s fault tolerance. Another complication is   anonymity , in the sense that cooperating robots may not necessarily rely on, or be aware of, each other’s identity. The identity is, for instance, irrelevant in a flock of drones that adjust their directions by looking at each other. Anonymity has a particularly disruptive impact on communication, as it renders existing traditional mechanisms such as point-to-point communication fundamentally inadequate. Another cause of concern with MRSs is  decentralisation , i.e. the absence of a central entity to coordinate the robots’ activities. Decentralisation makes synchronisation especially challenging, if possible at all, and in general makes it difficult to achieve an acceptable robustness of the interaction protocols. Another source of complexity in MRSs is the typically   large size   of the systems, and in particular the considerably large state space resulting from asynchronous interaction of large numbers of components. These features result in challenges to the specification of MRSs. A vast portion of literature relies on general-purpose languages to model MRSs (Pitonakova and Bullock, 2013; Pitonakova et al., 2016; Buchanan et al., 2016) but, typically, each work focuses on rather narrow classes of systems while making specific assumptions on the operating contexts. In general, modelling the mentioned features of MRSs using general-purpose languages is not intuitive, and can lead to increased code complexity, higher likelihood of programming errors, and generally makes programs hard to develop and maintain, and complicates reasoning about them. On the other hand, domain-specific languages with tailored, higher-level primitives that reduce the conceptual gap with the above mentioned features can make the specification of new MRSs easier, as well as constraining the complexity of the resulting global behaviour (Matari ́ c, 1993). However, the heterogeneity of the domains might be detrimental for compositionality; it may become harder to specify complex systems by composing available solutions. Also, there is some risk in adopting abstractions that are too specific, as they might oversimplify the problem space and might not be able to realistically describe scenarios of interest. Thus, linguistic support should aim at addresing the aforementioned sources of complexity, while achieving an acceptable trade-off between expressiveness and generality. The nature of MRSs also makes their analysis problematic. For instance, the correctness and efficiency of an MRS is commonly measured through simulations or experiments in a real,   yet controlled, environment. However, interaction between components may give rise to complex collective behaviour that is difficult to predict (Matari ́ c, 1995). The interleaving of individual processes also means that it is often impossible to systematically explore any possible behaviour through simulation: subtle corner cases can go unnoticed and lead to failure in a real-world deployment. Languages equipped with a clear semantics can address these concerns by supporting both informal reasoning and formal verification of properties. Appropriate primitives can also prove helpful in this regard, since verification can often exploit high-level information on the system to guide the analysis (Clarke et al., 1996; Flanagan and Godefroid, 2005). This, in turn, can make research on more complex systems feasible. In the long term, such languages could become the core element of integrated environments aiding the design of MRSs through automated reasoning tools, quite like the currently available integrated development environments (IDEs) for programming languages. In this paper we review some languages stemming from MRS and multi-agent systems (MAS) literature. Our selection is driven by their different nature and goals. Buzz is oriented to real-world applications and shares some similarities with popular languages, such as Python, JavaScript and Lua. ISPL and its surrounding framework are specifically designed to enable reasoning on the knowledge of agents, and provides explicit abstractions for the external environment. Finally, SCEL is a process description language where MRS features, such as as anonymity and open-endedness, are transparent to the designer,  This is a provisional file, not the final typeset article   2
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  allowing for a high degree of naturalness in the specification of individual behaviour. We highlight the main characterizing features of these three formalisms and compare them by considering how they model several traits commonly found in MRSs. We also analyse how well the languages can support the design phase through simulation or verification tools. We focus on languages based on   individual behaviour design . That is, a developer using said languages is mainly concerned with the behaviour of single components: the expected global behaviour is not explicitly programmed, but is expected to arise from interaction between the robots. Although alternative methods have been proposed, such as automatic design of individual behaviour from higher-level specifications (Ulusoy et al., 2013; Nikou et al., 2016) or top-down behavioural languages (Bachrach et al., 2008), the bottom-up approach is still widely adopted due to its intuitiveness (Brambilla et al., 2013). To guide our comparison, we focus on two popular case studies, namely   foraging   and   flocking . When foraging, robots must find items in the environment and bring them back to a fixed “home” location. Flocking, on the other hand, is a process where robots that initially move in different directions eventually agree to head in the same way. Both case studies are commonly observed in biological systems and cover most of the sources of complexity in MRSs. This paper is structured as follows. In Section 2 we list a set of features commonly found in MRSs, describing how they can represent a source of complexity during the specification or analysis of these systems. Section 3 introduces the considered languages and provides an overview of their main features. We then compare them on their ability to model the aforementioned features. In Section 4 we describe our case studies and, if possible, we provide a basic implementation in each language, along with observations on their respective advantages and limitations. Section 5 contains our conclusions, as well as related and future work.  2   COMMON FEATURES OF MULTI-ROBOT SYSTEMS  In this section we outline and categorize some common features of MRSs. First of all, these systems are typically   decentralized , as they lack a central unit of control: therefore there is no reliable way for a component to obtain correct information about the full state of the MRS. Robots might also be free to join or leave the system at any time, a feature known as   open-endedness . This may happen deliberately (e.g. robots returning to a home location to charge their batteries) or due to unexpected events, such as hardware failures. Open-endedness complicates reasoning: for instance, robots leaving the system create issues similar to those raised by failed processes in distributed computing (Lamport, 1978a). Meanwhile, robots that join a MRS often need to gather information from other components before they are able to cooperate; as another example, a robot might have to find alternative solutions when a collaborator leaves the system. This calls for components with   self-managing   capabilities, such as self-configuration (Kephart and Chess, 2003). Furthermore, computational processes are   distributed , both physically and logically, across the whole system. Physical distribution, among other consequences, means that inter-process communication may incur significant delays and possible failures. On the other hand, logical displacement requires additional care to avoid well-known risks of concurrent programming, such as deadlocks and process starvation. As a further source of complication, often there are no temporal constraints to computation and interaction, as these systems may be partially or fully   asynchronous . For instance, robots may take an arbitrary long time to send or read a message, and it is known that this can be the source of some fundamental problems in distributed computing, such as the distributed consensus (Fischer et al., 1985). Interaction in these systems is also characterized by   anonymity , as it does not typically rely on identity. Moreover, in a decentralized or open-ended system the whole concept of identity is not easy to  Frontiers   3
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  establish, and may even be irrelevant. The ability to select partners according to their current task, or their capabilities, can be more useful. For instance, robots in a foraging swarm can perform   recruiting  by communicating the position of food to idle neighbours (Pitonakova et al., 2017). Such action only relies on the observed state of neighbours, and thus can be performed also when agents are completely anonymous. Due to the above mentioned features, in a MSR, the common interaction patterns of concurrent and distributed systems, such as point-to-point communication, shared memory, or synchronization, turn out to be inadequate. Therefore, different solutions have been proposed which better fit to large, open-ended systems that do not rely on the concept of identity. These include many-to-many communication (e.g. multicast or broadcast), or even group-oriented interaction. A group-oriented network is composed of groups of collaborating processes, and the message passing primitives do not target individual processes, but whole groups (Birman, 1993). Indeed, robots that are popular in the MRS literature, like the Kilobot (Rubenstein et al., 2012), even lack hardware tools for unicast or synchronous communication, making the aforementioned approaches the only viable ones. As the complexity of MRSs increases, there is a growing need for them to react to new environmental conditions without human support. This feature, known as   adaptiveness , is considered a necessity for future computing systems as a whole (Kephart and Chess, 2003), but is especially attractive in the case of MRSs, since they are situated in a physical world where a large number of unexpected situations may arise. Adaptive behaviour can be found in various biological systems such as ant colonies: when a source of food is found, ants collectively find an optimal path from the nest. When said path is disrupted, the colony is able to found a new, optimal one by relying on a set of elementary actions performed by individual ants (Dorigo et al., 2006). This example also shows that system-wide adaptiveness can be obtained even from simple actions by individual components. Moreover, robots can be different from one another: their behavior, equipment and capabilities may be  heterogeneous . In principle, it is always possible to describe a system with differentiated behaviour as a homogeneous one, if the chosen formalism provides adequate control-flow statements. This approach can be acceptable for modelling mostly homogeneous swarms, but it is insufficient when different groups of specialized robots are considered: in fact, it introduces a significant overhead at various levels. First of all, it greatly increases the complexity of the resulting specification. Because of that, very heterogeneous systems could become hard to understand and maintain. For instance, errors in the control flow may produce unwanted behaviour. The need to differentiate behaviour at runtime may also negatively affect the performance of simulations and real-world implementations. Finally, informal reasoning on system with a complicated control flow is difficult, as well as verification through automated tools. The   large size   of the system may hinder the feasibility of practical implementations, as it puts a high stress on the underlying runtime environment and data structures. Often, an individual behaviour that is acceptable when the number of robots is small becomes unworkable as the population grows. For instance, each robot can obtain a quite accurate view of a small system by just exchanging messages with all the others. But, due to the limited computational and networking capabilities of robots, this is usually not possible in the case of large MRSs. A large size is detrimental to verification, and even simulation may become harder. These effects are further complicated by   non-determinism   and   non-linearity . When the system is non-deterministic, multiple transitions are executable from a given state, complicating the analysis. Non-linearity, on the other hand, means that a local change may trigger a disproportionate, potentially system-wide effect. As a consequence, simulation is not only more demanding, but also less significant, as it might not spot critical, yet subtle cases where the system fails. The size of a system also  This is a provisional file, not the final typeset article   4
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  plays a role in its classification. For instance, nearly-homogeneous MRSs with a very large number of components typically fall into the   swarm robotics   category. A quantitative definition classifies a system of size   N   as a swarm when   10 2   < N < <   10 23 , with the rationale that “Avogadro-large” systems are better treated with statistical tools (Beni, 2005; Hamann, 2018). MRSs represent a more generic classification as they can be smaller in size but more heterogeneous. The presence of an   environment   plays a critical role in MRSs, too. In fact, many applications of MRSs involve   sensing   and   actuation , i.e. the gathering of data from, or manipulation of, the external environment. It is often unfeasible to model these actions with the same tools used to describe agents, since additional guarantees of synchrony, atomicity and consistency must be provided which do not hold in agent-to-agent communication. A similar observation has also been made in the more general context of multi-agent systems (Weyns and Holvoet, 2004; Weyns et al., 2006). The manipulation of the environment can also work as a medium of indirect interaction between robots. This mechanism, known as   stigmergy , is often found in biological systems (Grass ́ e, 1959; Theraulaz and Bonabeau, 1999) and has some benefits over direct message passing. For instance, it is inherently anonymous, as each agent simply react to changes in the environment without knowing who caused them. It is also considered a highly scalable solution (Heylighen, 2016). While inaccuracies in sensing and actuation can lead to lossy information transfer, these advantages make stigmergic interaction attractive and widely studied (Arkin, 1992; Werfel et al., 2005; Pitonakova and Bullock, 2013). Additional pecularities of MRSs are strictly related to the knowledge of robots. Each component has only   partial awareness   of the current state system it is operating in and possibly even of its own state. For instance, robots can typically know the position of their neighbours, but not the one of robots that are farther away. In open-ended systems, they might even not know the size of the system itself. Even when robots are able to obtain information about the system, said knowledge might be partial or become outdated by the time it is accessed. This raises the problem of how to adequately represent knowledge and its propagation among components, which is an important element to accomplish complex coordination tasks (Pitonakova et al., 2017). As any kind of shared memory is unacceptable in large and distributed systems, resorting to distributed data structures may be the only feasible approach. However, the design of these structures must deal with the problems arising from the extremely dynamic nature of MRSs, which can lead to integrity and consistency problems.  3   LANGUAGES  In this section we present a set of languages suitable for the specification and analysis of MRSs, namely Buzz (Pinciroli and Beltrame, 2016), ISPL (Lomuscio et al., 2017) and SCEL (De Nicola et al., 2014b). Our selection is driven by their different nature, which makes them almost orthogonal with respect to each other. This allows us to better outline their respective strengths and drawbacks. Buzz is oriented to real-world applications and provides a quite mature runtime environment, including a reference virtual machine and a simulation platform with an integrated physical engine. Its similarities with popular general- purpose languages, such as Python, JavaScript and Lua, can also be considered an advantage. ISPL and its surrounding framework are specifically designed to support epistemic logics, which enables reasoning on the knowledge of individuals or groups of agents. Appropriate primitives are provided to model the interaction among agents and of agents with the environment. Finally, SCEL is a process calculus that offers the possibility of naturally guaranteeing features such as anonymity and open-endedness. This is made possible by its inherently group-oriented interaction primitives, which rely on dynamic ensembles  Frontiers   5
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  formed by taking into account the exposed features of components. Thanks to its parametric semantics, the language can also be adapted to manage different knowledge models.  3.1   Buzz  Buzz (Pinciroli and Beltrame, 2016) is a language for heterogeneous robot swarms. It is designed as a core language that provides a few communication and coordination primitives, and can be extended to suit the needs of the user. For instance, it supports asynchronous communication with neighbours: each component maintains a list of neighbours and can broadcast a key-value pair or listen (in a non-blocking fashion) for a given key. Swarms, i.e. dynamic ensembles of robots, are also a first-class abstraction in Buzz. Robots can join or leave an ensemble at runtime, and swarms can execute arbitrary functions. For instance, one could design a system where an ensemble periodically broadcasts sensor data, while a second swarm receives these messages and uses them to take decisions. A distinctive feature of the language is the concept of virtual stigmergies (Pinciroli et al., 2016). Stigmergies represent a first-class abstraction of a shared knowledge base. They are distributed key- value stores, replicated on all robots, where entries propagate or get overwritten based on their attached timestamps. For instance, when two agents try to bind the same stigmergy key to different values, there will be an initial phase where both entries will spread across the system. However, if the swarm is connected (i.e. each robot has at least one neighbour), at some point the entry with the lower timestamp will stop propagating. The newer entry, on the other hand, will continue spreading, eventually overwriting the other one on the local copy of every component. To avoid inconsistencies without resorting to a global clock, the mechanism relies on Lamport timestamps (Lamport, 1978b). This mechanism gives some guarantees over the eventual consistency of all local copies of the virtual stigmergies. Buzz is very marginally concerned with embodiment, i.e. the fact that robots are distinct entities situated in, and able to interact with, the physical world (Brooks, 1991). Indeed, any kind of sensing and actuation, including the robot’s own movements, must be modelled by extending the language with appropriate functions. This philosophy reduces the complexity of the language, but also leaves the developer the responsibility of defining the semantics of the extensions. The current implementation of Buzz requires all robots to have a unique identifier, which is attached to all messages. For instance, the tie-breaking protocol for virtual stigmergies reduces to a comparison between IDs. Moreover, all robots periodically broadcast their ID so that they can use these messages to keep their neighbours list up-to-date. These aspects might raise scalability issues, especially in dense swarms where each robot could have tens of neighbours. Buzz also assumes that a robot, upon receiving a message, can automatically detect the position of the sender thanks to   situated communication  equipment (Støy, 2001). As a consequence, there is no need for robots to declare their own position in the message payload, making the maintenance of the neighbour list less complex. At the same time, situated communication devices currently face other limitations: for instance, only robots that are in direct line-of-sight with each other can exchange messages. This might be a limiting factor in very cluttered environments. MRSs defined through Buzz can be simulated on the ARGoS platform (Pinciroli et al., 2012). The user configures the number of robots and the Buzz script they execute by editing an XML file. This file also describes the arena and its obstacles, the spatial distribution of robots, and their equipment. Even though the authors stress that all robots must execute the same Buzz script, we were actually able to simulate a system where two groups of MarXbots (Bonani et al., 2010) execute slightly different scripts. We observed that robots can communicate with each other through a virtual stigmergy, even if they belong to  This is a provisional file, not the final typeset article   6
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  different groups. However, we also noticed that different agents may have the same identifier. Even though our simulation behaved as expected, this violates the aforementioned assumption on the uniqueness of IDs and therefore can lead to undesired consequences.  3.2   ISPL (Interpreted Systems Programming Language)  The ISPL language (Lomuscio et al., 2017) is based on   interpreted systems , a generalization of labeled transition systems where multiple LTSs may synchronize on specific actions (Fagin et al., 1995). Each agent has a state (a set of user-defined variables) and a   protocol   that defines the actions it can perform given the current state. Changes to the local state are encoded in a   local evolution   function, which takes into account both the current local state and the actions performed by other agents. As a consequence there are no explicit primitives for communication, the latter is encoded in the evolution of agents as the result of the synchronization on specific actions. The state of agents is encapsulated: agents can only observe other agents’ actions, and eventually synchronize with them. The environment is an exception, as it is a distinct agent whose variables may be fully or partially observed by the other agents. The synchronization mechanisms over actions can be used to model different communication schemes involving an arbitrary number of agents. Furthermore, specific actions can be defined so that they require the simultaneous interaction of multiple agents and of the environment. This way of modelling interaction, while flexible, also makes asynchronous interaction difficult to describe. For instance, representing the delayed reception of a message requires the declaration of appropriate variables and evolutions within each agent. Value-passing is difficult to describe as well. In principle, agents should encode each possible value in a different action. This approach may cause an increase in the complexity of agents, and does not account for values over infinite domains. Moreover, anonymity and open-endedness are not considered, as the system size is fixed and transitions explicitly take into account other agents’ actions. These concerns have been partially addressed in the MCMAS-P framework (Kouvaros and Lomuscio, 2016b), where the size of system is parametrized. The user only specifies the behaviour of each kind of agent in the system; in the verification phase, concrete systems are instantiated by creating a fixed number of agents for each role. Thanks to cutoff techniques, verification of a property against a limited number of concrete systems can be sufficient to prove that all concrete systems derived from the same set of roles do satisfy the property. However, finding a cutoff for an arbitrary property is, in general, an undecidable problem. Hence, the cutoff search algorithm of MCMAS-P is sound but incomplete. Moreover, open- ended systems are still out of reach, as the size of each concrete instantiation is fixed. Verification is possible through model-checking of   epistemic properties   in the MCMAS framework. An epistemic formalism is typically derived from an existing temporal logics by adding modalities to “reason about the knowledge of the agents in the system” (Lomuscio et al., 2017). For instance, epistemic logics naturally allows to express properties such as “All agents eventually know   φ ” or “Agent  i   always knows   φ ”, where   φ   is another temporal or epistemic property. MCMAS originally supported the ATLK language, an extension of Alternating Temporal Logics (ATL) (Alur et al., 2002). A more recent implementation supports a significantly more expressive language, LDLK (Kong and Lomuscio, 2017). The same framework also provides support for interactive simulation, where the user can choose an initial state of the system and manually select a sequence of transitions to better understand the behaviour of agents.  Frontiers   7
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  3.3   SCEL (Software Component Ensemble Language)  SCEL (De Nicola et al., 2014b, 2015) is a formal language for the description and verification of collective adaptive systems (Hillston, 2014). In order to capture the highly dynamic nature of this class of systems, it naturally supports concepts such as open-endedness and anonymity. Communication in SCEL is deeply related to the concept of knowledge repositories. A knowledge repository is a container of knowledge items. The nature of repositories and items is not specified, and the SCEL semantics is parametric with respect to their semantics.   While most works use tuple spaces (Gelernter, 1985),   other kinds of repositories have been   proposed.   Soft constraint programming (Schiex et al., 1995), for instance, can be integrated into SCEL by defining repositories as constraint stores (Montanari et al., 2015). Each component is equipped with a set of   attributes , which are named values exposed to the whole system. Attributes and their values are stored in the knowledge repository of the component, thus they can change during the evolution of the system. The set of exposed attributes, known as   interface , can be dynamic as well. Communication is achieved through the manipulation of said repositories. In addition to inserting items (via the   put   action), a component can read or withdraw an item that matches a specified   pattern , or template (via the   qry   and   get   actions, respectively). All operations are either point-to-point or   attribute- based , i.e involving only those components that satisfy a given predicate over their exposed attributes. This leads to a high degree of anonymity, as components do not need to know the identity of interaction partners, nor to expose their own. Components are able to manipulate their own repository by using the special   self   identifier. The knowledge repository is also an abstraction layer over sensing and actuation. For instance, the intention of an agent to move towards a destination   d   could be represented by putting a  ( “moveTo” , d )   item into its own repository. It is assumed that another process will retrieve this tuple, drive the agent’s motors accordingly, and potentially announce the result of the operation by inserting another tuple in the repository. Notice that the   put   action is the only non-blocking one. The blocking nature of  qry   and   get   is useful to implement various reactive patterns and to guarantee processes synchronization. Guards, for instance, are naturally implemented by waiting until a specific item can be withdrawn from the component’s own repository. When the semantic of repositories is similar to that of tuple spaces,  generative communication   patterns can be easily applied (Carriero and Gelernter, 1989; Carriero et al., 1994). Implementing a runtime environment that respects the SCEL operational semantics is not trivial. The jResp implementation provides three options. The first one relies on a centralized message broker, which may be unacceptable in scenarios where full decentralization is needed. Alternatively, messages and predicates could be broadcasted in a bus-like topology. In this case, receivers accept or reject a given message after evaluating the associated predicate over their own interface. This solution is completely decentralized, but evidently does not scale well with the size of the system. The third option is a peer-to-peer topology based on the Scribe protocol (Castro et al., 2002). With jResp it is also possible to simulate the computational aspects of a SCEL system. However, physical simulation (such as the one offered by Buzz through ARGoS) is currently unavailable. Multiple verification approaches exist for systems specified in SCEL and its derivatives. The subset of SCEL without policies, known as SCELight, can be directly translated to Promela, thus allowing for model- checking through the SPIN tool (De Nicola et al., 2014a). The MISSCEL implementation (Belzner et al., 2014) enables simulation and logical model-checking within the M AUDE   framework.   Furthermore, M ULTI V E S T A can be used to verify systems through statistical model-checking, a technique based on  This is a provisional file, not the final typeset article   8
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  checking formulae satisfaction against a finite number of executions. As a consequence, it can only provide a statistical evidence that the required property is satisfied. On the other hand, it is highly parallelizable and can provide insight on systems that are too large to be formally verified (Legay et al., 2010).  3.4   Comparison  We summarize in Table 1 our findings about the three formalisms.  Table 1.   Comparison of MRS support of the languages we considered.  Buzz   ISPL   SCEL  Open-endedness   No   No   Yes  Asynchrony   Yes   No   Yes  Anonymity   Medium ( neighbors )   Low   High  Heterogeneity   Low   High   High  Communication   Ranged broadcast   Multicast   Multicast  Knowledge representation  Local variables, virtual stigmergies Local and environmental variables Parametric (e.g. tuple spaces)  Environment   No   Yes   Yes   (as   an   additional component)  Semantics   Reference implementation   Formal (Kripke structures)   Formal (SOS)  Analysis   Physics-based simulation (ARGoS) Simulation, Model-checking (MCMAS) Simulation (jResp); Model-checking (SPIN, M AUDE ); statistical model checking (V ESTA )  We found SCEL to be the only language with the capability to represent systems of dynamic size. Its syntax contains a   new   keyword that allows components to “spawn” additional agents. This can be crucial to naturally specify fully open-ended MRSs. ISPL is different from both Buzz and SCEL in that it enables explicit specification of the environment. It is not clear whether implementing an environment on top of Buzz would be possible, as its primitives are fully asynchronous and oriented to concrete robots. Extending the language seems the most appropriate approach. Meanwhile, using one or more SCEL components to model an environment could be viable, since the language provides both asynchronous and synchronous mechanisms, and a more flexible representation of knowledge. ISPL has no primitives for asynchronous interaction, nor value-passing. This means that replicating asynchronous features, while possible in principle, would be quite complex and might negatively affect verification times. The different approaches to communication are also reflected in the support for anonymity. In ISPL, anonymity is low as interaction happens through synchronization with specific agents: the mediation of the environment can represent a solution, like in our flocking example below, but adds complexity to the specification. Buzz offers the possibility of broadcasting or listening messages among neighbours, but the dependence on unique IDs contrasts with full anonymity. In SCEL, by contrast, attribute-based actions are inherently anonymous, as sender and receivers can communicate without any specific information on each other. As regards the analysis of specified systems, to the best of our knowledge Buzz is the only language equipped with a physics-based simulation environment. This could be important to study the behaviour of agents under conditions that they could face in the real world. Meanwhile, Buzz offers little support for formal verification. On the other hand, no language except SCEL provides documented support for  Frontiers   9
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  statistical model checking, which could be a useful tool for large MRSs. However, given that MCMAS can already compute traces from a given ISPL system, extending ISPL to support this technique seems relatively straightforward.  4   CASE STUDIES  4.1   Foraging  Foraging is considered a canonical case study in the literature related to MRS and robotic swarms, since it can be used to model many kinds of scenarios, such as “waste retrieval” and “search and rescue” (Brambilla et al., 2013). Specifying a foraging MRS can show the capabilities of the chosen specification language with respect to different features of these systems, such as the representation of the agents’ knowledge and their interaction with the environment through sensors and actuators.  Buzz . As Buzz lacks a notion of environment as well as synchronous communication primitives, food items have to be implemented as components, and specific protocols must be set up to limit inconsistencies. The system consists of into two   swarms : food items and forager agents. Foragers perform a random walk and repeatedly broadcast a pick-up request to all neighbours. Food items wait for pick-up requests and if the requesting forager is close enough, they respond with its id to signal that they have been collected successfully.  function   food_listen(vid,   value,   rid)   { #   Check   if   the   robot is   closer than 50 cm d   =   neighbors.get(rid).distance  if   (d <   50) { neighbors.broadcast("response",   rid) #   Stop responding to other foragers neighbors.ignore("pick_up") } }  function   robot_listen(vid,   value, rid) {  if   (value ==   id) { log(id, ":   picked up ", rid) } }  function   init()   { #   Robots with id =   0, 4,   8 etc. are   food items foodSwarm =   swarm.create(1) foodSwarm.select(id   % 4   == 0) #   All the others are foragers foragerSwarm =   foodSwarm.others(2)  if   (foodSwarm.in())   { neighbors.listen("pick_up", food_listen) }   else   { neighbors.listen("response", robot_listen) } }  This is a provisional file, not the final typeset article   10
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  function   step()   {  if   (foragerSwarm.in()) { #   Only foragers execute this block #   Random walk (sets linear   and   angular velocity) gotop(5,   math .rng.uniform(-3.0,   3.0)) neighbors.broadcast("pick_up",   id) } }  We encode the individual behaviour inside two standard Buzz functions. The first one is   init() , which will be executed only once, after the agent has been created. The function   step() , instead, is repeatedly executed by each robot until the experiment terminates. One might think of stopping food items once they signal their availability to one of the foragers, but it appears that the execution of function   step()   cannot be blocked through any statement provided by the language. This solution has still some limitations. For instance, it is still possible for two foragers to pick up the same food item. Indeed, if a food item receives two   pick-up   messages, it could perform the listener function   food   listen   twice and send two different   response   messages.  ISPL . Let us assume that the arena is a two-dimensional grid of size   10   ×   10 . We use the Environment agent to keep track of the position of food items and to recorder whether they have been collected or not. This information needs to be stored in   observable variables , since foraging robots need to access it. We also define an internal variable with the number of found items, which will be used for verification purposes. Robots, on the other hand, are agents with a position. We only give the specification of   Robot1 , as the only difference between foragers is their identifier.  Agent   Environment  Obsvars : food1X : 1   .. 10; food1Y : 1   .. 10; food1 :   boolean ; food2X : 1   .. 10; food2Y : 1   .. 10; food2 :   boolean ;  end   Obsvars Vars : foundItems : 0   ..   2;  end   Vars  -- ...  end Agent Agent   Robot1  Vars : x   : 1   .. 10; y   : 1   .. 10;  end   Vars  -- ...  end Agent  Frontiers   11
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  We define the protocol and evolution functions so that foragers perform a random walk and can only pick up an item when they are in its same position, and it has not been collected yet. When an item is collected, the environment updates the corresponding boolean variable and increments the internal counter.  -- Environment  Evolution : food1 =   false and   foundItems = foundItems+1   if  (Robot1.Action = PickFood1);  -- Repeat for all robots and food items  end   Evolution  -- Robots  Actions   = {Up,   Down, Left, Right,   PickFood1,   PickFood2};  Protocol : y   < 10   : {Up}; y   > 1   : {Down}; x   < 10   : {Right}; x   > 1   : {Left}; Environment.food1 =   true and  x =   Environment.food1X   and  y =   Environment.food1Y :   {PickFood1};  -- Repeat for all food items  end   Protocol Evolution : x   = x+1   if   ( Action   =   Right); x   = x-1   if   ( Action   =   Left); y   = y+1   if   ( Action   =   Up); y   = y-1   if   ( Action   =   Down);  end   Evolution  Finally, we specify some constraints on the initial state of the system: namely, all items are available and the   foundItems   counter is set to 0. As we specify no restriction on the positions of robots and items, their value will be fully non-deterministic.  InitStates  Environment.food1 =   true and  Environment.food2 =   true and  Environment.foundItems =   0;  end InitStates  Alternatively, one could model food items as components. Parametrised versions of this approach are available in the literature (Kouvaros and Lomuscio, 2016b), but to our knowledge these models do not take into account the physical location of robots and items.  SCEL . Let us assume knowledge repositories to be tuple spaces. The implementation we describe is based on more complex examples, related to search and rescue operations, available in the existing literature on SCEL (De Nicola et al., 2014b, 2015). We can model both foraging robots and food items as SCEL components. Each forager exposes its own position   pos , the task it is performing (initially all robots are   idle ), and the range of its sensor. Each food item runs the same process   P food   :  This is a provisional file, not the final typeset article   12
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  P food   ,   put   ( “food” ,   this .pos   ) @ ( task   =   “idle”   ∧ ‖ pos   −   this .pos ‖ ≤   range )   .P food  +  qry   ( “found”   ) @ self . nil  This means that the food item will repeatedly communicate its own position to all idle foragers that are closer than the range of their own sensor. This process will terminate when the item discovers a  ( “found” )   tuple into its own knowledge repository. ( nil   denotes the inactive process). Before describing the behaviour of foragers, let us assume that each food item initially has a   ( “lock” )   tuple in its repository. We will use it to ensure that only one forager is able to collect the item. Foragers alternate between the idle and working states. In the idle state, they just perform a random walk until they sense a food item. In that case, they change their   task   attribute accordingly and move towards the food source.  P idle   ,   get   ( “food” ,   ?f   ) @ self .P work   ( f   ) +   put   ( “randomWalk”   ) @ self .P idle  P work   ( food   )   ,   put   ( “task” ,   “work”   ) @ self .  put   ( “moveTo” ,   food   ) @ self . qry   ( “reached” ,   food   ) @ self . (  get   ( “lock”   ) @( pos   =   f ood ) . put   ( “found”   ) @( pos   =   f ood ) .  put   ( “task” ,   “idle”   ) @ self .P idle  +  put   ( “task” ,   “idle”   ) @ self .P idle )  The syntax   ( “food” ,   ?f   )   denotes a template. In this case, the template is matched by all two-element tuples where the first element is   “food” : when such a tuple is found, it is removed from the repository and its second element is bound to the variable   f   . Like in most programming languages,   P work   ( f   )   denotes a parametric invocation, where the actual parameter   f   is bound to the formal parameter   food   . As stated in Section 3, we use special tuples, such as   moveTo   and   reached , to represent the start and stop of a movement. Notice that updating the value of an attribute, such as   task , needs no additional primitives, as it just can be obtained by manipulating items in the local repository. As said above, to pick up an item, a robot must first withdraw its   lock   tuple. If this is not possible, it means that another forager has already picked up the item: hence the robot simply turns back to the idle state.  4.2   Flocking  Flocking is an example of emerging behaviour where agents starts from a state of incoherent motion, but eventually agree to move in the same direction. This case study is a basic instance of a consensus problem, which is fundamental for many cooperative tasks (Valentini et al., 2017). Except for cases where the language provides better suited primitives, we will address this problem by specifying some variation on the   voter model . In a voter model, agents are seen as nodes in a graph that initially have different   opinion   about what to choose among a finite number of possibilities (Liggett, 2005). Furthermore, each agent can observe and copy the opinion of a random neighbour. A voter model  Frontiers   13
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  can either converge (i.e. all agents eventually adopt the same opinion) or oscillate, based on a number of factors, such as the initial distribution of opinions, the topology of the graph, etc.  Buzz . We can easily adopt a virtual stigmergy to make the swarm agree on a direction (Table 2).  Table 2.   Flocking in Buzz with virtual stigmergies.  function   init()   {  math .rng.setseed(id*id) my_yaw =   math .rng.uniform(0,   2.0   *   math .pi) vstig =   stigmergy .create(1) vstig.put("yaw",   my_yaw) }  function   step()   {  var   cur_yaw =   pose .orientation.yaw %   (2. *   math .pi)  var   err =   vstig.get("yaw")   -   cur_yaw control(err) }  In the   init()   function we use the squared ID of the agent as a seed for the pseudo-random number generator (PRNG): this is needed to make each agent behave differently. We then generate a random value for the direction and put it into a virtual stigmergy. At each execution step, robots retrieve the direction from the stigmergy by calling the   vstig.get()  function, and compute the current error (i.e the difference between the desired yaw angle and the current one). The   control()   function then rotates the robot if the error is too big, and makes it move forward otherwise. An elementary implementation of such a function is the following:  function   control(err)   {  if   ( math .abs(err)   > 0.5) { sign =   err /   math .abs(err) gotop(0,   sign * 2)   # Rotate (+/-   2 rad/s)  }  else   { gotop(3,   0)   # Move forward (3 cm/s)  } }  Each time a robot reads a value from the stigmergy, the Buzz virtual machine automatically asks its neighbours to confirm whether its local value is up-to-date. Neighbours either use this information to update their own local copies or to reply with a more recent value. This mechanism makes it easier for all robots to converge to a common value, even when parts of the swarm become temporarily disconnected from the rest. A basic voter model can also be described in Buzz. We can use the neighbour communication primitives to enable each robot to broadcast its chosen direction among its neighbours. Periodically, robots listen to the direction of a neighbour and change their own accordingly (Table 3). Here the condition   (t %   20) == 0   means that robots can only attempt to change their opinion once every 20 time steps. By altering the condition it is possible to simulate other kinds of models.  This is a provisional file, not the final typeset article   14
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  Table 3.   Flocking in Buzz: a voter-model approach.  t =   0  function   init()   {  math .rng.setseed(id*id) my_yaw =   math .rng.uniform(0,2) *   math .pi  neighbors .listen("yaw",   function (vid,   value,   rid)   {  if (value !=   my_yaw   and   (t %   20) ==   0) { my_yaw =   value log(id,   "   change to   ",   my_yaw) } }) }  function   step()   { t   = t   + 1  var   cur_yaw =   pose .orientation.yaw %   (2. *   math .pi)  var   err =   my_yaw - cur_yaw control(err)  neighbors .broadcast("yaw",   my_yaw) }  For instance,   the waiting time of each robot could follow an exponential (Cox, 1989) or power- law (Takaguchi and Masuda, 2011) distribution. The effects of   zealots , i.e. agents that never change their opinion (Mobilia et al., 2007), could also be studied.  ISPL . We decided not to rely on explicit communication between robots. To do so, we should create appropriate protocol and evolution rules for each pair of agents: therefore the size of the specification would grow quadratically with the number of robots. Our implementation, again, takes advantage of the  Environment   agent. Each robot starts with a random direction stored in its state. At any moment, a robot can move in its stored direction, or it can watch and imitate the direction of the last robot that moved.  Agent   Environment  Obsvars : dir :   {Up,   Down,   Left,   Right};  end   Obsvars  -- ...  Evolution : dir =   Up   if   (Robot1.Action = Up);  -- Repeat for all robots and directions  end   Evolution end Agent Agent   Robot1  Vars : x   : 1   .. 10; y   : 1   .. 10; dir :   {Up,   Down,   Left,   Right};  end   Vars Actions   = {Up, Down, Left, Right,   Watch};  Protocol : dir =   Up   and   y   <   10: {Up,   Watch};  Frontiers   15
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  -- Similarly for other directions  Other:   {Watch};  end   Protocol Evolution : dir =   Environment.dir   if   (Action = Watch); y   = y+1   if   (Action =   Up);  -- Similarly for other directions  end   Evolution end Agent  We define the protocol so that robots cannot move in their chosen direction if they are are on the edges of the arena. For instance, an agent at position   (3 ,   10)   cannot go in the   Up   direction. In these cases, robots can only perform the   Watch   action. We encode this with the special condition   Other , which holds in all the states that do not match the other protocol rules. In this case we were able to verify that two robots will always agree to move in the same direction, by checking a property of the form   AF   consensus   (for all possible executions, eventually the   consensus   proposition will hold). However, when there are three or more robots, the MCMAS model checker is able to find cyclic traces where consensus is never achieved. We can slightly alter the description of robots, so that they can move across an edge and get to the opposite side of the grid. For instance, a robot at   (1 ,   4)   will be able to move left and reach   (10 ,   4) . In other words, we consider a toroidal, rather than square, arena. With these changes we are unable to prove global properties about consensus, even for the two-robot case.  Protocol : dir   = Up   : {Up, Watch};  -- ...  end Protocol Evolution : y   =   1   if   (Action =   Up   and   y   =   10); y   =   y+1   if   (Action = Up   and   y   < 10);  -- ...  end Evolution  While   ISPL   cannot   express   voter   models   in   a   natural   way,   an   ad-hoc   version   of   the language (ISPL-OFP) has been implemented to model and verify an array of opinion formation protocols (Kouvaros and Lomuscio, 2016a).  SCEL . Modelling a basic voter model in SCEL is simple. Each component exposes its current position and direction, and uses the   qry   action to copy the direction of a neighbour. Due to the semantics of the action, a neighbour will be selected nondeterministically among the components that satisfy an attribute- based predicate. In this example the predicate relies on an additional attribute, storing the communication range of the component, and only targets neighbours exposing a different direction.  P   ,   qry   ( “direction” ,   ?d   ) @ ( ‖ pos   −   self . pos ‖ ≤   self . range   ∧   direction   6   =   self . direction )   .  put   ( “direction” , d   ) @ self .P  This is a provisional file, not the final typeset article   16
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  We can further refine this behaviour by introducing logical clocks (Lamport, 1978b), obtaining a protocol similar to the one of Buzz based on virtual stigmergies. Suppose that each component has a  ( “time” ,   0)   tuple. This value is also exposed as the   time   attribute of the component. We use this attribute to the   qry   predicate to ignore out-of-date neighbours. We also attach a timestamp to   direction   tuples. Whenever a component finds a neighbour with a timestamp   t   higher than its own, it sets its own clock to  t   + 1 . A similar approach can be taken to divide the computation into “rounds” and solve more complex problems, such as distributed graph coloring, see e.g., (Abd Alrahman et al., 2017).  P   ,   qry   ( “direction” ,   ?d ,   ?t   ) @ ( ‖ pos   −   self . pos ‖ ≤   self . range   ∧   time   ≥   self . time )   .  put   ( “time” , t   + 1 ) @ self .  put   ( “direction” , d, t   + 1 ) @ self .P  5   CONCLUSIONS, RELATED AND FUTURE WORK  In this work, we have described a number of features typically found in multi-robot systems. These traits can make MRSs hard to design, implement and reason about. We have presented a selection of languages, showing how specific linguistic primitives can help in the specification of such systems. We also compared the languages considering the tools that have been provided to support analysis of their systems. To better understand the strengths and weaknesses of each language, we considered two case studies that are popular in the MRS literature, and provided basic implementation in the surveyed languages. We used these implementations to show how specific abstractions provided by the languages facilitates modelling non-trivial behaviours. For instance, the presence of synchronous operations is vital for scenarios where the interaction with the environment is predominant. At the same time, we have seen that group-oriented forms of interaction, either among neighbours or based on the more general framework of attribute-based communication, allow for a more natural specification of non-trivial cooperation between agents. Our work is by no means an exhaustive review of the state of the art. We focused on choosing a meaningful set of features to allow an effective qualitative comparison of existing languages. Additional languages and frameworks could be the subject of further investigation. Describing and clarifying the factors that make MRSs distinctively challenging is also an important first step towards the specification of new MRS- oriented languages, which is another possible direction of research.  Related   work.   A   number   of   language   surveys   can   be   found   in   the   field   of   Multi-Agent Systems (Mascardi et al., 2005; Bordini et al., 2006; Feraud and Galland, 2017). As MASs are a superset of multi-robot systems, said surveys may lack detail and miss specific features highlighted in our work.   Surveys of robotics languages and platforms are also available (Kramer and Scheutz, 2007; Nordmann et al., 2014), but to the best of our knowledge they do not address the sources of complexity presented in this overview. Peculiar traits of complex systems in general, such as emergence, are also the subject of a substantial amount of research (Heylighen, 1989; Barab ́ asi and Albert, 1999; Odell, 2002). The literature also provides taxonomies for specific aspects found in MRSs, such as coordination (Yan et al., 2013) and task allocation (Gerkey and Matari ́ c, 2004).  Future work.   This work is for us instrumental to design a new language for multi-agent systems by building on the lesson learned from the three languages we have surveyed. The language we are aiming at should make it possible an intuitive design of local specifications and automated analysis of global properties and emerging behaviours. We will aim at a language that combines stigmergic interaction of  Frontiers   17
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  Buzz with the attribute-based communication of SCEL, whose agents will interact by manipulating and asynchronously propagating their limited share of knowledge. The language will be equipped with a formal semantics to enable automatic verification of logical properties by building on tools and methods developed for ISPL.  REFERENCES  Abd Alrahman, Y., De Nicola, R., and Loreti, M. (2017).   Programming the Interactions of Collective Adaptive Systems by Relying on Attribute-based Communication 0 Alur, R., Henzinger, T. A., and Kupferman, O. (2002). Alternating-time temporal logic.   Journal of the ACM   49, 672–713. doi:10.1145/585265.585270 Arai, T., Pagello, E., and Parker, L. E. (2002). Advances in multirobot systems.   IEEE Transactions on Robotics and Automation   18, 655–661. doi:10.1109/TRA.2002.806024 Arkin, R. C. (1992).   Cooperation without communication: Multiagent schema-based robot navigation.  Journal of Robotic Systems   9, 351–364. doi:10.1002/rob.4620090304 Bachrach, J., McLurkin, J., and Grue, A. (2008). Protoswarm: A language for programming multi-robot systems using the amorphous medium abstraction.   7th International Joint Conference on Autonomous agents and multiagent systems   3, 1175–1178 Barab ́ asi, A.-L. and Albert, R. (1999). Emergence of Scaling in Random Networks.   Science   286, 509–512. doi:10.1126/science.286.5439.509 Bayındır, L. (2016). A review of swarm robotics tasks.   Neurocomputing   172, 292–321. doi:10.1016/j. neucom.2015.05.116 Belzner, L., De Nicola, R., Vandin, A., and Wirsing, M. (2014).   Reasoning (on) Service Component Ensembles in Rewriting Logic. In   Specification, Algebra, and Software , eds. S. Iida, J. Meseguer, and K. Ogata (Berlin, Heidelberg: Springer), vol. 8373. 188–211. doi:10.1007/978-3-642-54624-2   10 Beni, G. (2005). From Swarm Intelligence to Swarm Robotics. In   Swarm Robotics , eds. D. Hutchison, T. Kanade,   J. Kittler,   J. M. Kleinberg,   F. Mattern,   J. C. Mitchell,   M. Naor,   O. Nierstrasz, C. Pandu Rangan, B. Steffen, M. Sudan, D. Terzopoulos, D. Tygar, M. Y. Vardi, G. Weikum, E. S  ̧ ahin, and W. M. Spears (Berlin, Heidelberg: Springer), vol. 3342. 1–9. doi:10.1007/978-3-540-30552-1   1 Birman, K. P. (1993). The process group approach to reliable distributed computing.   Communications of the ACM   36, 37–53. doi:10.1145/163298.163303 Bonani, M., Longchamp, V., Magnenat, S., R ́ etornaz, P., Burnier, D., Roulet, G., et al. (2010).   The marXbot, a miniature mobile robot opening new perspectives for the collective-robotic research.   In  2010 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2010)   (IEEE), 4187– 4193. doi:10.1109/IROS.2010.5649153 Bordini, R. H., Braubach, L., Dastani, M., El Fallah Seghrouchni, A., Gomez-Sanz, J. J., Leite, J., et al. (2006). A survey of programming languages and platforms for multi-agent systems 30, 33–44 Brambilla, M., Ferrante, E., Birattari, M., and Dorigo, M. (2013). Swarm robotics: A review from the swarm engineering perspective.   Swarm Intelligence   7, 1–41. doi:10.1007/s11721-012-0075-2 Brooks, R. A. (1991). Intelligence without Reason. In   12th International Joint Conference on Artificial Intelligence (IJCAI’91)   (Sidney: Morgan Kaufmann), 569—-595 Buchanan, E., Pomfret, A., and Timmis, J. (2016).   Dynamic Task Partitioning for Foraging Robot Swarms.   In   Swarm Intelligence , eds. M. Dorigo, M. Birattari, X. Li, M. L ́ opez-Ib ́ a ̃ nez, K. Ohkura, C. Pinciroli, and T. St ̈ utzle (Cham: Springer International Publishing), vol. 9882. 113–124.   doi:10. 1007/978-3-319-44427-7   10  This is a provisional file, not the final typeset article   18
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  Carriero, N. and Gelernter, D. (1989).   Linda in context.   Communications of the ACM   32, 444–458. doi:10.1145/63334.63337 Carriero, N. J., Gelernter, D., Mattson, T. G., and Sherman, A. H. (1994).   The Linda alternative to message-passing systems.   Parallel Computing   20, 633–655. doi:10.1016/0167-8191(94)90032-9 Castro, M., Druschel, P., Kermarrec, A.-M., and Rowstron, A. I. T. (2002).   Scribe: A large-scale and decentralized application-level multicast infrastructure.   IEEE Journal on Selected Areas in Communications   20, 1489–1499. doi:10.1109/JSAC.2002.803069 Clarke, E. M., Enders, R., Filkorn, T., and Jha, S. K. (1996).   Exploiting symmetry in temporal logic model checking.   Formal Methods in System Design   9, 77–104. doi:10.1007/BF00625969 Cox, J. T. (1989).   Coalescing Random Walks and Voter Model Consensus Times on the Torus in $ \ mathbb { Z } ˆ d$.   The Annals of Probability   17, 1333–1366. doi:10.1214/aop/1176991158 De Nicola, R., Latella, D., Lafuente, A. L., Loreti, M., Margheri, A., Massink, M., et al. (2015). The SCEL Language: Design, Implementation, Verification.   In   Software Engineering for Collective Autonomic Systems   (Springer), vol. 8998 of   LNCS . 3–71. doi:10.1007/978-3-319-16310-9   1 De Nicola, R., Lluch Lafuente, A., Loreti, M., Morichetta, A., Pugliese, R., Senni, V., et al. (2014a). Programming and verifying component ensembles.   In   From Programs to Systems. The Systems Perspective in Computing (ETAPS 2014)   (Springer),   vol.   8415 of   LNCS , 69–83.   doi:10.1007/ 978-3-642-54848-2   5 De Nicola, R., Loreti, M., Pugliese, R., and Tiezzi, F. (2014b). A Formal Approach to Autonomic Systems Programming.   ACM Transactions on Autonomous and Adaptive Systems   9, 1–29. doi:10.1145/2619998 Dorigo, M., Birattari, M., and Stutzle, T. (2006).   Ant colony optimization.   IEEE Computational Intelligence Magazine   1, 28–39. doi:10.1109/MCI.2006.329691 Fagin, R., Halpern, J. Y., Moses, Y., and Vardi, M. Y. (1995).   Reasoning about Knowledge   (Cambridge, Mass: MIT Press) Feraud, M. and Galland, S. (2017). First Comparison of SARL to Other Agent-Programming Languages and Frameworks.   Procedia Computer Science   109, 1080–1085. doi:10.1016/j.procs.2017.05.389 Fischer, M. J., Lynch, N. A., and Paterson, M. S. (1985). Impossibility of distributed consensus with one faulty process.   Journal of the ACM   32, 374–382. doi:10.1145/3149.214121 Flanagan, C. and Godefroid, P. (2005).   Dynamic partial-order reduction for model checking software.  ACM SIGPLAN Notices   40, 110–121. doi:10.1145/1047659.1040315 Gelernter, D. (1985).   Generative communication in Linda.   ACM Transactions on Programming Languages and Systems   7, 80–112. doi:10.1145/2363.2433 Gerkey, B. P. and Matari ́ c, M. J. (2004).   A Formal Analysis and Taxonomy of Task Allocation in Multi-Robot Systems.   The International Journal of Robotics Research   23, 939–954.   doi:10.1177/ 0278364904045564 Grass ́ e, P.-P. (1959). La reconstruction du nid et les coordinations interindividuelles chez Bellicositermes natalensis et Cubitermes sp. la th ́ eorie de la stigmergie: Essai d’interpr ́ etation du comportement des termites constructeurs.   Insectes Sociaux   6, 41–80. doi:10.1007/BF02223791 Hamann, H. (2018).   Swarm Robotics: A Formal Approach   (Cham: Springer International Publishing). doi:10.1007/978-3-319-74528-2 Heylighen, F. (1989). Self-Organization, Emergence and the Architecture of Complexity. In   Proceedings of the 1st European Conference on System Science (AFCET)   (Paris), 23–32 Heylighen, F. (2016).   Stigmergy as a universal coordination mechanism I: Definition and components.  Cognitive Systems Research   38, 4–13. doi:10.1016/j.cogsys.2015.12.002  Frontiers   19
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  Hillston, J. (2014). Challenges for Quantitative Analysis of Collective Adaptive Systems. In   Trustworthy Global Computing , eds. M. Abadi and A. Lluch Lafuente (Cham: Springer International Publishing), vol. 8358. 14–21. doi:10.1007/978-3-319-05119-2   2 Kephart, J. O. and Chess, D. M. (2003).   The vision of autonomic computing.   Computer   36, 41–50. doi:10.1109/MC.2003.1160055 Kong, J. and Lomuscio, A. (2017). Model Checking Multi-Agent Systems against LDLK Specifications. In   26th International Joint Conference on Artificial Intelligence (IJCAI 2017)   (California: International Joint Conferences on Artificial Intelligence Organization), 1138–1144. doi:10.24963/ijcai.2017/158 Kouvaros, P. and Lomuscio, A. (2016a).   Formal Verification of Opinion Formation in Swarms.   In  Proceedings of the 2016 International Conference on Autonomous Agents and Multiagent Systems  (Singapore, Singapore: International Foundation for Autonomous Agents and Multiagent Systems (AAMAS’16)), 1200–1208 Kouvaros, P. and Lomuscio, A. (2016b).   Parameterised verification for multi-agent systems.   Artificial Intelligence   234, 152–189. doi:10.1016/j.artint.2016.01.008 Kramer, J. and Scheutz, M. (2007). Development environments for autonomous mobile robots: A survey.  Autonomous Robots   22, 101–132. doi:10.1007/s10514-006-9013-8 Lamport, L. (1978a).   The implementation of reliable distributed multiprocess systems.   Computer Networks (1976)   2, 95–114. doi:10.1016/0376-5075(78)90045-4 Lamport, L. (1978b). Time, clocks, and the ordering of events in a distributed system.   Communications of the ACM   21, 558–565. doi:10.1145/359545.359563 Legay, A., Delahaye, B., and Bensalem, S. (2010).   Statistical Model Checking: An Overview.   In  International Conference on Runtime Verification (RV 2010)   (Springer), vol. 6418 of   LNCS , 122–135. doi:10.1007/978-3-642-16612-9   11 Liggett, T. M. (2005).   Interacting Particle Systems . Classics in Mathematics (Berlin, Heidelberg: Springer Berlin Heidelberg). doi:10.1007/b138374 Lomuscio, A., Qu, H., and Raimondi, F. (2017).   MCMAS: An open-source model checker for the verification of multi-agent systems.   International Journal on Software Tools for Technology Transfer  19, 9–30. doi:10.1007/s10009-015-0378-x Mascardi, V., Demergasso, D., and Ancona, D. (2005). Languages for Programming BDI-style Agents: An Overview.   In   WOA 2005: Dagli Oggetti Agli Agenti. 6th AI*IA/TABOO Joint Workshop “From Objects to Agents”: Simulation and Formal Analysis of Complex Systems , eds. F. Corradini, F. D. Paoli, E. Merelli, and A. Omicini (Camerino, Italy: Pitagora Editrice Bologna), 9–15 Matari ́ c, M. J. (1993). Designing Emergent Behaviors: From Local Interactions to Collective Intelligence. In   From Animals to Animats 2. Second International Conference on Adaptive Behavior   (Honolulu, Hawai, USA: MIT Press), 432–441 Matari ́ c, M. J. (1995). Issues and approaches in the design of collective autonomous agents.   Robotics and Autonomous Systems   16, 321–331. doi:10.1016/0921-8890(95)00053-4 Mobilia, M., Petersen, A., and Redner, S. (2007). On the role of zealotry in the voter model.   Journal of Statistical Mechanics: Theory and Experiment   2007, P08029–P08029. doi:10.1088/1742-5468/2007/ 08/P08029 Montanari, U., Pugliese, R., and Tiezzi, F. (2015).   Programming Autonomic Systems with Multiple Constraint Stores. In   Software, Services, and Systems   (Cham: Springer), vol. 8950 of   LNCS . 641–661. doi:10.1007/978-3-319-15545-6   36  This is a provisional file, not the final typeset article   20
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  Nikou, A., Tumova, J., and Dimarogonas, D. V. (2016). Cooperative task planning of multi-agent systems under timed temporal specifications. In   2016 American Control Conference (ACC 2016)   (IEEE), 7104– 7109. doi:10.1109/ACC.2016.7526793 Nordmann, A., Hochgeschwender, N., and Wrede, S. (2014). A Survey on Domain-Specific Languages in Robotics.   In   Simulation, Modeling, and Programming for Autonomous Robots. 4th International Conference   { SIMPAR 2014) , eds. D. Brugali, J. F. Broenink, T. Kroeger, and B. A. MacDonald (Cham: Springer International Publishing), vol. 8810 of   LNCS , 195–206. doi:10.1007/978-3-319-11900-7   17 Odell, J. (2002). Agents and Complex Systems.   The Journal of Object Technology   1, 35. doi:10.5381/jot. 2002.1.2.c3 Pinciroli, C. and Beltrame, G. (2016).   Buzz: An extensible programming language for heterogeneous swarm robotics. In   2016 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2016)   (IEEE), 3794–3800. doi:10.1109/IROS.2016.7759558 Pinciroli, C., Lee-Brown, A., and Beltrame, G. (2016).   A Tuple Space for Data Sharing in Robot Swarms.   In   Proceedings of the 9th EAI International Conference on Bio-Inspired Information and Communications Technologies (Formerly BIONETICS)   (ACM). doi:10.4108/eai.3-12-2015.2262503 Pinciroli, C., Trianni, V., O’Grady, R., Pini, G., Brutschy, A., Brambilla, M., et al. (2012).   ARGoS: A modular, parallel, multi-engine simulator for multi-robot systems.   Swarm Intelligence   6, 271–295. doi:10.1007/S11721-012-0072-5 Pitonakova, L. and Bullock, S. (2013). Controlling ant-based construction. In   12th European Conference on the Synthesis and Simulation of Living Systems (ECAL 2013)   (MIT Press), 2003, 151–158. doi:10. 7551/978-0-262-31709-2-ch023 Pitonakova, L., Crowder, R., and Bullock, S. (2016). Information flow principles for plasticity in foraging robot swarms.   Swarm Intelligence   10, 33–63. doi:10.1007/s11721-016-0118-1 Pitonakova, L., Crowder, R., and Bullock, S. (2017).   Behaviour-data relations modelling language for multi-robot control algorithms. In   2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2017)   (IEEE), 727–732. doi:10.1109/IROS.2017.8202231 Rubenstein, M., Ahler, C., and Nagpal, R. (2012). Kilobot: A low cost scalable robot system for collective behaviors. In   2012 IEEE International Conference on Robotics and Automation (ICRA 2012)   (IEEE), 3293–3298. doi:10.1109/ICRA.2012.6224638 Schiex, T., Fargier, H., and Verfaillie, G. (1995).   Valued Constraint Satisfaction Problems: Hard and Easy Problems. In   14th International Joint Conference on Artificial Intelligence (IJCAI’95)   (Morgan Kaufmann Publishers Inc.), 631–637 Støy, K. (2001).   Using Situated Communication in Distributed Autonomous Mobile Robotics.   In  Proceedings of the 7th Scandinavian Conference on Artificial Intelligence (SCAI’01) , eds. H. H. Lund, B. H. Mayoh, and J. W. Perram (IOS Press), vol. 66 of   Frontiers in Artificial Intelligence and Applications , 44–52 Takaguchi, T. and Masuda, N. (2011). Voter model with non-Poissonian interevent intervals.   Physical Review E   84. doi:10.1103/PhysRevE.84.036115 Theraulaz, G. and Bonabeau, E. (1999). A Brief History of Stigmergy.   Artificial Life   5, 97–116. doi:10. 1162/106454699568700 Ulusoy, A., Smith, S. L., Ding, X. C., Belta, C., and Rus, D. (2013).   Optimality and Robustness in Multi-Robot Path Planning with Temporal Logic Constraints.   The International Journal of Robotics Research   32, 889–911. doi:10.1177/0278364913487931  Frontiers   21
De Nicola et al.   Towards formal models and languages for verifiable Multi-Robot Systems  Valentini,   G.,   Ferrante,   E.,   and Dorigo,   M. (2017).   The Best-of-n Problem in Robot Swarms: Formalization, State of the Art, and Novel Perspectives.   Frontiers in Robotics and AI   4.   doi:10. 3389/frobt.2017.00009 Vasic, M. and Billard, A. (2013). Safety issues in human-robot interactions. In   2013 IEEE International Conference on Robotics and Automation (ICRA 2013)   (IEEE), 197–204.   doi:10.1109/ICRA.2013. 6630576 Werfel, J., Bar-Yam, Y., and Nagpal, R. (2005). Building patterned structures with robot swarms. In   19th International Joint Conference on Artificial Intelligence (IJCAI 2005) . 1495–1502 Weyns, D. and Holvoet, T. (2004).   A Formal Model for Situated Multi-Agent Systems.   Fundamenta Informaticae   63, 125–158 Weyns, D., Schumacher, M., Ricci, A., Viroli, M., and Holvoet, T. (2006). Environments in multiagent systems.   The Knowledge Engineering Review   20, 127. doi:10.1017/S0269888905000457 Yan, Z., Jouandeau, N., and Cherif, A. A. (2013). A Survey and Analysis of Multi-Robot Coordination.  International Journal of Advanced Robotic Systems   10, 399. doi:10.5772/57313  This is a provisional file, not the final typeset article   22