Logic for Timed Agent Network Topologies
Clovis Eberhart1,2 , James Haydon1 , Jérémy Dubut1,2 , Ahmet Cetinkaya1 , and Sasinee Pruekprasert1

Abstract— We define µTGL, a spatio-temporal logic with
fixed points and first-order agent quantification whose expressive power allows the definition of topological properties of
networks of communicating agents. The existence of temporal
operators and fixed points requires particular care whendefining its semantics. We also give a streaming monitoringalgorithm for µTGL formulas. Finally, we demonstrate thelogic’s usefulness on an example, where we monitor a complex
property that ensures resilient consensus.

I. INTRODUCTION
With more multi-agent systems being used in practice, theneed to study topological properties of automated multi-agent
networks has come to light. The key challenge in studying multi-agent networks arises from complex interactions
among the agents, especially when many agents are involved.
Efficiently describing desired properties for such systems isa non-trivial task that requires mathematical formalism.
Temporal logics, which can express system properties
dependent on time, have been proved useful for monitoring
specifications. In particular, Linear Temporal Logic (LTL)and Signal Temporal Logic (STL) have been extensively used
to monitor cyber-physical systems [1]. However, those logics
are not meant to model spatial relations between agents,
which are crucial to monitoring some interesting properties.
For instance, the distances between the different agents caninfluence the overall behaviour of the network.
Several previous studies proposed extensions of wellknown temporal logics to model spatio-temporal behavioursof multi-agent systems. Signal Spatio-Temporal Logic(SSTL) [2], [3] extends STL with spatial modalities, andimposes bounds on spatial and temporal operators. SpatialTemporal Logic (SpaTeL) [4] extends STL with spatial
component based on Tree Spatial Superposition Logic [5],resulting in a logic suitable for robotic swarm control [6].
Counting linear temporal logic (cLTL) [7] can specify desired behaviours for multi-robot systems with constraints on
the number of agents satisfying given LTL properties. To
specify topological properties of networks, we also need afixed-point operator (such as that from the µ-calculus [8]),which none of these logics have.
The authors are supported by ERATO HASUO Metamathematics for
Systems Design Project (No. JPMJER1603), JST. J. D. is also supported by
Grant-in-aid No. 19K20215, JSPS. A. C. is also supported by Grant-in-aid
No. 20K14771, JSPS. S. P. is also supported by Grant-in-aid No. 21K14191,
JSPS.
1 The authors are with the National Institute of Informatics, Hitotsubashi
2-1-2, Tokyo 101-8430, Japan {eberhart, jhaydon, dubut,
cetinkaya, sasinee}@nii.ac.jp.
2 C. E. and J. D. are also affiliated with the Japanese-French Laboratory
for Informatics, IRL 3527.

This paper proposes a new logic µTGL (Temporal Graph
Logic with fixed points). It has several features needed toexpress interesting properties of communicating agent networks. It has temporal operators, as well as a “connectivity”
operator that has a strong spatial flavour. It also contains firstorder agent quantification, which is necessary to express theproperties of agent networks with an unknown number of
agents. Finally, our logic contains fixed points, which allows
the definition of recursive properties that cannot be expressedby spatio-temporal logics proposed in the previous studies.
Using these constructs, we can express properties such as
the connectivity of the communication graph of the networkor the existence of communication chains between agents.
The presence of fixed points and temporal operators in the
logic implies that we may need to look at an infinite portionof the agents’ trajectories to be able to decide whether aproperty is satisfied or not. This leads us to come up witha novel semantics that takes into account how much of thesignal we are allowed to see. This semantics allows us todefine a streaming monitoring algorithm for µTGL.
Our logic draws inspiration from many other logics. The
temporal part is inherited from continuous-time temporal
logics such as Metric Temporal Logic (MTL) [9], MetricInterval Temporal Logic (MITL) [10], and STL [11]. The
diamond modality is inspired by spatial operators fromspatio-temporal logics [2], [3]. The fixed point operator isinspired from fixed-point logics, and in particular the µcalculus [8]. Since µTGL features a diamond modality corresponding to connectivity of agents, our logic is also related
to temporal graph logics [12]. However, such logics describe
graph rewriting properties rather than agent networks, so they
are quite different in practice. Moreover, our semantics uses
three-valued logic [13], more precisely, Kleene’s logic ofindeterminacy. It enables us to handle indeterminacy in themonitoring algorithm that we propose.
The rest of the paper is structured as follows. In Section II,
we define the syntax and semantics of µTGL, give examplesof especially useful formulas, and describe a monitoringalgorithm for it. In Section III, we give several examplesof formulas that showcase the expressivity of µTGL. In
Section IV, we give a monitoring algorithm for µTGL
formulas. In Section V, we design a µTGL formula that
describes a property that ensures resilient consensus in an
agent network, and apply our monitoring algorithm on a
specific scenario of mobile robots surveilling a perimeter.
Notations: We denote by N the set of natural numbers,by R, R≥0 , R, R≥0 the sets of real numbers, non-negative real
numbers, and their extensions with ±∞ and +∞ respectively.
We denote by 2 the set {⊺, } of booleans. We denote by

3 the set of booleans augmented with an indeterminate ⊺,and equipped with the order  < ⊺ < ⊺. It is equippedwith the usual functions on 2: ∨ and ∧ are respectively min
and max, and negation maps ⊺ to ⊺
. Uncertain sets arefunctions X → 3. They are equipped with the same orderand operations as 3, defined pointwise. We sometimes use
set notation {x ∈ X ∣ φ(x)} to denote an uncertain set, bywhich we mean that no element is mapped to ⊺
.

space

d
h

Fig. 1.

In this section, we define µTGL, its syntax and semantics, give examples of its uses, and describe a monitoringalgorithm for it.
We denote by A the set of agents, which we assume finite.
Agents move in a metric space (M, d) – usually Rn equippedwith the Euclidean distance.

Known and possible trajectories of agentsFree and bound variables are defined as usual. A formula
is closed if all X ∈ X in φ are bound.
Definition 2 (Truth formulas). Truth formulas are given by
the following grammar:Φ ∶∶= ⊺ ∣ φ ≤ φ ∣ ¬Φ ∣ Φ ∧ Φ ∣ FT Φ ∣ ∃a. Φ,

A. Syntax
We start by defining the syntax of µTGL, that is the setof µTGL formulas. From now on, we assume given sets
X of fixed-point variables and A of agent variables, bothinfinite countable. We also fix a set P of predicates on M ,i.e. functions from M to 2.
Definition 1 (Agent formulas). Agent formulas are given by
the following grammar:φ ∶∶= ⊺ ∣ p ∣ ¬φ ∣ φ ∧ φ ∣(propositional logic)◊D φ ∣ FT φ ∣(spatio-temporal logic)a ∣ ∃a. φbtime

