Related papers: Computer Aided Formal Design of Swarm Robotics Alg…

Social insects in nature such as ants, termites and bees construct their colonies collaboratively in a very efficient process. In these swarms, each insect contributes to the construction task individually showing redundant and parallel…

Formal methods provide remarkable tools allowing for high levels of confidence in the correctness of developments. Their use is therefore encouraged, when not required, for the development of systems in which safety or security is…

Integrated Task and Motion Planning (ITMP) for mobile robots in a dynamic environment with moving obstacles is a challenging research question and attracts more and more attentions recently. Most existing methods either restrict to static…

Developing reusable software for mobile robots is still challenging. Even more so for swarm robots, despite the desired simplicity of the robot controllers. Prototyping and experimenting are difficult due to the multi-robot setting and…

Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised implementations can be generated automatically. Theory of…

We apply a compositional formal modeling and verification method to an autonomous aircraft taxi system. We provide insights into the modeling approach and we identify several research areas where further development is needed. Specifically,…

This paper describes a formalization of discrete real closed fields in the Coq proof assistant. This abstract structure captures for instance the theory of real algebraic numbers, a decidable subset of real numbers with good algorithmic…

Swarm based optimization algorithms have demonstrated remarkable success in solving complex optimization problems. However, their widespread adoption remains sceptical due to limited transparency in how different algorithmic components…

A swarm algorithm framework (SWAF), realized by agent-based modeling, is presented to solve numerical optimization problems. Each agent is a bare bones cognitive architecture, which learns knowledge by appropriately deploying a set of…

Coordination behavior in robot swarms is inherently multi-modal in nature. That is, there are numerous ways in which a swarm of robots can avoid inter-agent collisions and reach their respective goals. However, the problem of generating…

Swarm robotics is a promising approach for the coordination of large numbers of robots. While previous studies have shown that evolutionary robotics techniques can be applied to obtain robust and efficient self-organized behaviors for robot…

We explore a simplified class of models we call swarms, which are inspired by the collective behavior of social insects. We perform a mean-field stability analysis and perform numerical simulations of the model. Several interesting types of…

We present an algorithm to solve the problem of locating the source, or maxima, of a scalar field using a robot swarm. We demonstrate how the robot swarm determines its direction of movement to approach the source using only field intensity…

Autonomous systems are highly complex and present unique challenges for the application of formal methods. Autonomous systems act without human intervention, and are often embedded in a robotic system, so that they can interact with the…

Cloud solutions are increasingly used for a plethora of purposes, including solving memory-intensive and computation-intensive problems. Ensuring the reliability, availability, scalability, and security of cloud solutions, as networked…

The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as…

Matching logic is a formalism for specifying, and reasoning about, mathematical structures, using patterns and pattern matching. Growing in popularity, it has been used to define many logical systems such as separation logic with recursive…

Studies of human-robot interaction in dynamic and unstructured environments show that as more advanced robotic capabilities are deployed, the need for cooperative competencies to support collaboration with human problem-holders increases.…

Computer Algebra systems are widely spread because of some of their remarkable features such as their ease of use and performance. Nonetheless, this focus on performance sometimes leads to unwanted consequences: algorithms and computations…

We propose a novel approach for the formal verification of biological systems based on the use of a modal linear logic. We show how such a logic can be used, with worlds as instants of time, as an unified framework to encode both biological…