# Knowledge in multi-robot systems: an interplay of dynamics, computation and communication

Giorgio Cignarale, Stephan Felber, Eric Goubault, Bernardo Hummes Flores, Hugo Rincon Galeana

<figure><img src="image_1.png" /></figure>

## To cite this version:

Giorgio Cignarale, Stephan Felber, Eric Goubault, Bernardo Hummes Flores, Hugo Rincon Galeana.
Knowledge in multi-robot systems: an interplay of dynamics, computation and communication. 2025.
hal-05413842

HAL Id: hal-05413842

https://hal.science/hal-05413842v1

Preprint submitted on 12 Dec 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Knowledge in multi-robot systems: an interplay of dynamics, computation and communication

Giorgio Cignarale ✉️ ID

TU Wien, Vienna, Austria

Stephan Felber ✉️ ID

TU Wien, Vienna, Austria

Eric Goubault ✉️ ID

École Polytechnique, Palaiseau, France

Bernardo Hummes Flores ✉️ ID

École Polytechnique, Palaiseau, France

Hugo Rincon Galeana ✉️ ID

TU Berlin, Berlin, Germany

## Abstract

In this paper, we provide a framework integrating distributed multi-robot systems and temporal epistemic logic. We show that continuous-discrete hybrid systems are compatible with logical models of knowledge already used in distributed computing, and demonstrate its usefulness by deriving sufficient epistemic conditions for exploration and gathering robot tasks to be solvable. We provide a separation of the physical and computational aspects of a robotic system, allowing us to decouple the problems related to each and directly use methods from control theory and distributed computing, fields that are traditionally distant in the literature. Finally, we demonstrate a novel approach for reasoning about the knowledge in multi-robot systems through a principled method of converting a switched hybrid dynamical system into a temporal-epistemic logic model, passing through an abstract state machine representation. This creates space for methods and results to be exchanged across the fields of control theory, distributed computing and temporal-epistemic logic, while reasoning about multi-robot systems.

2012 ACM Subject Classification Computer systems organization → Robotics; Theory of computation → Modal and temporal logics; Theory of computation → Distributed computing models

**Keywords and phrases** distributed computing, mobile robotics, temporal-epistemic logic, switched system, robot tasks

## 1 Introduction

We formulate in this paper a framework connecting a hybrid systems approach to distributed multi-robot systems and temporal epistemic logic. This forms a bridge whose value is twofold: we bring the success of logical analysis of tasks in distributed computing [17] to distributed robotics, and we generalize the multi-robot model from state machines to dynamical systems [33], drawing a much closer frontier to real-life applications.

The distributed coordination of robots combines problems found in control theory [25, 35] with the problems commonly found in distributed computing [30]. By clearly separating the roles of the physical and computational parts of a robot, we are capable of showing a translation layer from distributed computing and control theory. While robotics is traditionally concerned with physical entities that must behave in accordance to their dynamical constraints, the distributed computing perspective arises once the robots must exchange information under varying difficulties associated to their communication capacities [1, 12]. For instance, understanding the impact of synchrony, coordination and message loss are essential for the efficient design and analysis of state-of-the-art multi-robot systems solving
2 Knowledge in multi-robot systems

various tasks.

Our modeling is extended for the multi-robot scenario, where we introduce the notion of a scheduler as a path in the space of executions, so to tie local to global time. Bridging these fields enables us to combine well-known methods and results from control theory, distributed computing and temporal epistemic logic in a simple and harmonious fashion. Our framework successfully captures the spatial information used to reason about multi-robot tasks, namely exploration and gathering, as it is constructed with the memory of the robots during their computations. We devise a logical model consisting of a variation of the runs and systems framework, which we construct by defining explicitly a distributed state machine for both the system dynamics and the robot protocols. We further demonstrate the usefulness of our approach by deriving the first ever sufficient epistemic conditions for solving the exploration, approximate gathering and surveillance robot tasks.

In [1] the authors famously showed that exact gathering is impossible by reducing the robot task to the consensus problem in distributed computing and deriving its well understood impossibility borders from there. In essence, the present paper puts this reduction on a sound footing by deriving the distributed system implied by the control theoretic model and equipping it with the tools found in epistemic logic.

The distributed computing community has approached the characterization of tasks in distributed robot systems [18] in various ways, such as according to the system space (continuous or discrete) [3, 11], communication capacities [37] and synchronicity [26]. Model checking using linear temporal logic is also a common tool in this computational perspective of robotics, where it has been used for gathering [14], perpetual exploration [5, 13] and terminating exploration [5].

The control theoretic view on multi-agent systems has been developed by a number of authors, see e.g. the survey [4]. Similarly, logical views on hybrid systems have been considered, see e.g. [32]. As we mentioned also, logics, in particular epistemic logic [22] and temporal-epistemic logic [27] have been developed and applied to multi-agent systems, through in particular epistemic planning [15].

Epistemic logic [23] is a powerful conceptual tool for reasoning about the uncertainty of agents in a system, both regarding facts and other agents' epistemic states, making it especially suitable for the modeling of multi-agent systems, including distributed systems. It was adapted for and introduced to distributed systems in [22], subsequently employed to characterize: the firing rebels with relay in [19], two agent approximate consensus in [28], sufficient conditions for stabilizing consensus in [8], optimal consensus with respect to message transmission in [20] and different notions of knowledge in [31], to name just a few. A crucial feature of epistemic logic in multi-agent systems is that it provides a precise and formal representation of higher order epistemic attitudes, such as nested and/or common knowledge, often crucial for the success of distributed tasks. For instance, coordinated actions are inevitably tied to nested knowledge, i.e., any agent needs to know to some extent what other agents know in order to successfully execute a coordinated behavior [31]. Another interesting feature of epistemic logic is that, when combined with temporal logic, it allows to express properties that must hold (and be known) throughout the execution, without focusing on the specific communication mechanisms leading to such knowledge. Thus, epistemic logic is a universal vehicle for expressing communication models, including those that rely on lack of explicit communication (also known as communication by silence) [19, 20]. Our approach is the first one to seamlessly integrate these three complementary views: the ones from control theory, distributed systems and temporal epistemic logic.

**Contributions.** We present, to the extent of our knowledge, the first interdisciplinary
framework that connects all three fields of control theory, distributed computing, and temporal epistemic logic, in a general setting that enables a comprehensive and integral approach to multi-robot systems. We showcase the potential of our framework by defining a simple yet sufficiently expressive temporal epistemic language that allows us to express multi-layered knowledge of space. In particular, this enables a precise formalization for the completion of spatial robotic tasks, such as exploration and approximate gathering. More precisely, our main contributions are:

- We define a robot abstraction representing multi-robot system (Definition 3) executions compatible with to both the control theory (Definition 1) and distributed computing (Definitions 4 and 5) frameworks.

- We provide a temporal epistemic logic framework (Definition 15), based on the runs and systems framework, for expressing robot exploration as knowledge of atomic propositions that represent open sets of a compact topological space.

- We provide an epistemic analysis of exploration (Definition 18), and approximate gathering (Definition 30). Furthermore, we characterize exploration with cooperative termination (Theorem 25), and we prove that the sufficient conditions to solve approximate gathering mimic the sufficient conditions for the stabilizing agreement problem in distributed systems (Theorem 32).

**Paper Organization.** In Section 2 we introduce the basic concepts used for modeling multiple robots: first as a system of ordinary differential equations (Section 2.1), then as state machines (Section 2.2). In Section 3, we introduce time paths as a geometric model relating global and local times (Section 3.1), followed by their usage in the definitions of runs in both dynamical (Section 3.2) and computational models (Section 3.3). We conclude by showing that the computational content of these runs match (Section 3.4). Section 4, the main contribution of the paper, connects the robotic abstraction to the epistemic modeling by turning the abstract robot state machine into a suitable epistemic frame. The latter is enriched into an epistemic model (Section 4.1), which is then used for the epistemic analysis of robot tasks such as simple exploration (Section 4.2) and approximate gathering (Section 4.3). Finally, concluding thoughts are provided in Section 5.

## 2 The Robot Model

In this section, we introduce two multi-robot system models with distinct degrees of abstractions, and subsequently show one model to be an abstraction of the other. The first is a description of robots as a switched hybrid dynamical system, close to models found in the control theory literature [24]. The second is a state machine executing LOOK-COMPUTE-MOVE cycles, an abstraction commonly found in the distributed computing community [18].

### 2.1 Robots as Dynamical Systems

From the dynamical systems perspective, a robotic system can be modeled via differential equations that describe the evolution of its state over time. Hybrid systems combine a continuous state space, associated to the physical features of a robot, with a discrete space, more natural to capture computations. We start by describing the model for a single robot.

► **Definition 1 (Robot).** A robot is a hybrid system, composed of an ontic state *x* and epistemic state *e*. It has actuators that evolve its ontic state and sensors that perform
4 Knowledge in multi-robot systems

observations. It has an intelligence and a memory that generate new epistemic states and control commands.

$$
\dot{\mathbf{x}}(t) = f(\mathbf{x}(t), \mathbf{u}[t]) \qquad (\text{ontic evolution}) \qquad (1)
$$

$$
\mathbf{y}(t) = g(\mathbf{x}(t)) \qquad (\text{observation}) \qquad (2)
$$

$$
\mathbf{e}[t+1] = \varphi(\mathbf{e}[t], \mathbf{y}[t]) \qquad (\text{epistemic evolution}) \qquad (3)
$$

$$
\mathbf{u}[t] = h(\mathbf{e}[t], [t]) \qquad (\text{control}) \qquad (4)
$$

The ontic evolution *f* and the observation *g* occur in continuous time *t*, while the epistemic evolution *φ* and the control *h* occur in discrete time [*t*], defined by the staircase function ⌊*t*⌋.

The ontic state corresponds to the physical state of the robot, while the epistemic state
corresponds to the memory state of the robot. The distinction between the ontic and
epistemic states allows for physical and computational problems to be described separately.
As such, a robot's behavior is given by a (hybrid) switched system [29], a particular case of
hybrid system, as the control **u**[t] is possibly discontinuous over time.

Note that Definition 1 also encompasses more traditional models of robots in the control-theoretic literature, such as output-feedback controllers [25]. This can be achieved by using the epistemic evolution $\varphi$ as a simulator that imitates the dynamics of the model.

► **Remark 2 (Discrete Observations).** Due to the physical limitations in memory of any physical computing device, we assume that the observation function *g* has a finite domain *D*(*g*), which corresponds to the digital representation of the continuous quantities it is capable of measuring.

We now consider the modifications required for modeling a multi-robot system where
interactions increase in complexity with the added notions of communication and perception
among robots. Note that the distinction between communication and perception is a
consequence of the distinction between ontic and epistemic states, as both are required to
represent the possible information to be exchanged. For two robots **r** and **r'**, they are defined
via a pair of functions.

$$
\hat{\mathbf{x}}_{rr'}(t) = \eta_r(\mathbf{x}_{r'}(t)) \qquad (\text{perception}) \qquad (5)
$$

$$
\hat{\mathbf{e}}_{rr'}[t] = \lambda_r(\mathbf{e}_{r'}[t]) \qquad (\text{communication}) \qquad (6)
$$