II. µTGLX ∣ µX. φ ∣ Hh φ ∣a(fixed points)(quantification),where a ∈ A is an agent variable, p ∈ P is a predicate, T
and D are intervals of R≥0 , h ∈ R≥0 is a non-negative real,and X ∈ X is a fixed-point variable. We impose the usual
condition that, for µX. φ to be well-formed, all occurrencesof X must be positive in φ (i.e., they occur under an evennumber of negations).
Intuitively, agent formulas hold for some agents, or equivalently represent a set of agents (those agents for which theformula holds). This intuition is made precise in Definition 6.
The propositional logic constructs are self-explanatory. The
FT φ construct is the temporal eventually modality: it holds
for agent a if there is a point in time t ∈ T when φ holds for a.
The ◊D φ construct is the diamond modality, an equivalent
to eventually for agent connectivity: it holds for a if thereis b “connected” to it (i.e., within a certain distance fromit) for which φ holds. The µX. φ construct is the least fixed
point construct. The only unusual construct is the horizon
construct HT , whose use we will explain in Section II-B.
We use the usual syntactic sugar for propositional logic
, φ ∨ ψ, φ → ψ, as well as GT φ ≡ ¬FT ¬φ and ◻D φ ≡¬ ◊D ¬φ for spatio-temporal operators, ∀a. φ ≡ ¬∃a. ¬φ foruniversal quantification, and νX. φ ≡ ¬µX. ¬φ[X → ¬X]
for greatest fixed point. We also use F φ and G φ when thetime interval is [0, +∞).

where φ and ψ are closed agent formulas in φ ≤ ψ, and therest is as in Definition 1.
Truth formulas use the same constructs as agent formulas
except fixed points and diamond, and also allows for comparison of agent formulas through φ ≤ ψ.
We also introduce some syntactic sugar for equality on
agent formulas: φ = ψ ≡ (φ ≤ ψ)∧(ψ ≤ φ), a ≠ b ≡ ¬(a = b).
Example 3 (Connectedness of communication graph). We
consider a network of communicating agents where agentscan communicate up to some distance d. The communicationgraph Gt at time t of such a network is a graph whose nodes
are agents, and there is an edge between a and b if they arewithin communication range at time t. The following formulaexpresses connectivity of the communication graphs between
agents at all times:G ∀a. (⊺ ≤ µX. (a ∨ ◊[0,d] X)).
The subformula µX. (a ∨ ◊[0,d] X) represents the set of
agents that can be reached in the communication graph fromthe agent represented by a. Therefore, the whole formulaexpresses the fact that, at all times, all agents are reachable
from any other agent, so the communication graph is connected. Another way to state the same property is as follows:Φcon = G ∀a, b. a ≤ µX. (b ∨ ◊[0,d] X).
We will show later in Example 8 that this formula indeed
has its intended meaning.
B. Semantics
In this section, we give a semantics to agent and truth
formulas. In general, a semantics takes a formula and a model(in our case, a signal of all agent positions at all times), andreturns a boolean: whether the formula is true or false in thismodel. In our case, however, we need to be slightly more
subtle: because of the presence of fixed points and temporal
operators, we may need to look arbitrarily far into the future
to prove or disprove a formula. Let us show an example.

Example 4 (Communcation chain). Let us consider the samesetting as in Example 3, but with agents re-broadcasting
messages sent by other agents for duration t. The following
formula expresses the existence, at all times and for all pairs(a, b) of agents, of a communication chain from a to b, thatis a list of agents that can communicate within time t totransmit a message from a to b:
Φch = G ∀a, b. a ≤ µX. (b ∨ F[0,t] ◊[0,d] X).

(1)

However, deciding whether Φch holds may require knowing
an arbitrarily long part of the signal (even if we restrict toG[0,T ] ). Let us assume that the whole network consists of
two agents a and b that move on a line, as in Fig. 1. If welook at the signal up to time h, we can neither prove nor
disprove the existence of a communication chain from a tob: if a follows the red trajectory in the future, there will be
no such chain, but there will be one if it follows the blue one(namely a → a → . . . → a → b).
There are two problems with this. First, we may needinfinite time before being able to compute the semantics,
which is not feasible in practice. Second, and more importantly, we may want to express properties such as “there
exists a communication chain from a to b such that they
can communicate within time t”, which cannot be expressedwith the current examples.
As a first step towards fixing this, we use a three-valued
logic, rather than a boolean one. The semantics of a formula
can thus also be indeterminate (⊺), meaning that we do nothave enough information to determine its actual value.
This single change does not however solve the problem.
Indeed, in the case we describe in Example 4, the semanticsof Φch would be ⊺ unless we look at the whole time interval.
We therefore introduce the horizon construct, whose purpose
is to “give up” on trying to prove that a formula holds: if
the semantics of φ is undetermined and “enough time has
passed”, then we “stop searching” and say it is false.
Example 5 (Bounded-time communication). Building on
Example 4, we express the fact that all agents can communicate with one another within time t. This property canbe expressed byG ∀a, b. a ≤ Ht µX. (b ∨ F[0,t] ◊[0,d] X).

(2)

This is the same formula as (1), with an added horizon
construct Ht . The intuitive meaning of this construct is that
it forbids chains that are longer than t.
The semantics of a formula is relative to a model. Ourmodels here are signals. Given a set A of agents, a signal isa function σ∶ (A × R≥0 ) → M , which represents the fact thatagents evolve through time in space M .
The final piece of structure we need before we can define
the semantics, is contexts. A context is a partial function thatmaps X to functions (R≥0 × R) → A → 3 and A to A.
Definition 6 (Semantics). The semantics JφKρ (σ, t, h) of anagent formula φ on signal σ, at time t ∈ R≥0 , with horizonh ∈ R, and in context ρ is an uncertain set of agents definedinductively as in Fig. 2. The semantics JΦKρ (σ, t, h) ∈ 3 oftruth formulas is also given in Fig. 2.
The existence of fixed points is ensured by the fact thatvariables appear positively in fixed-point formulas. When
writing JφKρ (σ, t, h), we assume that ρ is defined on all
free variables of φ. All of the definitions are rather standard,
except for a few points that we describe here.
The first unusual point is the presence of the horizon
variable h, which represents how much into the future weare allowed to see. This variable is untouched by mostconstructs. However, when constructs make use of positions(such as ◊D φ), if the horizon h is negative (i.e., we do notknow the value of the signal at that point in time), then thesemantics uses ⊺. When constructs do not use positions (suchas a), then it does not matter whether the horizon is negative
or not. Moreover, the semantics of FT φ shifts the horizon
variable to reflect the fact that we evaluate the semantics ofφ at a different point in time.
Secondly, the semantics of the diamond modality is rather
long, but J◊D φKρ (σ, t, h)(a) is ⊺ if h ≥ 0 and there
is an agent b whose distance from a at time t is in D
and JφKρ (σ, t, h)(b) is ⊺, which corresponds to the usual
semantics of ◊D . It is  in two cases: first, if h ≥ 0 and for
all agents b, either their distance to a at time t is not in D
or JφKρ (σ, t, h)(b) is ; second, if h < 0 and for all agentsb, JφKρ (σ, t, h)(b) is . In the first case, we have access topositions and can refute the formula if the distance between
agents is not in D. In the second one, do not have accessto positions, and must therefore refute φ for all agents to be
sure that ◊D φ is . It is ⊺ otherwise: either h < 0 and there
is an agent b such that JφKρ (σ, t, h)(b) is not , or h ≥ 0
and there is an agent b whose distance to a at time t is in.
D and such that JφKρ (σ, t, h)(b) is ⊺Remark 7 (Diamond modality, space, and connectivity).
In this paper, the diamond modality has a spatial flavour,
since we chose its interpretation to be about the distance
between agents. In this sense, our logic is close to spatiotemporal logics. However, from a theoretical point of view,the diamond modality is an agent modality, rather thana spatial one, and we could similarly define a semantics
on a graph, rather than on trajectories (µTGL stands for
Temporal Graph Logic with Fixed Points). We stick to thisinterpretation of the diamond modality in this paper because
it is general enough to express the properties we are interested in.

Finally, the only non-standard construct is Ht φ. Intuitively, it asks whether φ is true by looking only at horizon h′ .
To do so, it computes the semantics of φ with (the potentiallyshorter) horizon min(h, h′ ) and returns it. However, whenh ≥ h′ , we have a long enough horizon to give a boolean
answer, and therefore ⊺ is changed to  (we were unable toprove the property with horizon h′ ). This helps give formulasa boolean value in finite time, since it gets rid of ⊺
 values
when enough time has passed.
Example 8 (Semantics of Φcon ). For any formula φ where X