The perception is $\hat{\mathbf{x}}_{r,r'}$ is the estimation of the ontic state of robot $\mathbf{r}'$ by robot $\mathbf{r}$. Similarly, The communication function generates the estimation $\hat{\mathbf{e}}_{r,r'}$ of the epistemic state of robot $\mathbf{r}'$ by robot $\mathbf{r}$. Moreover, the introduction of multiple robots operating in the system brings forward the notions of "local" and "global" execution time, which will be formalized in Section 3.1.

Communication and perception complement the observation step with information about
the other robots. These multiple pieces of information are later processed together by the
robot's epistemic evolution, matching the intuition of observations as simply inputs to a
computing system. This leads to the definition of a hybrid multi-robot system.

**► Definition 3 (Hybrid multi-robot system).** A *hybrid multi-robot system H* consists of *N* robots, capable of observing the environment and interacting with the other robots through perception and communication. For a given sequence of activations *p*, its evolution is given
by:

$$ \dot{\mathbf{X}}(t) = F_p(\mathbf{X}(t), \mathbf{U}[t]) \qquad (\text{global ontic evolution}) \qquad (7) $$

$$ \mathbf{Y}(t) = G(\mathbf{X}(t), \eta(\mathbf{X}(t)), \lambda(\mathbf{E}[t])) \qquad (\text{multi-robot observation}) \qquad (8) $$

$$ \mathbf{E}[t+1] = \Phi(\mathbf{E}[t], \mathbf{Y}(t)) \qquad (\text{global epistemic evolution}) \qquad (9) $$

$$ \mathbf{U}[t] = H(\mathbf{E}[t], t) \qquad (\text{global control}) \qquad (10) $$

This definition is a consequence of the evolution of single robots alongside the interaction functions, as in Definition 1 and Equations (5) and (6). We now consider a generic scheduler that provides the set of active robots at each time t, defining the modes of the switched system, and that will be made precise with the introduction of time paths in Section 3.1.

## 2.2 Robots as Mobile Computing Systems

We provide now a state machine abstraction that allows us to focus on the computational component of the robots in Definition 1. Robots are algorithmically described as mobile entities that follow a cycle of LOOK-COMPUTE-MOVE operations as they interact with the environment. This is known as the LCM cycle [18]:

1. **LOOK**. The robot retrieves a snapshot of the ontic state of other robots in the environment.

2. **COMPUTE**. The robot computes its next epistemic state from the information in **LOOK**.

3. **MOVE**. The robot updates its physical state based on its current epistemic state.

4. **WAIT**. The robot does not perform any action, but remains observable.

All robots operate in the same environment, e.g. a graph or continuous region of space. Uncertainty in the behavior of each step, such as the accuracy of the information or the actual moved distance, are possible choices for adversarial behavior in the LCM model. Some variations are depicted in Appendix A.

Two models for robots running LCM cycles are predominant in the literature: oblivious, introduced in [36], and luminous, introduced in [10]. They contrast in the means for communication and memory made available to the robots. Robots under the oblivious robot model, OBLOT, have no memory and can only obtain information from observing other robots in the LOOK step. Robots under the luminous robot model, LUMI, are enhanced with a set of programmable lights that can be user for both (indirect) communication and storing information for future COMPUTE steps. The lights are a physical element representing the exposed memory of a robot, and hence can be observed with the rest of the ontic state of a robot during LOOK operations and are updated during a MOVE operation. We will use the LUMI model, as we require the lights to handle both communication and perception. We instantiate the robot r in an environment $\mathcal{E}$ executing A as follows.

**► Definition 4 (Robot state machine).** A robot r executes the state machine
$\mathcal{A} = \langle S_{e_r}, S_{y_r}, S_{u_r}, g_r, \varphi_r, h_r \rangle$ where

■ $S_{e_r}$ is a finite set of possible memory states;

■ $S_{y_r}$ is a finite set of possible observations obtained from the environment $\mathcal{E}$;

■ $S_{u_r}$ is a set of actions that can be executed in the environment $\mathcal{E}$;

■ $g: \mathcal{E} \to S_{y_r}$ is the function that retrieves an observation from the current environment $\mathcal{E}$;

■ $\varphi: S_{e_r} \times S_{y_r} \to S_{e_r}$ is a function taking an epistemic state and an observation to a new epistemic state;

■ $h: S_{e_r} \to S_{u_r}$ is a function that generates an action given an epistemic state.
The environment itself is dynamic and therefore also a state machine. It provides the
observations used by the robots during their execution of A and evolves according to the
robots' actions and some possible adversarial factor. It abstracts the ontic state of all robots
as a single entity, with which all of the robot state machines interact.

► **Definition 5 (Environment state machine).** *The environment executes the state machine*
*E = ⟨S_E, I_B, {S_{u_r}}_{r∈Π}, {S_{y_r}}_{r∈Π}, F_E, G_E⟩ where*

- $S_{\mathcal{E}}$ is a set of possible environment states;

- $I_B$ is a set of possible choices made by the adversary;

- {$S_{\mathbf{u}_r}$}$_{r \in \Pi}$ is a collection of possible robot actions;

- {$S_{y_r}$}$_{r \in \Pi}$ is a collection of possible observations;

- $F_{\mathcal{E}} : S_{\mathcal{E}} \times \prod_{r \in \Pi} S_{\mathbf{u}_r} \times I_B \rightarrow S_{\mathcal{E}}$ is the function generating a new environment state from
  the latest actions and the adversarial interference;

- $G_{\mathcal{E}} : S_{\mathcal{E}} \times I_B \rightarrow \prod_{r \in \Pi} S_{y_r}$ is the function that generates observations from the current environment state and possible adversarial interference.

Definition 4 lets us focus on the computations executed locally, while Definition 5 abstracts the ontic states and updates of all robots in a single machine interacting with the individual computations. *LOOK* and *MOVE* are split into distinct functions at the interface between the environment and each robot: the data is “prepared” by $h_r$ and $G_{\mathcal{E}}$, and “consumed” by $F_{\mathcal{E}}$ and $g_r$.

A computational multi-robot system $\mathcal{C}$ is then a set of robots and one environment state machine, i.e., $\mathcal{C} = (\{\mathcal{A}_r\}_{r \in \Pi}, \mathcal{E})$. This separation will facilitate stating the correspondence between computational and dynamical perspectives in Section 3.4.

3 Schedulers and System Runs

In this section, we define a scheduler (Section 3.1) that dictates the possible activations of
the distributed system. System runs are thus introduced, in both the dynamical (Section 3.2)
and computational (Section 3.3) definitions. The runs will be later used as building blocks
to generate a general epistemic frame for multi-robot tasks in Section 4.

**3.1 Scheduler: Global and Local Time**

The robots' order of activation is given by a scheduler, which chooses the robot that
will execute the next step of its cycle. Common schedulers found in the literature are
the synchronous, where all steps happens simultaneously, semi-synchronous, where the
synchronization is guaranteed at every full cycle, and asynchronous, where there is no shared
notion of time. See [18] for more details on the taxonomy of schedulers. A scheduler that is
not fully synchronous may lead to a global time that differs from the local time of the robots.

We introduce a time path to capture the relationship between the local execution of the robots and a common global time variable. A set of *n* robots induces a space of possible executions $\mathbb{R}_+^n$, LCM cycles are mapped to each sequential unit interval. Any monotonic increasing path rooted in the origin of this space defines a possible execution order of the system. Each coordinate of $\mathbb{R}_+^n$ corresponds to the local time of a robot, and the length of the path corresponds to the global time. A robot is said to execute a step whenever a path's projection to the corresponding local time axis crosses said step's activation point. This leads to the following definition.
**► Definition 6 (Time path).** For a system of n robots, a *time path* is a differentiable map $p$, from $[0, T]$ to $\mathbb{R}_+^n$, for some $T \ge 0$, that has the following properties:

- (initialisation) $p(0) = (0, \dots, 0)$.

- (monotonicity) For any $t, t' \in [0, T]$ with $t \le t'$, $p_i(t) \le p_i(t')$, for all components $i \in [1, \dots, n]$.

- (rectification) For all $t \in [0, T]$, the global time $t$ is the maximum of all local times, i.e.,
  $t = \max(|p_1(t) - p_1(0)|, |p_2(t) - p_2(0)|, \dots, |p_n(t) - p_n(0)|)$.

A time path defines the relative progress of every robot, where the monotonicity property makes time always go forwards, and the rectification property sets the global time to match the fastest local time. A scheduler is then a family of time paths. For instance, a synchronous scheduler can only correspond to a diagonal straight line, where all operations are aligned. A semi-synchronous scheduler will have any of its possible time paths crossing all `COMPUTE` steps simultaneously, where synchronization happens. In the case of instantaneous moves, as in [1], the behavior of robots would be undefined at points where a `LOOK` operation would happen at the same time as a `MOVE` operation, and consequently one should forbid access to points near the intersection of `MOVE` and `LOOK` operations. Such forbidden zones (represented as small squares) and two possible executions of a multi-robot system composed of two robots is illustrated in Figure 1.

<figure><img src="image_3.png" /><figcaption>■ **Figure 1** Two global time paths, blue and red, represent different possible executions of robots with local times $[t]_1$ and $[t]_2$. Each robot executes the sequence of actions (M) update ontic state, (L) observe environment and other robots, (C) update epistemic state. Each moment the time path crosses a dotted line, the associated robot executes the corresponding action. The squares are used to distinguish paths with different activation orders, as a `LOOK` operation before and after a `MOVE` provides different amounts of information. The actions are indexed by the cycle they belong to.</figcaption></figure>

In the following, we use $t$ for the continuous time and $[t]$ for discrete time, as per Definition 1. A subscript with the robot identifier is used to depict local time, as in $t_r$ or $[t]_r$, and its absence represents global time. Given a time path $p$, the local time of robot $r$ is given by $t_r$ or $[t]_r$, depending on whether it is continuous or discrete.

## 3.2 Dynamical Runs of Distributed Multi-Robot System

We attest now the uniform treatment of time provided by the scheduler by bridging the understanding of system runs of robots as dynamical systems (Section 2.1) similarly to that of computing systems (Section 2.2).
Given a time path $p$, the hybrid dynamics in global time coordinates $\mathbf{X}(t) = \mathbf{x}(p_i(t))$ for every robot $i$ satisfy

$$ \dot{\mathbf{X}}(t) = F_p(\mathbf{X}(t), \mathbf{U}[t]) = \langle \dot{p}, f(\mathbf{X}(t), \mathbf{U}[t]) \rangle $$

where $\langle \cdot, \cdot \rangle$ denotes the scalar product in $\mathbb{R}^n$. This connect the scheduler to the physical evolution via the time path.

For simplicity, we assume that all robots live in a hypercube bounded by the $[0, 1]^k$, with $k \ge 1$, along with its standard Euclidean metric, i.e. $d(\bar{x}, \bar{y}) = \sqrt{\sum_{i=1}^k (x_i - y_i)^2}$, where $\bar{x} = (x_1, \dots, x_k)$ and $\bar{y} = (y_1, \dots, y_k)$. We consider only the case of homogeneous multi-robot systems, equipped with identical capacities and behavior, but note that the described model does not limit to such case.

The (arbitrary) switched system of Definition 3 has a notion of solution, which will be used later as the dynamical system version of “runs”. For this, we need to see our switched system as a more general differential inclusion:

**Definition 7 (Solutions to differential inclusions [2]).** Consider the general differential inclusion $\dot{x} \in \mathbb{F}(x)$ where $\mathbb{F}$ is a map from $\mathbb{R}^n$ to $\mathcal{P}(\mathbb{R}^n)$, the set of subsets of $\mathbb{R}^n$. A function $x(\cdot) : \mathbb{R}^+ \to \mathbb{R}^n$ is a **solution** to the inclusion if $x$ is an absolutely continuous function and satisfies for almost all $t \in \mathbb{R}$, $\dot{x}(t) \in \mathbb{F}(x(t))$.

In general, there can be many solutions to a differential inclusion. Throughout the section we note $S_F(x_0)$ the set of all (absolutely continuous) solutions to the differential inclusion.

In some cases, we can be more precise about the solution set. By the Filippov-Wažewski theorem [29], all solutions to the (closure of the) convexification of a differential inclusion can be approximated by solutions of the original differential inclusion with the same initial value, at least over a compact time interval, and under some simple hypotheses. And the solutions of the closure of the convexification of the original differential inclusion exist under simple hypotheses:

We know from [2] that when $\mathbb{F}$ is a Marchaud map, then the inclusion has a solution such that $x(t_0) = x_0$ (for all $x_0$) and for a sufficiently small time interval $[t_0, t_0 + \varepsilon)$, $\varepsilon > 0$. Global existence, for all $t \in \mathbb{R}$ can be shown provided $\mathbb{F}$ does not allow “blow-up” ($\|x(t)\| \to \infty$ as $t \to t^*$ for a finite $t^*$).

The solutions to the switched system in Definition 3 provide the dynamical runs, treated as a differential inclusion defined on time $[0, T]$, as follows. The **dynamical run** is then the pair of trajectories $(\mathbf{X}(t), \mathbf{E}[t])$ for $t \in [0, T]$, representing the evolution of the global ontic and epistemic states generated by the switched system in Definition 3.

## 3.3 Computational Runs of Distributed Multi-Robot Systems

We now describe the robot runs looking only at local epistemic computations. We use the fact that the global and local times associated to a time path correspond precisely to the clock of the environment and of the robots, respectively, in Definitions 4 and 5.

**Definition 8 (Execution).** Let $\mathbf{r} \in \Pi$ be a robot, with an epistemic evolution specified by Definition 4. Let a pair $\langle \mathbf{e}_\mathbf{r}, \mathbf{y}_\mathbf{r} \rangle$ be a **robot configuration**. We say that an **execution** of $\mathbf{r}$ is a sequence $\{\langle \mathbf{e}_\mathbf{r}[t]_\mathbf{r}, \mathbf{y}_\mathbf{r}[t]_\mathbf{r} \rangle\}$ indexed by its local time $[t]_\mathbf{r} \in \mathcal{N}$, where $\mathbf{e}_\mathbf{r}[t]_\mathbf{r} \in S_\mathbf{r}$, $\mathbf{y}_\mathbf{r}[t]_\mathbf{r} \in S_\mathbf{y}$, and $\phi_\mathbf{r}(\mathbf{e}_\mathbf{r}[t]_\mathbf{r}, \mathbf{y}_\mathbf{r}[t]_\mathbf{r}) = \mathbf{e}_\mathbf{r}[t+1]_\mathbf{r}$.

The robot execution can now be extended to a computational system run, its robot system analog. For this, we define first the global robot configurations, which will take the role of possible worlds in the epistemic frame, later described in Section 4.
**► Definition 9 (Global robot configuration).** A global robot configuration is a tuple $C = \langle \{e_r\}_{r \in \Pi}, \{y_r\}_{r \in \Pi}, [t] \rangle$ consisting of all local robot configurations at a global computation time $[t]$. $C_r$ is the restriction of a global configuration $C$ to the robot $r$.

**► Definition 10 (System run).** A system run $\sigma$ from time 0 to $T$, determined by time path $p$, is a sequence of global robot configurations $\{C[t]\}_{[t] \in [0, T]}$, where, for any $t \in [0, T]$:

- there exists a subset $\emptyset \neq P_p(t) \subseteq \Pi$ of participating robots, activated by the time path $p$ at global time $t$.

- we have

$$C_r[t+1] = \begin{cases} \varphi_r(C[t]_r) & \text{if } r \in P_p(t) \\ C[t]_r & \text{if } r \notin P_p(t) \end{cases}$$

We denote the set of all possible runs $\mathcal{I}$, representing all the possible evolutions of the system solely based on the robot's behavior. An execution correspond to the individual epistemic evolution of a single robot, while a run represent the epistemic evolution of all the robots. Note that this definition of run abstracts away the ontic (physical) updates in similar fashion to how the robot state machine represents solely the robots' computations. We effectively focus on the epistemic states, while the ontic evolution related constraints and interactions are encompassed by the environment.

## 3.4 Correspondence of the Dynamical and Computational Perspectives

We establish now the conditions on which the computational model of a multi-robot system from Section 2.2 is a faithful abstraction of the switched hybrid dynamical system of Section 2.1. We show that the computational content of the system runs are the same in both dynamic (Section 3.2) and computational (Section 3.3) models. This justifies using the runs from computational models as the basis for the epistemic frames (Section 4), as they capture all of the information available in the robots' decision process.

We rely on a system abstraction procedure that converts a hybrid multi-robot system $\mathcal{H}$ into a computational system $C$. We now define this abstraction and specify under which assumptions it preserves the computational information.

**► Definition 11 (System abstraction).** Given a hybrid system $\mathcal{H}$, a system abstraction $\Phi$ is a tuple of surjective functions $\Phi = (\Phi_E, \Phi_Y, \Phi_U, \Phi_X)$ that map the global state spaces as follows.

- $\Phi_E: \mathcal{E} \to S_e$, partitions the global epistemic state space into a finite set of discrete memory states;

- $\Phi_Y: \mathcal{Y} \to S_Y$, maps the global observations into a finite set of discrete observations, as per Remark 2;

- $\Phi_U: \mathcal{U} \to S_U$, maps the global control commands to a finite set of global actions;

- $\Phi_X: \mathcal{X} \to S_\mathcal{E}$, partitions the global ontic state space into a finite set of environment states.

**► Lemma 12 (Induced run abstraction).** A system abstraction $\Phi: \mathcal{H} \to C$ induces a function $\Phi^*: \Sigma_\mathcal{H} \to \Sigma_C$ that maps hybrid runs to computational runs.

**Proof.** The function $\Phi^*$ is constructed by applying the system abstraction to every trajectory $(X(t), E[t]) \in \Sigma_\mathcal{H}$ at every discrete time step $[t] \in [0, T]$. ▼
The induced system abstraction need not be surjective, as some computational runs may
not be physically possible. For instance, the computational model of a robot may allow for a
state transition where its position updates faster than its speed limit. We filter those cases
as follows.

**Assumption 13 (Physical realizability).** Let $\mathcal{H}$ be a hybrid system with protocol defined by its epistemic evolution $\Phi$ and control function CTL. Let $C$ be its computational abstraction. We assume that every run in $\Sigma_C$ has a physical counterpart, i.e., $\Sigma_C \subseteq \Phi^*(\Sigma_{\mathcal{H}})$.

**Theorem 14 (Computational trace equivalence).** Let $\Sigma_{\mathcal{H}}$ be the set of all runs of a computational system $\mathcal{H}$, and $\Sigma_C$ the set of all runs of a hybrid system $C$. If $C$ is a faithful abstraction of a hybrid system $\mathcal{H}$, then $\Phi^*(\Sigma_{\mathcal{H}}) = \Sigma_C$.

**Proof.** We proceed by showing the mutual inclusion $\Phi^*(\Sigma_{\mathcal{H}}) \subseteq \Sigma_C$ and $\Sigma_C \subseteq \Phi^*(\Sigma_{\mathcal{H}})$.

$\Phi^*(\Sigma_{\mathcal{H}}) \subseteq \Sigma_C$. This follows from Lemma 12, as the codomain of the induced system abstraction $\Phi^*$ is $\Sigma_C$.

$\Sigma_C \subseteq \Phi^*(\Sigma_{\mathcal{H}})$. This holds directly from assumption 13.

<figure><img src="image_4.png" /></figure>

This equivalence relies on assumption 13, as we expect for the computation abstraction to be faithful to the physical dynamics. Theorem 14 formalizes the consequence of this assumption.

4 Robot Tasks and Temporal Epistemic Logic

The remaining of this paper focuses on the computations of the distributed multi-robot
systems described in Section 3, i.e., on their epistemic states and on their transitions. The
epistemic evolution of robotic systems is described using epistemic frames that are built
from the system runs of Definition 10:

**Definition 15 (Epistemic Frame).** Given a set of robots $\Pi$ and the set of all possible runs $\Sigma$, an epistemic frame $\mathcal{F} = \{\mathcal{C}\}_{\mathcal{C} \in \Sigma}$, $\{\sim_r\}_{r \in \Pi}$ is composed of a set of global robot configurations $\{\mathcal{C}\}_{\mathcal{C} \in \Sigma}$ (Definition 9) and a collection of indistinguishability relations $\{\sim_r\}_{r \in \Pi}$, where:

- Each global robot configuration, or point, is constituted by a pair $(\sigma, [t])$ of system run $\sigma$ (Definition 10) and the corresponding global timestamp $[t]$ (Definition 6), which is relative to the run $\sigma \in \Sigma$;

- the collection of indistinguishability relations $\sim_r$ indexed by robot $r \in \Pi$ are computed based on the equivalence of the local state: $(\sigma, [t]) \sim_r (\sigma', [t'])$ iff $e_r^C = e_{r'}^{C'}$ where $\sigma[t] = C$, i.e., if the epistemic state $e_r$ of $r$ in two different global robot configurations is the same.

The structure of the epistemic frame, and in particular its indistinguishability relations, depends on the assumptions of the robot model. For instance, if one considers that robots may not complete their `MOVE` steps (non-rigid model), uncertainty regarding their current locations will be added; visibility influences how much information can be gained (and discerned) during a `LOOK` step; asynchronicity allows indistinguishability to range among points with the exact same global state but different global time, and so on.

The epistemic frames, generated from the system runs of Definition 10, are used to reason about the knowledge of the multi-robot system throughout the robot tasks. Fittingly, we consider only the epistemic states of the system, as the ontic (physical) states are abstracted away in the transitions between computation steps.

In robot tasks, we assume that robots are able to sense a portion of the environment in which they are embedded, represented as a topological space. We call the "observable"
portion of the environment the observable space, which we assume to be a compact topological space, denoted by $(X, \tau)$. In particular, it is a compact normalized Euclidean space, i.e. $X \subseteq [0, 1]^n$ with the standard Euclidean metric. To every open set $U$ of $\tau$ we associate a unique proposition $\text{sp}(U)$. $\text{sp}(X)$ is associated to the whole observation space $X$ and $\text{sp}(\emptyset)$ to the empty space $\emptyset$. We refer to $P_X$ as the set of space statements. Space statements satisfy some important properties: $V \supseteq U$ implies that $\text{sp}(V) \to \text{sp}(U)$. Thus, $(P_X, \to)$ is a poset, induced by the containment of open sets. Furthermore, since $(X, \tau)$ is closed under union $(P_X, \to)$ is a join-lattice, allowing us to express, for example, information in a compact way: robot a need only communicate to another robot b, the largest region that contains all others, i.e., a single atom.

We say that a robot $\mathbf{r}$ knows a formula $\psi$ at $(\sigma, [t])$ iff such a formula holds at all points that are indistinguishable from $(\sigma, [t])$ to $\mathbf{r}$. In particular, because indistinguishability between points is defined on equivalence of robots' local states, the S5 epistemic logic<fnref n="1" /> is the natural candidate. This notion of knowledge can be extended to groups, such as distributed knowledge ($\mathcal{D}_A\varphi$) via the equivalence relation $\sim_{\mathcal{D}_A}:= \bigcap_{\mathbf{r} \in A} \sim_{\mathbf{r}}$ consisting of the intersection of indistinguishabilities and representing the “collective knowledge” spread across all robots in $A$.

An epistemic model $\mathcal{M}$ is a tuple of an epistemic frame $\mathcal{F}$ and an evaluation function $\pi: P_X \to 2^{\mathcal{C}}_{c \in \Sigma}$ that assigns a truth value to atoms at each point of the model, where $\mathcal{C}$ is a global robot configuration, and $P_X$ is the collection of space statements The function $\pi$ simply maps a proposition $\text{sp}(U)$ corresponding to a region $U$, to all the global configurations where $U$ holds. In line with the runs and systems framework, we call our epistemic model interpreted system, denoted by $\mathcal{I}$.

Note that, even though our logic is *factive*, known facts about the real world are not necessarily true in the real world. As knowledge of robots depends on the robots *observation*, factivity can only hold with respect to that observation. Consider as an example the formula $(\sigma, [t]) = K_{\mathbf{r}}\text{position}(\mathbf{r}, x, y)$ denoting that robot $\mathbf{r}$'s position at the time $t$ is at the point $(x, y)$ and lets assume that this was actually true in the actual world at the time robot observed its surrounding. This does not imply that it is *still true* at any time $t' \neq t$ where $[t'] = [t]$. In fact our knowledge operator is only S5 with respect to the epistemic observations, but not with respect to the *real world*. Common knowledge experiences similar frictions, where attainability depends on the model and timing assumptions [16, 22], yet our modeling unveils the crucial dependency on *observations*. This is in line with the fact that we consider only the epistemic states of the system, abstracting away the ontic (physical) states in the transitions between computation steps.

## 4.1 A Temporal Epistemic Logic of Space

The following grammar defines temporal epistemic logic formulas:

► **Definition 16 (Language $\mathcal{L}_{\text{space}}$).** The language is defined by the following grammar:

$$ \varphi ::= \text{sp}(U) \mid \neg\varphi \mid (\varphi \land \varphi) \mid K_{\mathbf{r}}\varphi \mid D_{A}\varphi \mid \Diamond\varphi $$

where $U \in P_X$, $\mathbf{r} \in \Pi$, and $A \subseteq \Pi$.

<footnote n="1">¹ In an S5 modal logic, the knowledge operator satisfies factivity ($K_a\psi \to \psi$), positive introspection ($K_a\psi \to K_a K_a\psi$) and negative introspection ($\neg K_a\psi \to K_a \neg K_a\psi$).</footnote>
**12 Knowledge in multi-robot systems**

In this grammar, sp(U) is a space statement, $K_r\varphi$ represents "r knows $\varphi$", $D_A\varphi$ stands for "group A has distributed knowledge of $\varphi$", and $\diamond\varphi$ reads "eventually $\varphi$".

**Definition 17 (Semantics of $\mathcal{L}_{space}$).** Let $\mathcal{I}$ be a set of runs (Definition 15), with its respective set of configuration-time pairs $\mathcal{W}$, an evaluation function $\pi: P_X \to 2^\mathcal{W}$, a run $\sigma \in \mathcal{I}$, and a robot $\mathbf{r} \in \Pi$:

- $\mathcal{I}, (\sigma, [t]) \models sp(U) \text{ iff } sp(U) \in \pi(\sigma, [t])(sp(U))$

- $\mathcal{I}, (\sigma, [t]) \models \neg\varphi \text{ iff } \mathcal{I}, (\sigma, [t]) \not\models \varphi$

- $\mathcal{I}, (\sigma, [t]) \models (\varphi \wedge \psi) \text{ iff } \mathcal{I}, (\sigma, [t]) \models \varphi \text{ and } \mathcal{I}, (\sigma, [t]) \models \psi$

- $\mathcal{I}, (\sigma, [t]) \models K_r\varphi \text{ iff } \mathcal{I}, (\sigma', [t}') \models \varphi \text{ for all } (\sigma', [t}') \in \mathcal{W} \text{ s.t. } (\sigma, [t]) \sim_r (\sigma', [t'])$

- $\mathcal{I}, (\sigma, [t]) \models D_A\varphi \text{ iff } \mathcal{I}, (\sigma', [t}') \models \varphi \text{ for all } (\sigma', [t}') \in \mathcal{W} \text{ s.t. } (\sigma, [t]) \underset{D_A}{\sim} (\sigma', [t'])$

- $\mathcal{I}, (\sigma, [t]) \models \diamond\varphi \text{ iff } \mathcal{I}, (\sigma, [t}') \models \varphi \text{ for some } [t]' \ge [t]$.

We further set $\Box\varphi := \neg\Diamond\neg\varphi$ and $\varphi \vee \psi := \neg(\neg\varphi \wedge \neg\psi)$. We also define mutual knowledge $E_{\Pi}\varphi$ as the conjunction of the knowledge of robots in $\Pi$: $E_{\Pi}\varphi := \bigwedge_{\mathbf{r} \in \Pi} K_r\varphi$.

A formula $\varphi$ is valid in $\mathcal{I}$ if, for all $(\sigma, [t]) \in \mathcal{W}$, $\mathcal{I}, (\sigma, [t]) \models \varphi$. If $\varphi$ is valid in $\mathcal{I}$, we use the notation $\mathcal{I} \models \varphi$.

**4.2 Application to Exploration**

In this section we analyze the robot exploration task for a LCM model using the framework introduced in the previous section. Spatial atoms now denote that a certain region is *explored*, i.e., some robot has observed it, without changing the semantics.

**Definition 18 (Simple robot exploration).** We say that a system is consistent with a simple exploration system if, for any $\mathbf{r} \in \Pi$, and any region $U$, it satisfies:

- **Exploration agency:** $\mathcal{I} \models sp(U) \to D_{\Pi}sp(U)$, i.e., if a region $U$ has been explored, it has been explored by at least one robot

- **Exploration independence:** $\mathcal{I} \models D_A sp(U) \to \bigwedge_{\mathbf{r} \in A} K_r sp(V_r)$ s. t. $\bigcup_{\mathbf{r} \in A} V_r = U$, i.e., any space atom known distributively by robots in $A$, is given by the union of the space atoms known by robots in $A$

- **Stable space statements:** $\mathcal{I} \models \bigwedge_{sp(U) \in \mathcal{L}_{exp}^{-}} sp(U) \to \Box sp(U)$, i.e., once a region has been explored, it is forever explored.

- **Stable exploration knowledge (perfect recall):** $\mathcal{I} \models K_r sp(U) \to \Box K_r sp(U)$, i.e., once a space atom is known by a robot, it will be known forever by that robot.

In the exploration task, if a robot knows that a certain region of space sp(U) has been explored, denoted by $K_r sp(U)$, it implies that all subsets of that region are also known by that robot, i.e., $K_r sp(V)$ with $V \subseteq U$ and $V$ open. This follows directly from the compactness of the exploration space.

**Definition 19 (Termination conditions).** Given an interpreted system $\mathcal{I}$ consistent with simple robot exploration (Definition 18), with a set of robots $\Pi$, exploration space $X$, and its respective space statements $P_X$, we say that $\mathcal{I}$ is consistent with:

- **Parallel termination:** iff $\mathcal{I} \models \Diamond D_{\Pi} sp(X)$, i.e., no single robot needs to know that the whole space is explored;
■ **Selfish termination:** iff $\mathcal{I} \models \diamond E_{\Pi}\text{sp}(X)$, i.e., each robot needs to know that the whole space is explored;

■ **Cooperative termination:** iff $\mathcal{I} \models \diamond E_{\Pi} \diamond E_{\Pi} \text{sp}(X)$, i.e., each robot needs to know that the whole space is explored and that other robots know that the whole space is explored.

Parallel termination can be characterized in terms of a very weak condition, called exploration liveness:

**Definition 20 (Exploration liveness).** A run $\sigma$ satisfies exploration liveness iff there exists a collection of open sets, $\mathcal{U}$, such that $\bigcup_{U \in \mathcal{U}} U = X$, and for any $U \in \mathcal{U}$, $\mathcal{I}, \sigma \models \diamond \text{sp}(U)$. A model satisfies exploration liveness iff all of its runs satisfy exploration liveness.

In other words, exploration liveness says that any point $x \in X$ of the exploration space $X$ will eventually be explored.

**Theorem 21 (Exploration Liveness Necessity).** Exploration liveness is necessary for simple exploration.

*Proof.* Note by contraposition that if there is a run $\sigma$, such that no open cover $\mathcal{U}$ of eventually explored regions exists. Naturally, we may consider $\mathcal{U}' = \{U \mid \mathcal{I}, \sigma \models \diamond \text{sp}(U)\}$. Since $\mathcal{U}'$ is not an open cover of $X$, then $\bigcup_{U \in \mathcal{U}'} U \neq X$. Therefore, there is a point $x \in X$, $x \notin \bigcup_{U \in \mathcal{U}'} U$. Thus, by definition of $\mathcal{U}'$, $x$ is never explored, and consequently $X$ is not explored in $\sigma$. ◀

**Theorem 22 (Exploration Liveness Sufficiency).** Let $\mathcal{I}$ be a model with a compact exploration space $X$. If $\mathcal{I}$ satisfies exploration liveness, then $\mathcal{I} \models \diamond \text{sp}(X)$.

*Proof.* Consider an arbitrary run $\sigma$ of $\mathcal{I}$, from Definition 20, there is an open cover $\mathcal{U}$ such that for any $U \in \mathcal{U}$, $\mathcal{I}, \sigma \models \diamond \text{sp}(U)$. Since $X$ is compact and $\mathcal{U}$ is an open cover of $X$ then there exists a finite subcover $\mathcal{U}' = \{V_1, \dots, V_k\} \subseteq \mathcal{U}$, such that $\bigcup_{i=1}^k V_i = X$. Also, since $\mathcal{I}, \sigma \models \diamond \text{sp}(V_i)$, then for any $i \in [1, k]$, then for each $V_i$ there is a time $[t_i]$ such that $\mathcal{I}, \sigma, [t_i] \models \text{sp}(V_i)$. Simply consider $[t_{\text{max}}] = \max\{[t_i]\}$. Since space statements are stable facts, then $\mathcal{I}, \sigma, [t_{\text{max}}] \models \bigwedge_{i=1}^k \text{sp}(V_i)$. Therefore $\mathcal{I}, \sigma, [t_{\text{max}}] \models \text{sp}(X)$. Thus $\mathcal{I}, \sigma \models \diamond \text{sp}(X)$. Since $\sigma$ is an arbitrary run of $\mathcal{I}$, then it follows that $\mathcal{I} \models \diamond \text{sp}(X)$. ◀

Theorem 21, Theorem 22, and exploration agency from Definition 18 imply that whenever $X$ is compact exploration liveness is necessary and sufficient for parallel termination<fnref n="2" />.

**Definition 23 (Exploration flooding).** We say that the communication of a robot system is exploration flooding iff at each phase of the LCM cycle, each robot tries to communicate the largest region of space it knows to be explored to the rest of the robots.

**Lemma 24.** Consider a model $\mathcal{I}$ with an exploration space $X$, from a $\mathcal{LUMI}$ robot system with full visibility and exploration flooding, and $\text{sp}(U)$ an space statement, an arbitrary run $\sigma$ from $\mathcal{I}$, and an arbitrary robot $\mathbf{r} \in \Pi$. If $\mathcal{I}, \sigma \models \diamond K_{\mathbf{r}}\text{sp}(U)$, then $\mathcal{I}, \sigma \models \diamond E_{\Pi}\text{sp}(U)$.

*Proof.* Since $\mathcal{I}, \sigma \models \diamond K_{\mathbf{r}}\text{sp}(U)$, then there exists a time $[t_0]$ such that $\mathcal{I}, \sigma, [t_0] \models K_{\mathbf{r}}\text{sp}(U)$. Since robots have perfect recall, and space statements are stable, $\mathcal{I}, \sigma, [t] \models K_{\mathbf{r}}\text{sp}(U)$ for any $[t] \ge [t_0]$.

Let $\mathbf{r}' \in \Pi$ be an arbitrary robot. Since we don't consider crash failures, there is a time $[t]_{\mathbf{r}'} \ge [t_0]$ when $\mathbf{r}'$ is able to read the lights of robot $\mathbf{r}$. Let $U'$ be the maximal region that

<footnote n="2">² Note that this is not necessarily true in non-compact spaces.</footnote>
$\mathbf{r}$ knows to be explored at time $[t]_{\mathbf{r}'}$. Since the robot system is exploration flooding, then robot $\mathbf{r}$ is communicating $sp(U')$ through its lights. Therefore, robot $\mathbf{r}'$ learns $sp(U')$, i.e. $K_{\mathbf{r}'}\text{sp}(U')$. However, recall that $U \subseteq U'$. Thus $\mathcal{I}, \sigma, [t]_{\mathbf{r}'} \models K_{\mathbf{r}'}\text{sp}(U)$.

Since $\Pi$ is finite, then there is a $[t_{\max}]$ such that $\mathcal{I}, \sigma, [t_{\max}] K_{\mathbf{r}''}\text{sp}(U)$ for any robot $\mathbf{r}'' \in \Pi$.
Finally, $\mathcal{I}, \sigma \models \Diamond E_{\Pi}\text{sp}(U)$. ◀

**Theorem 25.** Consider an interpreted system $\mathcal{I}$ with a compact exploration space $X$ such that $\mathcal{I}$ satisfies the exploration liveness condition, and such that the robot system is exploration flooding. Then $\mathcal{I}$ satisfies the cooperative termination property from Definition 19, namely, $\mathcal{I} \models \Diamond E_{\Pi} \Diamond E_{\Pi} \text{sp}(X)$

**Proof.** Since $X$ is compact and satisfies exploration liveness, then by Theorem 21, then $\mathcal{I} \models \Diamond \text{sp}(X)$. By exploration agency, then $\mathcal{I} \models \Diamond D_{\Pi}\text{sp}(X)$. Let $\sigma$ be a fixed run of $\mathcal{I}$, then there exists a time $[t_0]$ such that $\mathcal{I}, (\sigma, [t_0]) \models D_{\Pi}\text{sp}(X)$. Consider for each robot $\mathbf{r} \in \Pi$, a region $U_{\mathbf{r}} := \bigcup \{U \subseteq X \mid \mathcal{I}, \sigma, [t_0] \models K_{\mathbf{r}}\text{sp}(U)\}$. Note that $K_{\mathbf{r}}\text{sp}(U_{\mathbf{r}})$, and $U_{\mathbf{r}}$ is the maximal region that robot $\mathbf{r}$ knows to be explored. From exploration independence (Definition 18), it follows that $\bigcup_{i=1}^k U_i = X$.

From Lemma 24, it holds that $\mathcal{I}, \sigma \models \Diamond E_{\Pi} U_{\mathbf{r}}$. Therefore, $\mathcal{I}, \sigma \models \Diamond E_{\Pi} \bigcup_{i=1}^n U_i$. This shows that $\mathcal{I}, \sigma \models \Diamond E_{\Pi} \text{sp}(X)$.

Let $[t_1]$ be such that $\mathcal{I}, \sigma, [t_1] \models E_{\Pi}\text{sp}(X)$. In particular consider an arbitrary robot $\mathbf{r}' \in \Pi$. Since $\mathcal{I}, \sigma, [t_1] \models K_{\mathbf{r}}\text{sp}(X)$, then by definition of knowledge, in any other run $\sigma'$ and any other time $[t']$ that is indistinguishable from $\sigma$ at time $[t_1]$ to $\mathbf{r}'$, $\text{sp}(X)$ holds. From Lemma 24, it follows that $\mathcal{I}, \sigma', [t'] \models \Diamond E_{\Pi}\text{sp}(X)$. Thus, from the definition of the knowledge modality, $\mathcal{I}, \sigma, [t_1] \models K_{\mathbf{r}'} \Diamond E_{\Pi}\text{sp}(X)$. Since $\mathbf{r}'$ is arbitrary, then $\mathcal{I}, \sigma, [t_1] \models E_{\Pi} \Diamond E_{\Pi}\text{sp}(X)$. Therefore $\mathcal{I}, \sigma \models \Diamond E_{\Pi} \Diamond E_{\Pi}\text{sp}(X)$. Therefore, $\mathcal{I} \models \Diamond E_{\Pi} \Diamond E_{\Pi}\text{sp}(X)$. ◀

**Corollary 26.** All termination conditions are equivalent for a *LUMI* robot system with exploration flooding, and exploration fairness.

**Proof.** Note that Cooperative Termination $\Rightarrow$ Selfish termination $\Rightarrow$ Parallel Termination. Finally note that Theorem 25 shows that Parallel Termination $\Rightarrow$ Cooperative Termination, which completes the equivalence cycle. ◀

Our result can be extended to cover arbitrary communication, nevertheless, a communication liveness condition would still be necessary.

**Definition 27 (Communication liveness).** We say that a model $\mathcal{I}$ with an exploration space $X$ satisfies the communication liveness condition if for any run $\sigma$ of $\mathcal{I}$, any time $[t]$, any robot $\mathbf{r}$, and any space statement $p_u$, $\mathcal{I}, (\sigma, [t]) \models K_{\mathbf{r}}\text{sp}(U) \Rightarrow \mathcal{I}, \sigma \models \Diamond E_{\Pi}\text{sp}(U)$.

**Theorem 28.** Consider a model $\mathcal{I}$ with a compact exploration space $X$ such that $\mathcal{I}$ satisfies the exploration liveness and communication liveness conditions, and such that the robot system is exploration flooding. Then $\mathcal{I}$ satisfies the cooperative termination property from Definition 19, namely, $\mathcal{I} \models \Diamond E_{\Pi} \Diamond E_{\Pi} \text{sp}(X)$

**Proof.** Note that we can reuse the proof of Theorem 25, but using Definition 27 instead of Lemma 24. ◀

## 4.3 Application to Approximate Gathering

In the approximate gathering task, robots need to ensure that their position and all other robots' positions' are eventually contained in a specific open set, called the rendezvous region.
For this epistemic modeling we need to extend the language of Definition 16 with additional atoms:

- **Positional atoms** $pos_r(x) \in P_{g(X)} \subseteq X$ (i.e., a finite subset of the domain of the observation function $g$ in Definition 1) with $|P_{g(X)}| \in \mathbb{N}$;

- **Initial position atoms** $init(pos_r(x)) \in P_{g(X)}$, meaning the starting position of robot $r$;

- **Inclusion atoms** $(x \in U) \in P_{\tau}$ representing the inclusion of points in open sets in the exploration space $\in_{x,U}$;

We define the set of Rendezvous region $P_{rz(X)} \in 2^X$, which are a finite set of regions of space such that $\forall U, V \in P_{rz(X)} : U \cap V = \emptyset$ and $|P_{rz(X)}| \in \mathbb{N}$. $\vec{x} \in P_{\tau}^X$ denotes a vector with a position for each robot. The following grammar defines temporal epistemic logic formulas for approximate gathering.

**► Definition 29 (Language $\mathcal{L}_{gather}$).** The gathering language is defined by the following grammar:

$$ \varphi ::= p \mid \neg \varphi \mid (\varphi \land \varphi) \mid K_r \varphi \mid D_A \varphi \mid \diamond \varphi $$

where $p \in P_{\tau} \cup P_{g(X)}$, $r \in \Pi$, and $A \subseteq \Pi$. When obvious from the context, we will omit the subscript $X$.

The semantics of $\mathcal{L}_{gather}$ is analogous to the one of $\mathcal{L}_{exp}$ in Definition 17, except for the newly introduced atoms:

- $\mathcal{I}, (\sigma, [t]) \models pos_r(x)$ iff $pos_r(x) \in \pi(\sigma, [t])(pos_r(x))$

- $\mathcal{I}, (\sigma, [t]) \models init(pos_r(x))$ iff $pos_r(x) \in \pi(\sigma, 0)(pos_r(x))$

- $\mathcal{I}, (\sigma, [t]) \models (x \in U)$ iff $(x \in U) \in \pi(\sigma, [t])(x \in U)$

Positional atoms $pos_r(x)$ mean that robot $r$ is at actual position $x$ discretized to $x$. As $g$ is surjective, it is possible that $g_r(x) = g_r(x')$ even though $x \neq x'$, meaning two different actual robot positions result in the same position for that robot. We assume that robots know their own position: $pos_r(x) \leftrightarrow K_r pos_r(x)$.

The approximate gathering is solved if all robots' positions are contained in the same rendezvous region forever, assuming each robot starts in one rendezvous region. To do so, they need to agree on one rendezvous region and move here. They are allowed to change the rendezvous region finitely often, but eventually need to stick to one forever. We require it to be impossible for any robot to intersect two rendezvous regions at the same time, i.e., $pos_r(x) \land (x \in U) \implies (\bigwedge_{U \neq V \in P_{rz(X)}} \neg (x \in V))$.

**► Definition 30 (Approximate gathering).** System $\mathcal{I}$ is consistent with approximate gathering iff the following two conditions hold:

- **Eventual Gathering:** There is a rendezvous region where all robots eventually meet forever

$$ \mathcal{I} \models \bigvee_{U \in P_{rz(X)}} \bigwedge_{r \in \Pi} \diamond \Box \bigvee_{x \in P_{g(X)}} pos_r(x) \land (x \in U) $$

- **Starting Validity:** If all robots are already contained in a rendezvous region initially, that is also the final rendezvous region

$$ \mathcal{I} \models \bigwedge_{U \in P_{rz(X)}, \vec{x} \in P_{g(X)}^{\Pi}} \left( \left( \bigwedge_{r \in \Pi} \text{init}(pos_r(x_r)) \right) \land (x_r \in U) \right) \rightarrow (\diamond \Box \bigvee_{\vec{y} \in P_{g(X)}^{\Pi}} (\bigwedge_{r \in \Pi} pos_r(y_r)) \land (y_r \in U)). $$
These conditions strongly resemble the stabilizing agreement conditions, epistemically characterized in [8]. It is defined by the following formulas, where $\mathcal{V}$ is the set of values to choose from, the atom $choose_a(v)$ denotes that agent $a$ chooses value $v$. $decide_a(v)$ is defined as $\square choose_a(v)$, where $a, b$ are agents, i.e., robots with no dynamical constraints:

► **Definition 31** (Stabilizing agreement [8]). System $\mathcal{I}$ is consistent with stabilizing agreement if (Agreement) and (Validity) hold.

■ **Agreement:** There is a value such that every agent decides on that value

$$ \mathcal{I} \models \bigvee_{v \in \mathcal{V}} \bigwedge_{a \in \Pi} \diamond \mathit{decide}_a(v) $$

■ **Validity:** An agent can only choose a known initial value of some agent

$$ \mathcal{I} \models \bigwedge_{v \in \mathcal{V}} (choose_a(v) \rightarrow K_a \bigvee_{b \in \Pi} init_b(v)) $$

Observe that covering a rendezvous region can be seen as that robot choosing that region. Rendezvous regions are the objects the robots choose from. As each robot initially sits in exactly one region, that region can be seen as the problem input. The last obstacle is reducing the strong validity, as its called in the distributed computing literature (see for example [9]), to the weak validity of approximate gathering.

► **Theorem 32.** Consider a model $\mathcal{I}$ with a space $X$, together with the language defined *Definition 29*, an arbitrary run $\sigma$ from $\mathcal{I}$. If $\mathcal{I}$ is consistent with stabilizing agreement, then it is also consistent with approximate gathering.

Consider setting the set of possible choices $\mathcal{V}$ to be the set of possible rendezvous regions $P_{rz(X)}$, setting $choose_r(U) \leftrightarrow \bigvee_{x \in P_{g(X)}} pos_r(x) \wedge (x \in U)$ and $decide_r(U) = \square choose_r(U)$, and setting $init_r(U) \leftrightarrow \bigvee_{x \in P_{g(X)}} init(pos_r(x)) \wedge (x \in U)$.

**Proof.** We start by substituting for $choose$ and $init$ as defined in Definition 31. For (Agreement) we immediately arrive at (Eventual Gathering):

$$ \mathcal{I} \models \bigvee_{U \in P_{rz(X)}} \bigwedge_{\mathbf{r} \in \Pi} \diamond \Box \bigvee_{x \in P_{g(X)}} pos_{\mathbf{r}}(x) \wedge (x \in U). \qquad (11) $$

For (Starting Validity) we need to provide more reasoning, consider the following, where we already prepended the validity with a conjunction over all robots:

$$ \mathcal{I} \models \bigwedge_{\substack{\mathbf{r} \in \Pi, \\ U \in P_{rz(X)}}} \left( \left( \bigvee_{x \in P_{g(X)}} pos_{\mathbf{r}}(x) \wedge (x \in U) \right) \rightarrow \left( K_{\mathbf{r}} \bigvee_{\mathbf{r}' \in \Pi} \bigvee_{x \in P_{g(X)}} init(pos_{\mathbf{r}'}(x)) \wedge (x \in U) \right) \right). \qquad (12) $$

As we need to prove an implication, we assume its antecedent and derive the consequent. Assuming

$$ \bigwedge_{\mathbf{r} \in \Pi} init(pos_{\mathbf{r}}(x_{\mathbf{r}})) \wedge (x_{\mathbf{r}} \in U), \qquad (13) $$
we want to derive

$$ (\diamond \Box \bigvee_{\vec{y} \in \mathbb{P}_{g(X)}^{\Pi}} (\bigwedge_{\mathbf{r} \in \Pi} \mathrm{pos}_{\mathbf{r}}(y_{\mathbf{r}})) \wedge (y_{\mathbf{r}} \in U)), \qquad (14) $$

for any $U \in \mathbb{P}_{rz(X)}$ and any $\vec{x} \in \mathbb{P}_{g(X)}^{\Pi}$. Choose any $U, \vec{x}$ which satisfies Equation (13), meaning a starting position vector that intersects over $U$. Note that there is only one such $U$ as initial rendezvous regions are unique.

Observe that, as robots know their own initial positions, Equation (13) implies the antecedent in Equation (12) for all robots $\mathbf{r}$:

$$ \begin{align} \mathrm{init}(\mathrm{pos}_{\mathbf{r}}(x_{\mathbf{r}})) \wedge (x_{\mathbf{r}} \in U) &\implies \nonumber \\ K_{\mathbf{r}} \mathrm{init}(\mathrm{pos}_{\mathbf{r}}(x_{\mathbf{r}})) \wedge (x_{\mathbf{r}} \in U) &\implies \nonumber \\ K_{\mathbf{r}} \bigvee_{\mathbf{r}' \in \Pi} \mathrm{init}(\mathrm{pos}_{\mathbf{r}'}(x_{\mathbf{r}'})) \wedge (x_{\mathbf{r}'} \in U) &\implies \nonumber \\ (K_{\mathbf{r}} \bigvee_{\mathbf{r}' \in \Pi} \bigvee_{y \in \mathbb{P}_{g(X)}} \mathrm{init}(\mathrm{pos}_{\mathbf{r}'}(y_{\mathbf{r}'})) \wedge (y_{\mathbf{r}'} \in U)). \tag{15} \end{align} $$

Therefore the consequent in Equation (12) is true for only one choice of $U$ (the same that satisfies Equation (13)) and false for all other $V \in \mathbb{P}_{rz(X)}$.

By Equation (11) there exists some $V, t$ such that

$$ \mathcal{I}, (\sigma, t) \models \bigvee_{x \in \mathbb{P}_{g(X)}} \mathrm{pos}_{\mathbf{r}}(x) \wedge (x \in V) \qquad (16) $$

holds for all $t' > t$ and for all robots $r$. We see that Equation (16) is precisely the antecedent of Equation (12), and, as Equation (12) is a validity, it is satisfied by the fixed choice for $V, t$. Since the consequent in Equation (12) is true only for $U$ as derived in Equation (15) (but Equation (12) is a validity), Equation (16) has to be false for any $W \neq U$. But by the previous reasoning we know that Equation (16) is true for at least one $V$ for all $t' > t$, implying that $U = V$ for all $t' > t$. We can now derive Equation (14) from Equation (16):

$$ \begin{align} \bigvee_{x \in \mathbb{P}_{g(X)}} \mathrm{pos}_{\mathbf{r}}(x) \wedge (x \in U) \nonumber \\ \bigvee_{\vec{y} \in \mathbb{P}_{g(X)}^{\Pi}} (\bigwedge_{\mathbf{r} \in \Pi} \mathrm{pos}_{\mathbf{r}}(\vec{y}_{\mathbf{r}})) \wedge (x \in \vec{y}_{\mathbf{r}}) \nonumber \\ (\diamond \Box \bigvee_{\vec{y} \in \mathbb{P}_{g(X)}^{\Pi}} (\bigwedge_{\mathbf{r} \in \Pi} \mathrm{pos}_{\mathbf{r}}(\vec{y}_{\mathbf{r}})) \wedge (x \in \vec{y}_{\mathbf{r}})), \tag{17} \end{align} $$

meaning the robots gather at the initially intersected rendezvous region forever.

<figure><img src="image_5.png" /></figure>

## 4.4 Application to Surveillance

In the surveillance task, we consider that an external agent might invade the robots space at a given time frame. If such an intruder happens to invade the space, then the robots should be able to detect it. In the following, we will show that the surveillance task can be formulated as a variant of the exploration task.

We will consider a normalized time frame for detection, represented by the closed interval $[0, 1] \subset \mathbb{R}$. As with exploration, we consider a compact space $X$, which we will call our surveillance space. Note that the product space of our surveillance space with the normalized
time frame, $X \times [0, 1]$ is a compact topological space with the product topology, which we will call the surveillance cylinder.

Note that each region observed by the robots in the surveillance also induces a region in the surveillance cylinder by simply taking the time of the observations into account. For instance, if a robot explores a region $U$ of the surveillance space at a time $t$, then it already has explored $U \times t$ within the surveillance cylinder. Furthermore, if the intruder's speed is known to be bounded by a factor of $f$, then the exploration of $U$ at time $t_1$, implies that that at the next time $t_2$ at which the robot is active, $(U \setminus B_{f,t}(\partial U))$, $t)_{t \in [t_1, t_2]}$ is also seen, where $B_{f,t}(\partial U)$ is the ball of radius $f \cdot t$ around the boundary of $U$. This comes from the fact that if the intruder was not observed inside $U$ at time $t_1$, then the farthest that the intruder can reach at a time $t \in [t_1, t_2]$ is given by the ball of radius $f \cdot t$ around the boundary of $U$.

For the surveillance task, we will consider a set of propositional atoms consisting of space statements of the surveillance cylinder $X \times [0, 1]$, namely $P_{X \times [0, 1]}$. Each of these space statements represent that a part of the surveillance cylinder was explored and no intruder was found. In addition to $P_{X \times [0, 1]}$, we also consider two additional propositional atoms, FOUND, and SECURE. Thus, we can define a set of propositional atoms for surveillance, denoted by $P_{\text{Surv}(X)} := P_{X \times [0, 1]} \cup \{\text{FOUND}, \text{SECURE}\}$. Furthermore, we consider an epistemic temporal language for surveillance in the same way as we did for exploration, but with $P_{\text{Surv}(X)}$ instead of $P_X$.

**Definition 33 (Language $\mathcal{L}_{\text{surv}}$).** The surveillance language is defined by the following grammar:

$$ \varphi ::= p \mid \neg \varphi \mid (\varphi \land \varphi) \mid K_r \varphi \mid D_A \varphi \mid \diamond \varphi $$
where $p \in P_{\text{Surv}(X)}$, $r \in \Pi$, and $A \subseteq \Pi$.

The semantics of $\mathcal{L}_{\text{surv}}$ is analogous to the one of $\mathcal{L}_{\text{space}}$ in Definition 17. Note that the surveillance space is considered to be secure iff there does not exist a path $\xi: [0, 1] \to X$ such that the trace of $\xi$. $\text{tr}(\xi) := \{(\xi(t), t) | t \in [0, 1]\}$ is not explored. A naive approach to secure the surveillance cylinder would be to consider the exploration on $X \times [0, 1]$. However this is largely impractical, and often unfeasible, as it is equivalent to observing the space $X$ at all times during the time interval $[0, 1]$. Instead, it is sufficient to explore a “cut” or section of the surveillance cylinder. For instance, if the surveillance space $X$ was explored completely at a fixed time time, i.e., if the set $X \times \{t\}$ from the surveillance cylinder is explored, then the path of any intruder would intersect $X \times \{t\}$. More generally, if there is a manifold in the surveillance cylinder that has been observed, and can be expressed as the trace of a continuous function $f: X \to [0, 1]$; $\text{tr}(f) := \{(x, f(x)) | x \in X\}$.

**Lemma 34 (Curve catching lemma).** Let $\alpha: [0, 1] \to X$ be an arbitrary curve in $X$, and $f: X \to [0, 1]$ a continuous function. Then, the trace of $\alpha$, $\text{tr}(\alpha) := \{(\alpha(t), t) | t \in [0, 1]\}$ and the trace of $f$, $\text{tr}(f) := \{(x, f(x)) | x \in X\}$ intersect.

**Proof of Lemma 34.** Simply note that $f \circ \alpha: [0, 1] \to [0, 1]$ is a continuous function on $[0, 1]$. Thus by the Brouwer's fixed-point theorem, there must exist a $t_0$ such that $f \circ \alpha(t_0) = t_0$. Let $\alpha(t_0) = y$. Thus $(y, t_0) \in \text{tr}(\alpha)$ and by definition $(\alpha(t_0), f(\alpha(t_0))) \in \text{tr}(f)$. Therefore $(y, t_0) \in \text{tr}(\alpha) \cap \text{tr}(f)$. $\quad \blacksquare$

Intuitively, this lemma shows that continuous manifolds on $X$ work as a “catching net” that is able to capture the path of any invader. Therefore, in addition to the conditions required for simple exploration (Definition 18), we also consider the following conditions:
**► Definition 35 (Found and secure conditions).**

*Detection Agency* Consider an arbitrary run $\sigma$ in a robot system, and an intruder path $\alpha: [0, 1] \to X$. We say that FOUND holds at a time $t$ iff either there exists a robot $p_i$ whose observation region at time $t$ intersects $\alpha$, or there is a time $t' < t$ such that FOUND holds at time $t'$.

*Observation Correctness* Consider an arbitrary run $\sigma$, and an intruder path $\alpha: [0, 1] \to X$. Let $U$ be a region of the surveillance cylinder $X \times [0, 1]$ such that $U \cap \text{tr}(\alpha) \neq \emptyset$. Then $\neg \text{sp}(U)$.

*Securement* Let $f: X \to [0, 1]$ be any continuous function. Let $U$ be a region of the surveillance cylinder $X \times [0, 1]$, if $\text{tr}(f) \subseteq U$, then $\text{sp}(U) \to \text{SECURE}$.

*Completion condition* $\mathcal{I} \models (\text{SECURE} \implies \Box \neg \text{FOUND}) \wedge (\text{FOUND} \implies \Box \neg \text{SECURE})$.

Detection agency means that the FOUND atom only holds if an intruder has already been detected by a robot. Observation correctness means that a region in the surveillance cylinder is not secure if an intruder is moving through a space-time point in the region, i.e., exploration regions in this context refer only to regions where no intruder has been found. Securement captures the idea from Lemma 34 that shows that it is sufficient to explore the trace of a continuous manifold in $X$. Completion condition states that if part of the surveillance cylinder was explored then the intruder was not found (and never will), and if the intruder was found then the surveillance cylinder was not secure (and never will be). Also note that if the trace of the manifold has even a single discontinuity point, then this may be enough for an intruder to evade detection.

We provide the following definition for the surveillance robot task (without termination):

**► Definition 36 (Surveillance).** Consider a robot system and a model $\mathcal{I}$ consistent with Definition 18 with respect to its surveillance cylinder, that satisfies Definition 35. Let $\sigma$ be a run of $\mathcal{I}$. We say that the model solves the surveillance task if $\mathcal{I}, \sigma \models \diamond \text{FOUND} \vee \diamond \text{SECURE}$.

Note that by Completion condition (Definition 35) SECURE and FOUND atoms are mutually exclusive in a run.

As with the simple exploration task, we can consider multiple termination conditions for the surveillance task.

**► Definition 37 (Termination for surveillance).**

*Parallel Termination* $\mathcal{I}, \sigma \models \diamond D_{\Pi} \text{FOUND} \vee \diamond D_{\Pi} \text{SECURE}$

*Selfish Termination* $\mathcal{I}, \sigma \models \diamond E_{\Pi} \text{FOUND} \vee \diamond E_{\Pi} \text{SECURE}$

*Cooperative Termination* $\mathcal{I}, \sigma \models \diamond E_{\Pi} \diamond E_{\Pi} \text{FOUND} \vee \diamond E_{\Pi} \diamond E_{\Pi} \text{SECURE}$

Since Lemma 34 shows that exploring a continuous manifold of the surveillance cylinder is enough to detect an intruder, it is also enough to fully secure the space, thus we can replace the exploration liveness condition to a manifold instance.

**► Definition 38 (Manifold liveness).** We say that run $\sigma$ of a robot system has the manifold liveness condition iff there exists a continuous function $f_{\sigma}: X \to [0, 1]$ such that $\sigma$ satisfies the exploration liveness condition for $\text{tr}(f_{\sigma})$.

**► Theorem 39 (Manifold liveness sufficiency).** Consider a robot system that satisfies the simple exploration conditions, Definition 18, for the surveillance cylinder $X \times [0, 1]$, the surveillance conditions, Definition 35, and the manifold surveillance liveness condition, Definition 38. Then the surveillance task is solved at $\sigma$.

**Proof of Theorem 39.** Follows from Lemma 34, and Theorem 22.

<figure><img src="image_6.png" /></figure>
**► Theorem 40.** Consider a model $\mathcal{I}$ with a compact surveillance space $X$ that satisfies the communication liveness, the manifold liveness condition, the simple exploration conditions for the surveillance cone $X \times [0, 1]$, the surveillance conditions, and the exploration flooding with respect to the surveillance cylinder. Then $\mathcal{I}$ satisfies the cooperative termination property.

**Proof of Theorem 40.** Let $\sigma$ be a run of $\mathcal{I}$, from Theorem 39, $\mathcal{I}, \sigma = \diamond \text{FOUND} \lor \diamond \text{SECURE}$. Recall that by Completion condition (Definition 35) SECURE and FOUND are mutually exclusive in a run. First, let us assume that $\mathcal{I}, \sigma = \diamond \text{FOUND}$. From Definition 35, there must exist a robot $\mathbf{r}_i$ such that finds an intruder at a time $t_i$. Since $\mathbf{r}_i$ detects the intruder, it holds that $\mathcal{I}, \sigma, t_i = K_{\mathbf{r}_i} \text{FOUND}$. From Definition 27, it holds that $\mathcal{I} \sigma = \diamond E_{\Pi} \text{FOUND}$. In particular, in all runs $\sigma'$ that are indistinguishable to $\mathbf{r}_i$, $\mathcal{I}, \sigma' = \diamond E_{\Pi} \text{FOUND}$. Therefore, $\mathcal{I}, \sigma, t_i = K_{\mathbf{r}_i} \diamond E_{\Pi} \text{FOUND}$. Since $\mathcal{I}, \sigma = \diamond E_{\Pi} \text{FOUND}$, then we can repeat the previous argument for any other robot. Therefore $\mathcal{I}, \sigma = \diamond E_{\Pi} \diamond E_{\Pi} \text{FOUND}$.

Now, assume that $\mathcal{I}, \sigma = \diamond \text{SECURE}$ holds. Then, it follows that no intruder was found. From Definition 38, it holds that there exists a continuous manifold $f_\sigma: X \to [0, 1]$, such that $\mathcal{I}, \sigma = \diamond p_{\text{tr}(f_\sigma)}$. Note that the conditions for Theorem 28 hold, therefore, $\mathcal{I}, \sigma = \diamond E_{\Pi} \diamond E_{\Pi} p_{\text{tr}(f_\sigma)}$. From the securement condition from Definition 35, it follows that $\mathcal{I}, \sigma = \diamond E_{\Pi} \diamond E_{\Pi} \text{SECURE}$. ◀

**► Corollary 41.** In particular for the LUMI model with full visibility, if the robot system satisfies the manifold liveness, then it solves the surveillance task with cooperative termination

## 5 Conclusions and future work

In this paper, we developed a framework that seamlessly integrates control theory, distributed systems and temporal epistemic logic in the context of multi-robot systems, with applications to exploration, gathering and surveillance tasks. We present, at the same time, new complementary perspectives for modeling distributed robot systems as dynamical systems and as state machines. The novel separation of a robot state into ontic and epistemic parts is exploited by developing a common understanding of scheduler that ties their local executions to a global time. We extend this first bridge between control theory and distributed computing by also providing access to the epistemic reasoning present in distributed computing, now adapted for multi-robot tasks and their particularities, namely the fact that robots exist in some (physical) space. This reasoning arena takes the form of an epistemic model capable of expressing the knowledge of the system at their computation operations. A temporal epistemic logic of space is employed and its usefulness made evident with applications to concrete exploration and gathering tasks, for both of which sufficient epistemic conditions are derived.

This work has multiple implications and holds the promise of future developments in exchanging tools and results across fields. One of the most striking implications is that the classical luminous robot model [10] with full visibility is very strong in a distributed computing sense, as confirmed by the existence of a whole research field on establishing and maintaining communication in multi robot systems. Some, such as [6, 7] have leveraged epistemic planning and action models in order to keep a live communication. As we have identified a sufficient condition for approximate gathering, we can directly judge the correctness of an action model, and therefore the correctness of a protocol, by its ability to reach a given specification in epistemic terms.

The results of this paper have already been extended for the task of surveillance, as can be found in Section 4.4, where a group of robots must monitor a region of space to be
absent of intruders. Other interesting extensions include (but are not limited to) considering
other robot tasks and their similarities to distributed tasks, as well as extending the logic
framework with deontic modalities expressing robots' permissions and obligations during
protocol execution given their current local knowledge. Furthermore, our framework is
capable of integrating the geometrical interpretation [21] of epistemic frames and the recent
advances [34] on sheaf theoretic and homological aspects of task solvability, however this is
out of scope for this paper, and could be the focal interest of follow-up work.

References

1. Manuel Alcántara, Armando Castañeda, David Flores-Peñaloza, and Sergio Rajsbaum. The topology of look-compute-move robot wait-free algorithms with hard termination. *Distrib. Comput.*, 32(3):235-255, 2019. doi:10.1007/s00446-018-0345-3.

2 Jean-Pierre Aubin and Arrigo Cellina. *Differential Inclusions, Set-Valued Maps And Viability Theory*. Number 264 in Grundl. der Math. Wiss. Springer, 1984.

3 Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. In Mohamed Faouzi Atig and Alexander A. Schwarzmann, editors, *Networked Systems*, pages 93–109. Springer International Publishing, 2019. doi:10.1007/978-3-030-31277-0_7.

4 Alberto Bemporad, Maurice Heemels, and Mikael Johansson, editors. *Networked Control Systems*, volume 406 of *Lecture Notes in Control and Information Sciences*. Springer, 2010. doi:10.1007/978-0-85729-033-5.

5 Béatrice Bérard, Pascal Lafourcade, Laure Millet, Maria Potop-Butucaru, Yann Thierry-Mieg, and Sébastien Tixeuil. Formal verification of mobile robot protocols. *Distrib. Comput.*, 29(6):459–487, 2016. doi:10.1007/s00446-016-0271-1.

6 Lauren Bramblett and Nicola Bezzo. Epistemic planning for heterogeneous robotic systems. In *2023 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)*, pages 691–698, 2023. doi:10.1109/IROS55552.2023.10341352.

7 Lauren Bramblett, Shijie Gao, and Nicola Bezzo. Epistemic prediction and planning with implicit coordination for multi-robot teams in communication restricted environments. In *2023 IEEE International Conference on Robotics and Automation (ICRA)*, pages 5744–5750, 2023. doi:10.1109/ICRA48891.2023.10161553.

8 Giorgio Cignarale, Stephan Felber, and Hugo Rincon Galeana. A sufficient epistemic condition for solving stabilizing agreement, 2024. URL: https://arxiv.org/abs/2403.01025, arXiv: 2403.01025.

9. Pierre Civit, Seth Gilbert, Rachid Guerraoui, Jovan Komatovic, and Manuel Vidigueira. On the validity of consensus. In *Proceedings of the 2023 ACM Symposium on Principles of Distributed Computing*, PODC '23, page 332-343, New York, NY, USA, 2023. Association for Computing Machinery. doi:10.1145/3583668.3594567.

10 Shantanu Das, Paola Flocchini, Giuseppe Prencipe, Nicola Santoro, and Masafumi Yamashita. Autonomous mobile robots with lights. *Theoretical Computer Science*, 609:171-184, 2016. doi:10.1016/j.tcs.2015.09.018.

11 Mattia D'Emidio, Gabriele Di Stefano, Daniele Frigioni, and Alfredo Navarra. Characterizing the computational power of mobile robots on graphs and implications for the Euclidean plane. *Information and Computation*, 263:57-74, 2018. doi:10.1016/j.ic.2018.09.010.

12 Gabriele Di Stefano and Alfredo Navarra. Optimal gathering of oblivious robots in anonymous graphs and its application on trees and rings. *Distributed Computing*, 30(2):75–86, 2017. Cited by: 37. doi:10.1007/s00446-016-0278-7.

13 Ha Thi Thu Doan, Françoise Bonnet, and Kazuhiro Ogata. Model Checking of a Mobile Robots Perpetual Exploration Algorithm. In Shaoying Liu, Zhenhua Duan, Cong Tian, and Fumiko Nagoya, editors, *Structured Object-Oriented Formal Language and Method*, volume 10189, pages 201–219. Springer International Publishing, 2017. doi:10.1007/978-3-319-57708-1_12.
14 Ha Thi Thu Doan, François Bonnet, and Kazuhiro Ogata. Model Checking of Robot Gathering. LIPIcs, Volume 95, OPODIS 2017, 95:12:1–12:16, 2018. doi:10.4230/LIPICS.OPODIS.2017.12.

15 Francesco Fabiano, Biplav Srivastava, Marianna Bergamaschi Ganapini, Jonathan Lenchner, Lior Horesh, and Francesca Rossi. E-PDDL: A Standardized Way of Defining Epistemic Planning Problems.

16 R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. *Common Knowledge Revisited*, pages 87–104. Springer Netherlands, Dordrecht, 2003. doi:10.1007/978-94-007-1001-6_5.

17 Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. *Reasoning About Knowledge*. MIT Press, 1995. doi:10.7551/mitpress/5803.001.0001.

18 Paola Flocchini, Giuseppe Prencipe, and Nicola Santoro, editors. *Distributed Computing by Mobile Entities: Current Research in Moving and Computing*, volume 11340 of *Lecture Notes in Computer Science*. Springer International Publishing, 2019. doi:10.1007/978-3-030-11072-7.

19 Krisztina Fruzsa, Roman Kuznets, and Ulrich Schmid. Fire! In Joseph Y. Halpern and Andrés Perea, editors, *Proceedings Eighteenth Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2021, Beijing, China, June 25-27, 2021*, volume 335 of *EPTCS*, pages 139–153, 2021. doi:10.4204/EPTCS.335.13.

20 Guy Goren and Yoram Moses. Silence. *J. ACM*, 67(1), jan 2020. doi:10.1145/3377883.

21 Éric Goubault, Roman Kniazev, Jérémy Ledent, and Sergio Rajsbaum. Semi-simplicial set models for distributed knowledge. In *38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023*, pages 1–13, 2023. doi:10.1109/LICS56636.2023.10175737.

22 Joseph Y. Halpern and Yoram Moses. Knowledge and common knowledge in a distributed environment. *J. ACM*, 37(3):549–587, jul 1990. doi:10.1145/79147.79161.

23 Jaakko Hintikka. *Knowledge and Belief: An Introduction to the Logic of the Two Notions*. Cornell University Press, 1962.

24 Luc Jaulin. *Mobile Robotics*. ISTE Ltd / John Wiley and Sons Inc, 2nd edition edition, 2019.

25 H.K. Khalil. *Nonlinear Control*. Pearson Education, 2014. URL: https://books.google.fr/books?id=OyGvAgAAQBAJ.

26 David Kirkpatrick, Irina Kostitsyna, Alfredo Navarra, Giuseppe Prencipe, and Nicola Santoro. On the power of bounded asynchrony: Convergence by autonomous robots with limited visibility. *Distrib. Comput.*, 37(3):279–308, 2024. doi:10.1007/s00446-024-00463-7.

27 Sophia Knight. *The Epistemic View of Concurrency Theory*. (Le point de vue épistémique de théorie de la concurrence). PhD thesis, École Polytechnique, Palaiseau, France, 2013. URL: https://tel.archives-ouvertes.fr/tel-00940413.

28 Jeremy Ledent, Sergio Rajsbaum, and Jorge Armenta-Segura. Two-agent approximate agreement from an epistemic logic perspective. In *Thirteenth Latin American Workshop on New Methods of Reasoning 2020, LANMR 2020*, December 2020. Thirteenth Latin American Workshop on New Methods of Reasoning 2020, LANMR 2020 ; Conference date: 10-12-2020 Through 11-12-2020.

29 Daniel Liberzon. *Switching in Systems and Control*. Systems and Control: Foundations and Applications. Birkhauser, 2003.

30 Nancy A. Lynch. *Distributed Algorithms*. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1996.

31 Yoram Moses. Relating knowledge and coordinated action: The knowledge of preconditions principle. In *Proceedings of the 15th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2015*, volume 215, pages 231–245, June 2016. Publisher Copyright: © Yoram Moses.; 15th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2015 ; Conference date: 04-06-2015 Through 06-06-2015. doi:10.4204/EPTCS.215.17.

32 André Platzer. *Logical Analysis of Hybrid Systems Book - Proving Theorems for Complex Dynamics*. Springer Berlin, Heidelberg, 2010. doi:10.1007/978-3-642-14509-4.
33 Romain Postoyan, Paolo Frasca, Elena Panteley, and Luca Zaccarian, editors. *Hybrid and Networked Dynamical Systems: Modeling, Analysis and Control*, volume 493 of Lecture Notes in Control and Information Sciences. Springer Nature Switzerland, 2024. doi:10.1007/978-3-031-49555-7.

34 Hans Riess and Robert Ghrist. Diffusion of Information on Networked Lattices by Gossip. In *2022 IEEE 61st Conference on Decision and Control (CDC)*, pages 5946–5952, 2022. doi:10.1109/CDC51059.2022.9992539.

35 Bruno Siciliano, Lorenzo Sciavicco, Luigi Villani, and Giuseppe Oriolo. *Robotics: Modelling, Planning and Control*. Springer Publishing Company, Incorporated, 1st edition, 2008.

36 Ichiro Suzuki and Masafumi Yamashita. Distributed Anonymous Mobile Robots: Formation of Geometric Patterns. *SIAM Journal on Computing*, 28(4):1347–1363, 1999. doi:10.1137/S009753979628292X.

37 Satoshi Terai, Koichi Wada, and Yoshiaki Katayama. Gathering problems for autonomous mobile robots with lights. *Theoretical Computer Science*, 941:241–261, 2023. doi:10.1016/j.tcs.2022.11.018.

## A Taxonomy of look-compute-move

There are several possible choices regarding the capacities of robots. The following Table 1 summarizes the most relevant variations for robots under the LOOK-COMPUTE-MOVE abstraction. They are chosen in order to make a model mode or less powerful, with additional assumptions on their communication, observation and movement capacities.
<table><caption>Table 1 Partial glossary of LCMterminology.</caption><thead><tr><th>Property</th><th>Variant</th><th>Description</th></tr></thead><tbody><tr><td>Memory</td><td><strong>Oblivious</strong><br><strong>Luminous</strong></td><td>No memory, all information is lost between rounds<br>Lights can be used to preserve information across rounds</td></tr><tr><td>Communication</td><td><strong>Silent</strong><br><strong>Luminous</strong></td><td>No communication between robots<br>Information passed indirectly by retrieving lights during LOOK</td></tr><tr><td>Visibility</td><td><strong>Myopic</strong><br><strong>Unlimited visibility</strong></td><td>LOOKretrieves a partial snapshot parametrized by view distance<br>LOOKretrieves a snapshot of the entire environment</td></tr><tr><td>Identity</td><td><strong>Anonymous</strong><br><strong>Indistinguishable</strong></td><td>No unique identifier<br>No external identifier</td></tr><tr><td>Movement</td><td><strong>Rigid</strong><br><strong>Non-rigid</strong></td><td>MOVEis always executed fully<br>MOVEcan be interrupted, parametrized by a minimum distance</td></tr><tr><td>Dynamics</td><td><strong>Holonomic</strong><br><strong>Non-holonomic</strong></td><td>MOVEcan be any arbitrary destination<br>MOVEhas to respect dynamic constraints, e.g. Dumbins' car</td></tr><tr><td>Orientation</td><td><strong>Oriented</strong><br><strong>Disoriented</strong><br><strong>Chiral</strong></td><td>There is a global coordinate system that all can access<br>Only different local coordinate systems<br>Different local coordinate systems, but with common north</td></tr><tr><td>Synchronicity</td><td><strong>ASYNC</strong><br><strong>k-ASYNC</strong><br><strong>SSYNC</strong><br><strong>FSYNC</strong></td><td>Scheduler, no shared notion of time<br>Scheduler, the robots are at most k rounds apart<br>Scheduler, a subset of the robots activated at each round<br>Scheduler, all robots are activated at each round</td></tr></tbody></table>