J⊺Kρ (σ, t, h) = ⊺JpKρ (σ, t, h)(a) = {p(σ(a, t))⊺

if h ≥ 0otherwise

JFT φKρ (σ, t, h) = ⋁ JφKρ (σ, t + t′ , h − t′ )Jφ ∧ ψKρ (σ, t, h) = JφKρ (σ, t, h) ∧ JψKρ (σ, t, h)
J◊D φKρ (σ, t, h)(a) = {
b∈A

t′ ∈T

⋁b∈A (JφKρ (σ, t, h)(b) ∧ d(σ(a, t), σ(b, t) ∈ D)(⋁b∈A JφKρ (σ, t, h)(b)) ∧ ⊺J∃a. φKρ (σ, t, h) = ⋁ JφKρ[a→b] (σ, t, h)

JXKρ (σ, t, h) = ρ(X)(t, h)

JHh′ φKρ (σ, t, h)(a) = {J¬φKρ (σ, t, h) = ¬ JφKρ (σ, t, h)
JφKρ (σ, t, min(h, h′ ))(a)if h ≥ 0otherwise

JaKρ (σ, t, h) = {ρ(a)}JµX. φKρ (σ, t, h) = lfp(f ↦ JφKρ[X→f ] (σ, −, −))(t, h)
if JφKρ (σ, t, h′ )(a) = ⊺ and h ≥ h′otherwiseJφ ≤ ψKρ (σ, t, h) = ⋀ (JφKρ (σ, t, h)(a) → JψKρ (σ, t, h)(a))
a∈A

Fig. 2.

Definition of the semantics

only appears positively, by the Kleene fixed-point theorem,
the sequence f0 (t, h) = , fn+1 (t, h) = JφKρ[X→fn ] (σ, t, h),reaches a fixed point, and JφKρ (σ, t, h) = supn∈N fn (t, h).
We apply this to Φcon from Example 3. Let us assume h ≥ 0,then we haveqyb ∨ ◊[0,d] X ρ (σ, t, h)(a) =By Lemma 9, if JφKρ (σ, t, h) = ⊺ for some h ∈ R, thenσ, t ⊧ρ φ, and similarly for . By Example 4, we know that
there are H-free formulas such that JφKρ (σ, t, h) = ⊺ for allh ∈ R. The following lemma shows that this behaviour does
not happen with infinite horizons, which is expected: having
information about the whole signal is enough to decide thesemantics.

{ρ(b)} ∨ ⋁ (ρ(X)(t, h) ∧ d(σ(a, t), σ(c, t)) ≤ d).
c∈A

If we denote by Gt the graph of agents, where a anda′ are connected if and only if d(σ(a, t), σ(a′ , t)) ≤ d,then we get that fn+1 (t, h) is the set of agents reachablefromρ(b) by a pathy of length at most n in Gt . ThereforeqµX. (b ∨ ◊[0,d] X) ρ (σ, t, h) is the set of agents reachable
from ρ(b) in Gt . Note in particular that it is a set, in thesense that it does not map any agent to ⊺. Therefore, thewhole formula states that, at all times, for all agents a andb, a is reachable from b at time t, so the communicationgraph at time t is connected.
C. Properties of horizons

Lemma 11 (+∞-determination). For all formulas φ, t ∈ R≥0 ,signals σ, and contexts ρ, either σ, t ⊧ρ φ or σ, t ⊭ρ φ.
The following lemma gives a concrete meaning to theintuition that ⊺ corresponds to a lack of information about
the signal.
Lemma 12 (Horizon lemma). For all H-free formulas φ,t ∈ R≥0 , h ∈ R, signals σ, and monotone contexts ρ:
if JφKρ (σ, t, h) = ⊺, then for all σ ′ such that σ ′ ∣[t,t+h] =σ∣[t,t+h] , σ ′ , t ⊧ρ φ,′′● if JφKρ (σ, t, h) = , then for all σ such that σ ∣[t,t+h] =′σ∣[t,t+h] , σ , t ⊭ρ φ,●Here, we discuss several properties of µTGL relative tohorizons. First, we want to show that ⊺ indeed corresponds
to the fact that the current data is not enough to conclude
whether the semantics is true or false. To represent information gain, we define the information order ⪯ on 3 generatedby ⊺ ≺ ⊺ and ⊺ ≺ . First, we should show that having alonger horizon can only lead to more information.
Lemma 9 (Monotonicity of semantics). For all H-freeformulas φ, t ∈ R≥0 , h ≤ h′ ∈ R, signals σ, and monotone
contexts ρ (i.e., such that ρ(X) is ⪯-monotone in h for allX), JφKρ (σ, t, h) ⪯ JφKρ (σ, t, h′ ).
This allows us to give meaning to the following notion:

Definition 10 (h-determination). We say that φ is hdetermined for h ∈ R≥0 , if for all times t, signals σ, andcontexts ρ, JφKρ (σ, t, h) ≠ ⊺. We write σ, t ⊧ρ φ to denotethe fact that JφKρ (σ, t, +∞) is ⊺ and σ, t ⊭ρ φ when it is .

where σ∣t,t′ is the restriction of σ to [t, t′ ].
As an immediate corollary, we get that, if there are signals
σ1 and σ2 , with σi∣[t,t+h] = σ∣[t,t+h] , σ1 , t ⊧ρ φ and σ2 , t ⊭ρφ, then JφKρ (σ, t, h) = ⊺.
By Lemma 12, the semantics of an h-determined formula
only depends on a window of size h of the signal. A
streaming algorithm is therefore able to yield a result fortime t after it has received the input signal up to time t + h.
For any formula φ, we can statically compute a horizon

φ (possibly infinite) as follows:⊺ ∶= 0,As in the previous section, we can modify (4) to obtainφ = µX. (ψ ∨ FT ◊D X), which expresses the inexistence ofcommunication chains to any agent that satisfied ψ.

f (a) > 0 ∶= 0,¬φ ∶= φ,φ ∧ ψ ∶= max(φ, ψ),◊D φ ∶= φ,F[s,t] φ ∶= φ + t,⎧⎪
⎪0 if φ = 0µX. φ ∶= ⎨⎪∞ otherwise,⎪⎩∃a. φ ∶= φ,

X ∶= 0,a ∶= 0,E. Expressive Power
We want to briefly discuss the expressive power of µTGL.
First, let us consider the variant of MITL [10] with syntax:
φ ∶∶= p ∣ ¬φ ∣ φ ∨ φ ∣ FT φ.

Here, we give some typical agent formulas that are usefulwhen specifying properties, as well as their semantics.
1) Reachability: The first class of formulas we are interested in are formulas that express reachability properties. In
our context, this corresponds to the possibility to reach anagent that satisfies some property ψ. One such formula is

In order to compare µTGL to MITL, they need to use
the same predicates, and we need to extend the set of MITL
predicates to contain some spatial operators. We thus assume
that MITL has a predicate pa for each predicate p of µTGL
and agent a which holds when p holds for agent a. We
also add a predicate da,b,D to MITL predicates for eachdistance interval D ⊆ R≥0 and agents a and b. It holds when
the distance between a and b is in D. Note that, in orderto do this, we need to know in advance all agents in the
network, so MITL is limited compared to µTGL on thatpoint. Nevertheless, to be able to compare the two logics,
we assume that the number of agents is known in advance.

Φreach,ψ = µX. (ψ ∨ ◊D X).

Lemma 14. MITL is strictly less expressive than µTGL.

Ht φ ∶= min(t, φ),φ ≤ ψ ∶= max(φ, ψ).

Lemma 13 (Bounded horizon). All formulas φ are φdetermined.
D. Notable Formulas(3)

Note that this is the shape of Φcon from Example 3. Its
semantics is basically the same as the one in Example 8,
but with a general formula ψ.
A variation on (3) is φ = µX. (ψ ∨ FT ◊D X), which adds
a temporal aspect to the formula. Its semantics JφKρ (σ, t, h)maps a to:● ⊺ if there exist agents a1 , . . . , an and times t1 , . . . , tn−1
such that a1 = a, for all i < n, d(σ(ai , ti ), σ(ai+1 , ti )) ∈D, for all i < n − 1, ti+1 − ti ∈ T , tn−1 ≤ h, andJψKρ (σ, t + tn , h − tn )(an ) = ⊺,● ⊺ if there exist agents a1 , . . . , an and times t1 , . . . , tn−1
such that a1 = a, , for all i < n, d(σ(ai , ti ), σ(ai+1 , ti )) ∈D, for all i < n − 1, ti+1 − ti ∈ T , and tn−1 > h orJψKρ (σ, t + tn , h − tn )(an ) = ⊺ (and we are not in theprevious case)●  otherwise.
Note that this is the shape of Φch from Example 4 andthat the semantics above is a formal definition of what acommunication chain from a to some agent that satisfies ψ
is. More precisely, the semantics is ⊺ if there is a chain within
horizon h, ⊺
 if there may be a chain after horizon h (but we
do not have enough information to know yet), and  if weknow there is no such chain (no matter the horizon).
2) Safety: Another class of formulas of particular interestis that of safety formulas, which in our case correspond toformulas that we can never reach an agent that satisfies someformula ψ. The typical formula that expresses this is

The translation of MITL into µTGL is straightforward.
Conversely, formulas such as Φch from Example 4 cannot be
expressed in MITL.
We can also express basic counting properties in µTGL[7], by which we mean that we can express properties suchas “at least n agents that satisfy φ”.
Given a constant integer n and a formula φ with an open
agent variable a, we can define the following syntactic sugar:Φsafe,ψ = νX. (¬ψ ∧ ◻D X).

Example 15 (Communication time). A possible refinementof Example 5 is to model the communication as taking afixed amount of time ε. We can then slightly modify (2) toobtain(4)Note that it is the negation of Φreach,ψ (up to double negations), and therefore its semantics is also negated. It therefore
exactly describes the impossibility to reach any agent thatsatisfies ψ.

(∣φ∣ ≥ n) = ∃a1 , . . . , an . (⋁ ⋁ (ai ≠ aj )) ∧ (⋀ φ[a → ai ]),
i j≠i

i

(∣φ∣ ≤ n) = ∃a1 , . . . , an . ∀a. φ → a ≤ ⋁ ai ,i(∣φ∣ = n) = (∣φ∣ ≥ n) ∧ (∣φ∣ ≤ n).
These formulas have the obvious meaning, e.g., the first onemeans “at least n agents satisfy φ”.
III. EXAMPLESIn this section, to showcase the expressive power of µTGL,
we discuss scenarios and formulas that express interesting
properties of these scenarios.
A. Communication
We start by expressing the existence of certain types ofcommunication chains in networks of communicating agents.
In all the following examples, we assume that we want tomodel a similar situation as in Example 4, where agents cancommunicate up to distance d.

G ∀a, b. a ≤ Ht µX. (b ∨ F[ε,t] ◊[0,d] X).

Note that communication chains may no longer be of arbitrary length, since at least ε has to pass when communicating
to another agent.
Example 16 (Message storing). Building on Example 15,
we can also model a scenario where agents only store themessages they receive for a finite amount of time s. The
existence of a communication chain in this scenario can be
expressed by
Ht G ∀a, b. a ⊆ µX. (b ∨ F[ε,s] ◊[0,d] X).
Example 17 (Chains of bounded length). While our logic
is not designed to, properties such as the existence ofcommunication chains of bounded length in the number of
agents can also be expressed by “unrolling” fixed points inthe previous formulas. For example, the fact that, at all times,
any two agents can communicate by passing through at mostone other agent can be expressed as
G ∀a, b. a ⊆ b ∨ ◊[0,d] (b ∨ ◊[0,d] b).
We can also model scenarios where communication isimpeded, either in some specific zones or by malicious agents
jamming signals.
Example 18 (Communication-forbidding zones). Assume
that there is a zone Z ⊆ M where communication is
impossible. We can define a predicate z such that z(x) holds
if and only if x ∈ Z. The existence of communication chains
between all agents can be expressed byG ∀a, b. a ⊆ µX. (¬z ∧ (b ∨ F[0,t] ◊[0,d] X)).
Adding the ¬z subformula ensures that all agents must beoutside Z in any communication chain.
Example 19 (Jamming agents). We can model a scenario
where malicious agents can jam the communication between
two agents if they are within distance j of either the senderor the receiver of the message. If agents evolve in space
M , we can model them as evolving in M ′ = {0, 1} × M ,with d′ inherited from d (d′ ((i, x), (i, y)) = d(x, y) andd′ ((i, x), (1 − i, y)) = 1 + d(x, y)), where malicious agentsare labelled 1. We can define a predicate j that holds on
points of the form (1, x), i.e., malicious agents.
In such a scenario, the existence of communication chains
between all agents can be expressed byG ∀a, b. ((a ∨ b ≤ ¬j) ∧ (a ≠ b)) →(a ≤ µX. (¬ ◊[0,j+1] j ∧ (b ∨ F[0,t] ◊[0,d] X)))
B. Network Topologies
Our logic can also express the existence of specific network topologies, and not only connectedness. In this section,
we will assume for simplicity that D = [0, d].
Example 20 (Star topology). The simplest topology to
express in our logic is the star topology, in which there isa single agent a that is linked to all other agents, and noother agents are linked to one another. This topology can be
expressed byΦ⋆ = ∃a. ∀b. (b ⊆ ◊D a) ∧ (a ≠ b → ◊D b ⊆ a ∨ b)
While Φ⋆ holds when agents are linked through a star
topology, it may also be useful to know when there is a starcommunication topology, possibly with more connections,which is simply expressed bỹ⋆ = ∃a. ∀b. b ⊆ ◊D a.
Φ
Example 21 (Linear topology). We can also express the factthat agents are linked through a linear topology, i.e., there
is a line of agents connecting all agents together. This canbe expressed by
Φ− = Φcon ∧ ∃a, b. ∣◊D a∣ = 2 ∧ ∣◊D b∣ = 2 ∧∀c. (c ∧ (a ∨ b) ⊆ ∅) → ∣◊D c∣ = 3.
Example 22 (Ring topology). Finally, we can also express
the fact that the communication graph between the agents
forms a ring by
Φ○ = Φcon ∧ ∀a. ∣◊D a∣ = 2.
C. MITL Properties
As expressed by Lemma 14, MITL properties (of agents)
can be expressed in µTGL. More precisely, any MITL
property φ can be translated to some µTGL formula φ′ that
describes the set of agents that satisfy φ. This translation canbe used to model certain kinds of scenarios.
The first typical case is when all agents must satisfy some
MITL property (for example a safety property, stating thatagents must stay in some safe zone). That all agents satisfy
this property is expressed in µTGL as ⊺ ≤ φ′ . The second
typical case is when at least one agent must satisfy someproperty (for example a progress property, stating that theagent much reach some zone). That at least an agent satisfies
this property is directly expressed as ¬(φ′ ≤ ).
Example 23 (MITL goals and connectivity). Let us consider a scenario where agents must “link” a starting zone
(expressed as some predicate s) to a goal zone (stated assome predicate g). Formally, there are three requirements:
1) that some agent stays in the start zone at all times(expressed as the MITL property G s), 2) that some agent
eventually reaches goal (MITL property F g), 3) that thecommunication graph stays connected at all times (µTGL
property G Φcon ). Then the formula that models the desired
property is G Φcon ∧ (⊺ ≤ G s) ∧ ¬(F g ≤ ).
IV. MONITORING
A. Monitoring Algorithm
In this section we describe an algorithm for monitoring aµTGL formula, see Algorithm 1.

1) Data structures: The algorithm manipulates values
representing piecewise constant functions R≥t0 → X, forsome set X. Such a function is represented by a sequenceof samples, pairsx = ((t0 , x0 ), . . . , (tn , xn ))where ti ∈ R≥0 and xi ∈ X. This represents the signalx̄∶ R≥t0 → X such that⎧⎪⎪xi when ti ≤ t < ti+1 , for some 0 ≤ i < n,x̄(t) = ⎨⎪xwhen tn ≤ t.
⎪
⎩ n
The time t0 is the start time and denoted start(x). Whenthe signal to be represented is only defined over some finite
interval, there is also a specified end time end(x), in whichcase x̄(t) = xn for all tn ≤ t ≤ end(x).
The main operation we need on signals represented in thisway is to zip them. This is a procedure which takes a signal
x of values of type X, a signal y of values of type Y , andproduces a signal x × y of values of type X × Y , such that

2) Computing semantics: We first describe computing thesemantics of a formula φ on a finite signal w with start time
t0 and end time end(w) = tend . The computation proceeds
by induction on the structure of φ. Most of the cases are
simple, so we will only describe the cases φ ∨ ψ, F[a,b] φand µX. φ.
● For φ ∨ ψ, the semantics are computed for φ andψ individually, producing two output signals wφ andwψ . Zipping these two signals produces wφ × wψ , asignal of pairs of signals of A-intervals. These pairs arethemselves zipped, thus producing a signal of signals ofpairs of A-intervals. Finally these pairs of A-intervals arejoined using the union operation lifted to A-intervals:[U, V ] ∨ [U ′ , V ′ ] ∶= [U ∪ U ′ , V ∪ V ′ ],thereby producing the desired result wφ∨ψ . Here we usethat [U ∪U ′ , V ∪V ′ ](a) = [U, V ](a)∨[U ′ , V ′ ](a). Mostof the other logical operations are computed in a similar
point-wise fashion. The operationx × y(t) = (x̄(t), ȳ(t))

wφ ∨ wψ ∶= wψ∨ψ

for all t for which both x̄(t) and ȳ(t) are defined. This isachieved by unifying the time-indices in x and y.
Uncertain sets, that is, functions A → 3 in the semantics,
are represented as A-intervals [U, V ] (U, V ∈ P(A)) indicating that the uncertain set could be any X ∈ P(A) such thatU ⊆ X ⊆ V , that is:⎧⊺ if a ∈ U ,⎪⎪⎪⎪[U, V ](a) = ⎨⊺ if a ∉ U and a ∈ V ,⎪⎪⎪⎪⎩ if a ∉ V .

just described will also be used in the semantics ofF[a,b] φ.
● The semantics of F[a,b] φ is computed by first computing
the semantics wφ of φ. Then, for each sample (t, wφ,t ) ∈wφ that lasts till t′ ∈ R≥0 , we construct the signal of
signals

The intuition here is that what is known about the uncertain
set is a lower bound U (elements that are surely members),
and an upper-bound V (all possible members). We denoteby  the A-interval [∅, ∅], which represents the uncertain
set a ↦ .
The uncertain sets manipulated in the algorithm also
depend on a horizon parameter h ∈ R≥0 , representing how
much future lookahead the information in the uncertain set
depends on. To model this we use signals of A-intervals
which always start from time index 0. The signal which isconstantly  is also denoted .
All in all, a semantic value w̄∶ R≥t0 × R≥0 × A → 3 isrepresented by a signal of signals of A-intervals:

F (t, t′ , wφ ) ∶= ((t0 , ), (t − b, delayb (wφ,t )), (t′ − a, ))with end time tend . This represents the information of
wφ available in [t, t′ ] given an allowed future lookahead of some duration d ∈ [a, b]. To understand thisconsider the following diagram:
0

0

t−b

a

a

b

b

t′ − att′

The blue region represents the non- portion ofF (t, t′ , wφ ). Here, a delay is needed to account for thefact that this lookahead has used up some of the horizon.
This is defined by⎧⎪when 0 ≤ s < b,⎪delayb (x)(s) = ⎨⎪x̄(s − b) when b ≤ s.
⎛ (t0 , ((h0,0 , [U0,0 , V0,0 ]), . . . , (h0,m0 , [U0,m0 , V0,m0 ]))), ⎞
⎪
⎩
⋮
⎟
w=⎜
⎝ (tn , ((hn,0 , [Un,0 , Vn,0 ]), . . . , (hn,mn , [Un,mn , Vn,mn ]))) ⎠ for all signals x. The semantics of F[a,b] φ is thenobtained by′such that⋁ F (t, t , wφ ).
⎧⊺ if a ∈ Ui,j ,⎪⎪⎪where the disjunction is taken over all the piecewise⎪w̄(t, h, a) = ⎨⊺ if a ∉ Ui,j and a ∈ Vi,j ,constant parts of wφ described above.
⎪
⎪
⎪
⎪

if
a
∉
V
.
●
The semantics of µX. φ is computed by repeatedlyi,j⎩computing the semantics of φ while using increasing
whenevervalues for resolving the variable X, starting with X = .
ti ≤ t < ti+1 and hi,j ≤ h − (t − ti ) < hi,j+1 .
Since X appears only positively in φ, successive values

Algorithm 1: Monitoring algorithm.
Input: a µTGL formula φ, a stream S
Output: a stream of {, ⊺}1 initialise the µ-cache to  for all top-level µ’s of φ;2 hmax ← φ;
3 if hmax = ∞ then
4
fail;
5 end
6 w ← ingest a window of size ≥ hmax of samples fromS;
7 t ← 0;8 repeat9o ←Semantics(φ,w);
10
yield ō(t, hmax );11drop the first sample from w and all items in theµ-cache;12t ← start(w);13s ← ingest new samples from S until w has size
≥ hmax ;14
Add a  sample to the end of all items in thecache;
15 until end of input stream S;

of X must be increasing. Since the number of agents isfinite, we are guaranteed to reach a fixed point in finite
time.
3) Streaming algorithm: We are now able to describe astreaming monitoring algorithm. This is achieved by computing an upper-bound hmax for the horizon of the formulaand then operating on a window of size hmax . Over sucha window the semantics are computed as described above.
Most forms are not computationally expensive, the exceptions are the µ-forms which may require a large numberof iterations before reaching a fixed point. Therefore, we
re-use the work done for computing the µ-forms of theprevious window. When monitoring a formula φ, all toplevelµ-forms of φ, that is, all subformulas µX. ψ of φ that are
not themselves sub-formulas of another µ-form, form theindex of the µ-cache. This is a mapping of such subformulas
to semantic values over the current time window. Whencomputing the semantics of a toplevel µ-form µX. ψ overthe current window, instead of starting the iteration at X = ,the current value of the cache is used instead.
The streaming algorithm is described in Algorithm 1. The
use of the µ-cache produces a correct result thanks to thefollowing two lemmas. The first ensures that to computeµX. ψ, the algorithm can start iterating from any element
we know to be smaller than the least fixed point, rather thanalways starting at :
Lemma 24. Assume L is a dcpo1 and that f ∶ L → L isa Scott-continuous function with least fixed point M . If
N ≤ M , then the supremum of the ascending Kleene chain
starting at N is M .
1 directed-complete partial order

The second ensures that when computing µX. ψ of a prefixof a signal, the result obtained is smaller than the result for
the full signal. In fact this is true for any positive formula:
Lemma 25. If σ ′ is a prefix of σ, and φ is positive, thenJφKρ (σ ′ , t, h)(a) ≤ JφKρ (σ, t, h)(a).
V. EXTENDED EXAMPLE: RESILIENTCONSENSUS
In this section, we prove the usefulness of our logic andmonitoring algorithm on the example of resilient consensus.
In Section V-A we give context and the existing relevant
results on resilient consensus. In Section V-B, we extendµTGL and give a formula that ensures resilient consensus.
In Section V-C, we discuss causality in consensus and deriveanother formula for resilient consensus. Finally, in Section VD, we discuss a specific example and test our monitoringalgorithm on it.
A. A Property for Resilient Consensus
We consider the resilient consensus problem in the presence of malicious/faulty agents. This problem involves anumber of cooperative agents that try to reach agreement on
a scalar value by exchanging data according to a consensus
protocol and non-cooperative agents that do not follow the
protocol either intentionally or due to a fault. In particular,
we consider scenarios where the cooperative agents do notknow which other agents are cooperative and thus may
receive and use malicious/faulty data transmitted from noncooperative agents.
It was shown in [14], [15] that consensus among cooperative agents is possible if the number of non-cooperative
agents is sufficiently small and the graph representing theinter-agent communication topology has sufficiently large
connectivity. In those articles, the connectivity of a graph
was characterized through the notion of r-robustness. For agiven a graph G with node set V , edge set E ⊆ V × V ,and neighbor sets Ni = {j ∣ (i, j) ∈ E}, i ∈ V , this notion isdefined as follows.
Definition 26 (r-robustness [14]). Given a positive integerr, a graph G is r-robust, if ∀S1 , S2 ∈ 2V ∖ {∅} suchthat S1 ∩ S2 = ∅, we have {i ∈ S1 ∣ ∣Ni ∖ S1 ∣ ≥ r} ≠ ∅ or{i ∈ S2 ∣ ∣Ni ∖ S2 ∣ ≥ r} ≠ ∅ or both.
An intuitive meaning of r-robustness is that, for any two
non-empty sets, if we choose any r − 1 nodes in the graph,then there is always a path between these two sets that avoids
these r − 1 nodes.
Recently, the notion of r-robustness was extended in [16]to handle the cases where the inter-agent communication
topology is time-varying. In the setting of [16], the communication topology at each time t ∈ N is represented by agraph G[t] with node set V , edge set E[t], and neighbor sets
Ni [t] = {j ∣ (i, j) ∈ E[t]}, i ∈ V . The notation ⋃Tτ=0 G[t−τ ]represents the union graph with node set V , and edge set⋃Tτ=0 E[t − τ ]. For a given time-varying graph G, the notionof (T, r)-robustness is defined as follows.

aDefinition 27 ((T, r)-robustness [16]). Given positive integers T and r, a time-varying graph G is (T, r)-robust if⋃Tτ=0 G[t − τ ] is r-robust for every t ≥ T .
It was shown by [16] that consensus among cooperative
agents can be achieved if there are at most F non-cooperative
agents in the network and the time-varying graph representing the communication topology is (T, 2F + 1)-robust.
Time-varying communication topologies and the notionof (T, r)-robustness are particularly useful for scenarios
where inter-agent data transmissions require the agents tobe physically close to each other. In such scenarios there is
a communication radius and two agents can exchange data
only when their distance is smaller than it.
The techniques that we introduced in earlier sections allow
us to develop monitoring algorithms for assessing (T, r)robustness in scenarios with time-varying communication
topologies by using the history of the physical locations ofagents and the communication radius.
B. Extending µTGL
In order to express (T, r)-robustness, we extend µTGL
with a second-order agent quantification construct ∃s. φ withthe following semantics:
J∃s. φKρ (σ, t, h) = ⋁ JφKρ[s→S] (σ, t, h).
S⊆AThis extension comes with syntactic sugar a ∈ S ≡ a ≤ s,a ∉ s, and ∣s∣ ≥ n and such defined as in Section II-E. We
also allow truth formulas inside agent formulas. For example,
we allow formulas such as µX. Φ ∧ (b ∨ ◊D X), which isthe connected component of ρ(b) if Φ holds, and empty
either. Formally, the semantics of a truth formula seen as anagent formula is defined as JΦKρ (σ, t, h)(a) = JΦKρ (σ, t, h)(where Φ is seen as a truth formula on the right). Extending
the monitoring algorithm is straightforward.
With this extension of µTGL, we can directly encode thedefinition of (T, r)-robustness.
Lemma 28 ((T, r)-robustness in µTGL). Given a signal
σ, a distance interval D ⊆ R≥0 , T ∈ R≥0 , and r ∈ N,
the communication graph is (T, r)-robust if and only if σsatisfiesG ∀s, s′ . (∃a. a ∈ s ∧ a ∈ s′ ) ∨ reachT,r (s) ∨ reachT,r (s′ ),where reachT,r (s) is∃a, a1 , . . . , ar . a ∈ s ∧ (⋀ri=1 ⋀rj=i+1 ai ≠ aj ) ∧(⋀ri=1 ai ∉ s ∧ ai ≤ F[0,T ] ai ) .
C. Robustness and Causality
As we explained, an intuition behind r-robustness is thatit guarantees the existence of paths that avoid any fixed r − 1
agents. However, the notion of (T, r)-robustness does nothave the same intuition, because it not causal: the path in⋃Tτ=0 G[t − τ ] may not be a causal chain, as illustrated in thenext example.
Example 29 ((T, r)-robustness and causality). Let us consider a scenario with three agents a, b, and c, moving

b

c

space

d
T

2T
time
Fig. 3. A (T, 1)-robust network. However, c cannot send a message to awithin time T at t = 0

on a line, as according to Section V-C, and which are allcooperating. This network is (T, 1)-robust, but at time t = 0,c cannot send a message to a within time T .
However, since agents can only act based on the messages
they have received, whether there is consensus or not does
not depend on non-causal properties. Therefore, we may
refine (T, r)-robustness into a causal property.
Definition 30 (Causal (T, r)-robustness). Given T ∈ R≥0 andr ∈ N, a time-varying graph G is causally (T, r)-robust if,
for every t ∈ R≥0 , ∀S1 , S2 ∈ 2V ∖ {∅} such that S1 ∩ S2 = ∅,for any i1 , . . . , ir−1 , there is a causal chain that starts fromsome i ∈ S1 at time t, ends at some j ∈ S2 at time t + T , andavoids all ik ’s.
Lemma 31 (Causal and non-causal (T, r)-robustnesses).
Causal (T, r)-robustness implies (T, r)-robustness. Conversely, if the network contains n agents, (T, r)-robustness
implies causal ((n − r)(n − r + 1)T /2, r)-robustness.
In particular, monitoring causal (T, r)-robustness isenough to guarantee consensus, and it may be faster: monitoring (T, r)-robustness may be in some cases as costly monitoring ((n − r)(n − r + 1)T /2, r)-robustness. The following
formula describes causal (T, r)-robustness in µTGL.
Lemma 32 (Causal (T, r)-robustness in µTGL). Given T ∈R≥0 , r ∈ N, and D ⊆ R≥0 the communication graph iscausally (T, r)-robust if and only if σ satisfies
G ∀a, b, x1 , . . . , xr .
r

( ⋀ ¬(xi ≤ (a ∨ b))) →i=1

ra ≤ HT µX. (¬ ( ⋁ xi ) ∧ (b ∨ F[0,T ] ◊D X)).
i=1

D. Monitoring for Resilient Consensus
We experimented on a perimeter surveillance scenario[16]. In this scenario, mobile robots circle around a point,with possibly different radii and velocities, and some of them
may be faulty or malicious. The robots in the network try toreach consensus to agree on a perimeter to circle. We monitored causal (T, r)-robustness, as expressed in Lemma 32,
which ensures that there is consensus.

falsification, we need to define a robust (or quantitative)
semantics, which will prove challenging, since the logic
is not boolean. Another direction is to look further into
causal robustness, its relationship to non-causal robustness,
and whether it can be of algorithmic interest.
R EFERENCES

Fig. 4.

Signals in the perimeter surveillance scenario

We created two sets of data with eight agents (among
which one malicious agent), where agents act according to
the control policy described in [16]. The only difference
between the two data sets is that, in the first case, thecommunication radius is 0.2, while it is 0.5 in the second.
The radius of the perimeter circled by each agent over timein the two data sets is plotted in Section V-D. It can be seenthat cooperative agents reach consensus in the second case,but not in the first one (there are two clusters).
We ran our monitoring algorithm on the two data sets forcausal (T, r)-robustness for r = 3 (which corresponds to 1
malicious agent). For the first example, we monitored causal
robustness for T = 120, and it did not hold, which means that
(non-causal) robustness is false for T = 8. For the second
example, we monitored causal robustness for T = 35, and it
held, ensuring consensus.
VI. CONCLUSION
We defined µTGL, showed its usefulness in expressing interesting properties of agent networks, designed a monitoringalgorithm for it, and showed its validity on an example toprove resilient consensus.
There is much left to do in the future. First, while thisexposition of µTGL has a strong spatial flavour, it is actuallycloser to a graph logic, and we want to study it from thatangle too. From a practical point of view, it may be interesting to look at general n-ary relations (rather than binary◇), since they can be used to model interesting properties,
such as more general jamming possibilities. To shorten thehorizon used by the monitoring algorithm, we want to refine
the definition of the horizon formula, which will require
some work to detect tautologies in the logic. Finally, forµTGL to be usable in advanced testing techniques such as[1] E. Bartocci, J. Deshmukh, A. Donzé, G. Fainekos, O. Maler,
D. Ničković, and S. Sankaranarayanan, “Specification-based monitoring of cyber-physical systems: a survey on theory, tools andapplications,” in Lectures on Runtime Verification. Springer, 2018,
pp. 135–175.
[2] L. Bortolussi and L. Nenzi, “Specifying and monitoring propertiesof stochastic spatio-temporal systems in signal temporal logic,” inProceedings of the 8th International Conference on Performance
Evaluation Methodologies and Tools, 2014, pp. 66–73.
[3] L. Nenzi, L. Bortolussi, V. Ciancia, M. Loreti, and M. Massink, “Qualitative and quantitative monitoring of spatio-temporal properties,” in
Runtime Verification. Springer, 2015, pp. 21–37.
[4] I. Haghighi, A. Jones, Z. Kong, E. Bartocci, R. Gros, and C. Belta,“Spatel: a novel spatial-temporal logic and its applications to networked systems,” in Proceedings of the 18th International Conference
on Hybrid Systems: Computation and Control, 2015, pp. 189–198.
[5] E. A. Gol, E. Bartocci, and C. Belta, “A formal methods approach
to pattern synthesis in reaction diffusion systems,” in 53rd IEEE
Conference on Decision and Control. IEEE, 2014, pp. 108–113.
[6] I. Haghighi, S. Sadraddini, and C. Belta, “Robotic swarm control
from spatio-temporal specifications,” in 2016 IEEE 55th Conferenceon Decision and Control (CDC). IEEE, 2016, pp. 5708–5713.
[7] Y. E. Sahin, P. Nilsson, and N. Ozay, “Multirobot coordination withcounting temporal logics,” IEEE Transactions on Robotics, vol. 36,
no. 4, pp. 1189–1206, 2019.
[8] D. Kozen, “Results on the propositional mu-calculus,” Theor.
Comput. Sci., vol. 27, pp. 333–354, 1983. [Online]. Available:
https://doi.org/10.1016/0304-3975(82)90125-6[9] R. Koymans, “Specifying Real-Time Properties with Metric Temporal
Logic,” Real Time Syst., vol. 2, no. 4, pp. 255–299, 1990. [Online].
Available: https://doi.org/10.1007/BF01995674[10] R. Alur, T. Feder, and T. A. Henzinger, “The Benefits of Relaxing
Punctuality,” J. ACM, vol. 43, no. 1, pp. 116–146, 1996. [Online].
Available: https://doi.org/10.1145/227595.227602[11] O. Maler and D. Nickovic, “Monitoring Temporal Properties
of Continuous Signals,” in FORMATS 2004, ser. Lecture Notes
in Computer Science, Y. Lakhnech and S. Yovine, Eds., vol.
3253. Springer, 2004, pp. 152–166. [Online]. Available: https://doi.org/10.1007/978-3-540-30206-3 12[12] P. Baldan, A. Corradini, B. König, and A. Lluch-Lafuente, “A temporalgraph logic for verification of graph transformation systems,” in
WADT 2006, ser. Lecture Notes in Computer Science, J. L. Fiadeiro
and P. Schobbens, Eds., vol. 4409. Springer, 2006, pp. 1–20.
[Online]. Available: https://doi.org/10.1007/978-3-540-71998-4 1[13] M. Bergmann, An Introduction to Many-Valued and Fuzzy Logic:
Semantics, Algebras, and Derivation Systems. Cambridge University
Press, 2008.
[14] H. J. LeBlanc, H. Zhang, X. Koutsoukos, and S. Sundaram, “Resilient
asymptotic consensus in robust networks,” IEEE Journal on Selected
Areas in Communications, vol. 31, no. 4, pp. 766–781, 2013.
[15] H. Zhang, E. Fata, and S. Sundaram, “A notion of robustness in complex networks,” IEEE Transactions on Control of Network Systems,
vol. 2, no. 3, pp. 310–320, 2015.
[16] D. Saldana, A. Prorok, S. Sundaram, M. F. Campos, and V. Kumar,“Resilient consensus for time-varying networks of dynamic agents,”
in Proc. American control conference, 2017, pp. 252–258.