Paper deep dive
Monitoring Diameters of Causal Communication Graph with Spatio-Temporal Logic
Lydia Bakiri, Jérémy Dubut, Sergio Mover
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 90%
Last extracted: 7/9/2026, 6:31:40 AM
Summary
This paper addresses the verification of multi-agent systems by extending the spatio-temporal logic μ-TGL with a 'space horizon' operator. This extension enables bounding communication chain distances and tracking communication costs, addressing limitations in analyzing reachability and system diameter. The authors provide a centralized offline monitoring algorithm with three-valued semantics and demonstrate its application on Consensus-Based Bundle Algorithms for task allocation.
Entities (7)
Relation Signals (7)
Space Horizon → extends → μ-TGL
confidence 95% · introduce an extension of muTGL, including a new operator called the space horizon
Space Horizon → enablesbounding → Communication Chain Distance
confidence 90% · allows us to bound the distance of communication chains
Centralized Offline Monitoring Algorithm → evaluates → Extended μ-TGL
confidence 90% · provide a centralized offline monitoring algorithm for this logic
μ-TGL → lacksexpressivityfor → Distance-Bounded Reachability
confidence 90% · lacks the expressivity needed to analyse reachability within specific distance bounds
Centralized Offline Monitoring Algorithm → appliedto → Consensus-Based Bundle Algorithms
confidence 85% · illustrate it on several examples on simulations of Consensus-Based Bundle Algorithms
μ-TGL → combines → MITL
confidence 85% · combines ideas from Metric Interval Temporal Logic (MITL [3]) and the modal μ-calculus
STREL → provides → Global Spatio-Temporal Operators
confidence 80% · STREL logic introduces more global spatio-temporal operators such as reachability and escape
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Verification of multi-agent systems requires the ability to check meticulous topological properties when it comes to agents that can move through space in continuous time. This demands a logic with sufficient expressiveness to capture these dynamics. MuTGL logic has interesting properties for expressing entangled space-time properties. However, this logic lacks the expressivity needed to analyse reachability within specific distance bounds, or to track the length or the cost of communication chains: these are fundamental for decentralized monitoring, or graph-theoretic analysis of distributed protocols, where algorithmic complexities often relates with the system's communication graph diameter. We then introduce an extension of muTGL, including a new operator called the space horizon. This addition allows us to bound the distance of communication chains, hence enhancing the logic's expressiveness. We show that this operator allows to encode modalities from other logics, such as reachability or escaping which were not available in vanilla muTGL, while allowing a deeper entanglement of spatial and temporal properties. We provide a centralized offline monitoring algorithm for this logic and illustrate it on several examples on simulations of Consensus-Based Bundle Algorithms, distributed protocols for task allocation.
Tags
Links
- Source: https://arxiv.org/abs/2606.21558v1
- Canonical: https://arxiv.org/abs/2606.21558v1
Trouble viewing inline? Open PDF directly →
Full Text
76,351 characters extracted from source content.
Expand or collapse full text
11institutetext: LIX, CNRS, École polytechnique, Institut Polytechnique de Paris, Palaiseau, France 11email: firstname.lastname@polytechnique.edu Monitoring Diameters of Causal Communication Graph with Spatio-Temporal Logic Lydia Bakiri Jérémy Dubut Sergio Mover Abstract Verification of multi-agent systems requires the ability to check meticulous topological properties when it comes to agents that can move through space in continuous time. This demands a logic with sufficient expressiveness to capture these dynamics. μ-TGL logic has interesting properties for expressing entangled space-time properties. However, this logic lacks the expressivity needed to analyse reachability within specific distance bounds, or to track the length or the cost of communication chains: these are fundamental for decentralized monitoring, or graph-theoretic analysis of distributed protocols, where algorithmic complexities often relates with the system’s communication graph diameter. We then introduce an extension of μ-TGL, including a new operator called the space horizon. This addition allows us to bound the distance of communication chains, hence enhancing the logic’s expressiveness. We show that this operator allows to encode modalities from other logics, such as reachability or escaping which were not available in vanilla μ-TGL, while allowing a deeper entanglement of spatial and temporal properties. We provide a centralized offline monitoring algorithm for this logic and illustrate it on several examples on simulations of Consensus-Based Bundle Algorithms, distributed protocols for task allocation. 1 Introduction Increasingly, critical infrastructures are being deployed as systems of systems that are highly distributed, autonomous, and interconnected. Such systems are becoming progressively more complex due to the growing number of interacting components and their dynamic environments. As a consequence, providing strong assurances regarding their correctness, safety, and overall behavior is becoming increasingly challenging. A central concern is the robust and efficient realization of distributed coordination mechanisms, such as consensus, task assignment, rendez-vous protocols, and related collective behaviors. These mechanisms must remain operational in the presence of failures or unexpected disruptions while simultaneously minimizing communication overhead, execution time, energy consumption, and other resource costs. Achieving these objectives strongly depends on the structure of the underlying communication graph. Robustness requirements often demand sufficient connectivity to tolerate failures and preserve information flow, whereas efficiency considerations require properties such as a limited graph diameter to reduce protocol rounds and resource consumption. The problem becomes significantly more challenging when communication topologies evolve over time, as occurs naturally in systems whose components move through physical space, such as fleets of autonomous vehicles or swarms of drones. In such settings, desirable graph properties become intricate entanglement of spatial and temporal constraints. Their analysis requires particular care because causality effects emerge naturally: communication relations are inherently directed in time, and chains of interactions cannot be treated as static connections. For example, if subsystem A communicates with B at time t0t_0, and B subsequently communicates with C at time t1>t0t_1>t_0, information may flow from A to C, but not necessarily in the reverse direction. Temporal ordering therefore induces asymmetric information dependencies that must be explicitly accounted for when reasoning about correctness and performance. Given the complexity and dynamic nature of these systems, applying heavyweight formal verification techniques at the scale of realistic systems of systems quickly becomes impractical. Instead, we focus on lightweight assurance methods, and in particular on monitoring techniques. Our setting is especially well-suited to centralized monitoring architectures, as many real-world systems of systems involve a human operator responsible for high-level strategic decisions while the individual subsystems operate autonomously at a lower level, as it is the case for directed systems of systems [15]. In this context, online monitoring can serve several complementary purposes. It may provide feedback to assist the human operator in adapting or correcting global strategies whenever potentially unsafe communication patterns or undesirable emergent behaviors are detected. It can also be integrated directly into a control loop, where it acts as a runtime filtering mechanism capable of rejecting decisions or execution paths predicted to lead to communication failures or degraded performance, as a safety shield during the learning of optimal policies [1], or as a component of a decision module responsible for selecting the appropriate controller within a Simplex architecture [22]. However, enabling such capabilities requires addressing two fundamental challenges. First, one needs a specification language expressive enough to capture the intricate interplay between spatial and temporal communication properties, including the causality constraints induced by evolving interaction patterns. Second, one needs effective monitoring algorithms capable of evaluating these specifications. In this work, we consider μ-TGL (Timed Graph Logic with fixpoint), a spatio-temporal logic previously introduced in [9]. This logic combines ideas from Metric Interval Temporal Logic (MITL [3]) and the modal μ-calculus [13]. It includes temporal modalities similar to the MITL F operator, as well as spatial modalities expressing the existence of agents satisfying a given property in the vicinity of the current agent. Crucially, μ-TGL also incorporates fixpoint operators. While the temporal and spatial modalities themselves are relatively local in nature—contrary to more global operators such as temporal until or graph reachability—the addition of fixpoints makes it possible to express complex recursive patterns that tightly interleave spatial and temporal reasoning. Such expressive power is essential for capturing the kinds of properties discussed above, where information propagation depends simultaneously on connectivity structures, movement patterns, and causality constraints. In particular, this framework enabled the specification of notions such as causal robust connectivity, a property extending robust connectivity, required to guarantee consensus in the presence of faulty agents [14], to the context of dynamically evolving communication graphs. A major challenge in this setting lies in designing semantics suitable for online monitoring. Following standard approaches, we rely on a three-valued semantics [5] in which an indeterminate value represents situations where the available observations are still insufficient to decide whether a formula is satisfied or violated. However, the presence of fixpoint operators introduces significant additional difficulties. In particular, care is required to manage computationally the notion of a time horizon, representing the amount of future information that may be needed before safely concluding that a property cannot be satisfied. In this paper, we address a limitation of the current logic. While μ-TGL allows one to constrain temporal propagation through its notion of time horizon, it currently lacks the ability to express that information propagates through communication chains that are spatially bounded, namely chains whose length remains limited in terms of communication hops or spatial cost. Such a capability is important in several related frameworks. For instance, the STREL logic [18, 17] introduces more global spatio-temporal operators such as reachability and escape, which have been successfully used to model phenomena including network routing protocols and virus propagation. In our context, this type of property is equally important for the monitoring of distributed protocols. The ability to constrain spatial propagation would make it possible to specify and monitor properties such as bounded communication diameter, which directly impacts the number of rounds required by many distributed algorithms, or bounded communication cost, which is closely related to energy consumption and resource usage. The syntactic extension proposed in this paper is remarkably simple: we introduce a space horizon operator that mirrors the role played by the time horizon mechanism in standard μ-TGL. However, extending the semantics and monitoring procedures to support this additional operator is substantially more challenging. The space budget must be carefully propagated and managed throughout the evaluation process, while the presence of fixpoint operators again introduces significant technical difficulties. In particular, ensuring that fixpoints remain computable through a finite number of iterations requires substantial modifications to both the semantic framework and the monitoring algorithm. Related Work (Spatio-)Temporal Logics. Our work is based on μ-TGL [9]. The closest logic is STREL [18, 17] – and by extension, its ancestors Spatial-Temporal Logic [10] (SpaTeL) and Signal Spatio-Temporal Logic [16] (SSTL) – however they cannot express suitable causal properties because their modalities are not sufficiently fine-grained in their interactions between time and space: their space modalities only look at the communication graph at a fixed time. Similarly, Counting Linear Temporal Logic [21] (cLTL) enables the specification of desired behaviors in multi-agent systems by allowing constraints on the number of agents satisfying particular LTL properties. The recent Hybrid Spatio-temporal Logic [23] (HSTL) combines ideas from both spatio-temporal and hybrid logics and is targeting the safety assurance of fleets of autonomous vehicle in highway scenarios. Although Signal Temporal Logic (STL) is not, strictly speaking, a spatio-temporal logic, spatial aspects can nevertheless be encoded within its atomic propositions, allowing certain spatial properties to be represented indirectly. More generally, logics for the verification of multi-agent systems is a hot topic, see for example Alternating-Time Temporal Logic [2] and its various extensions and fragments. Distributed Protocols. The motivation for this work is to be able to monitor spatio-temporal properties to ensure that some distributed protocols can be executed, even when agents can fail in a malicious way (Byzantine). The distributed protocols we are interested in are those that allow the agents to agree: consensus [19], task allocation typically through auctions [7], gathering [6], etc. Contributions We extend both the syntax and the semantics of μ-TGL, to be able to specify properties on the diameter of causal communication graphs or the length of communication chains. We implement an offline monitoring algorithm, implementing this semantics, and carefully prove its termination. We illustrate its feasibility on simulations of agents following Consensus-Based Bundle Algorithms, distributed protocols for task allocation. 2 Recap on μ-TGL μ-TGL and the extension introduced in this paper are logics over timed graphs, that is, signals whose values are weighted graphs. Such a graph represents a network of agents: its vertices correspond to the agents themselves, while an edge between two agents indicates that they can communicate. The weight associated with an edge captures quantitative information about the communication, such as the distance between the agents, the energy required to communicate, or a similar metric. Fix a set A of agents. A timed graph is simply a function σ:ℝ≥0×2→ℝ¯≥0σ\> \>R_≥ 0×A^2→ R_≥ 0, which maps a time and a pair of agents to the cost of communication between them, with the value +∞+∞ indicating that communication is impossible. Typically, agents move within a Euclidean space ℝnR^n, and the weights of a timed graph are obtained by applying a weighting function to the distances between agents. Examples include: 1) the identity function, in which case the weights are the distances themselves; 2) the constant function equal to 11, in which case the weights only encode the existence of a communication link (referred to as hops in [17]); 3) an energy function of the form E(d)=dγE(d)=d^γ, where γ is the path-loss exponent, whose value depends on the environment [20]. The primary purpose of μ-TGL is to express specifications such as: “it is possible to send a message to agent a through a causal chain of communications within a given time bound.” Let chaina chain_a denote such a formula. The semantic value of chaina chain_a depends on: 1) the timed graph, 2) the agent from which the message originates, 3) the time at which the message is sent, and 4) the available time budget. Example 1(Horizons) Let us illustrate this on this timed graph a11bbcc11ddee a11bbcc11ddee aabb11c11ddee where the left graph is at time 0, the center one is at time 11 and the right one is from time 22. When there is an edge (or a direct communication) between agents a and b at a given time t, then chaina chain_a is true for agent b at time t, for any time budget. Now observe that d does not communicate with c at time 0, but does so at time 11. This means that, for chainc chain_c to be true at time 0 for agent d, we need a time budget of at least 11. Since c communicates with b until time 22, chainb chain_b is also true for d at time 0 with a time budget of 11. Similarly, since d and e communicate at time 0, there is a causal communication chain e→d→c→be→ d→ c→ b that only requires a time budget of 11. Observe, however, that the reverse communication chain is not causal because d and e communicate at time 0, while d and c communicate at time 11. Therefore, e does not receive information from c via d, which means that chaine chain_e is false for agent c at time 0 for any time budget smaller than 22. In addition, to accommodate online monitoring, the semantics must take into account that we may not have enough information about the timed graph, as samples are received when available. For example, imagine that we want to monitor whether there is a causal communication chain from e to a within a time budget of 22 at time 0. From the analysis above, we know that this property is true if we have access to the three samples above. Now assume that we have only received the first two samples, but not the third one. In that case, we have not found a causal chain, but we have not yet received enough information to exhaust the allocated time budget. Therefore, the semantics should indicate that the truth value is not yet determined. To write such specifications, μ-TGL relies on modalities for both time and space constraints. Precisely, we have three modalities: FTφF_T\, , the usual “eventually” from MITL; ◇Dφ _D\, , similar to F\, but for space, requiring the existence of an agent at a distance in the interval D; and HhφH_h , which fixes a time budget of h; together with the usual Boolean connectives and atomic propositions, which correspond to individual agents. Given a timed graph σ, the semantics of such a formula ϕφ is then, as described above, a function of type ⟦ϕ⟧σ:ℝ≥0×ℝ×→3 φ _σ\> \>R_≥ 0×R×A 3, where 3 is the three-valued ordered set ⊥≤⊤⊥≤⊤ ≤ to0.0pt$ $ ≤ , consisting of Booleans extended with an indeterminate value. The intention is that ⟦φ⟧σ(t,h,a) _σ(t,h,a) gives the truth value of φ for agent a at time t with time budget h. In particular, for the three modalities: • ⟦FTφ⟧σ(t,h,a)=⋁t′∈T⟦φ⟧σ(t+t′,h−t′,a) F_T\,\> _σ(t,h,a)= _t ∈ T _σ(t+t ,h-t ,a) • ⟦◇Dφ⟧σ(t,h,a)=⋁b∈A⟦φ⟧σ(t,h,b)∧σ(t,a,b)∈D if h≥0⊤⊥ otherwise _D\,\> _σ(t,h,a)= \ array[]lr _b∈ A _σ(t,h,b) σ(t,a,b)∈ D& if h≥ 0\\ to0.0pt$ $ & otherwise array . • ⟦Hh′φ⟧σ(t,h,a)=⊥ if ⟦φ⟧σ(t,h′,a)=⊤⊥ and h≥h′⟦φ⟧σ(t,min(h,h′),a) otherwise H_h \> _σ(t,h,a)= \ array[]lr & if _σ(t,h ,a)= to0.0pt$ $ and h≥ h \\ _σ(t, (h,h ),a)& otherwise array . In particular, the time budget works as follows: whenever we try to access the timed graph without having any remaining budget, the result is indeterminate, which is the case in ◇D _D\,. This indeterminate value is then resolved to false when encountering a modality Hh′H_h with h′h small enough: if we could not determine the truth value within the time budget, then the formula is false. Finally, in order to iterate these local time and space properties, μ-TGL contains a fixpoint operator μX.φμ X.\> . Its semantics is defined as a least fixpoint. When a formula φ has X as a free variable, i.e., not bound by a μ, the semantics ⟦φ⟧σ _σ can be seen as a function from ℝ≥0×ℝ×→3R_≥ 0×R×A 3 to itself. This set is a complete lattice under the pointwise order. Furthermore, as usual, when φ is positive, i.e., every branch of φ ending in X contains an even number of negations, this function is monotone. Then, by the Cousot–Cousot theorem [8], the least fixpoint exists and can be computed by iteratively applying the semantic function to the least element of the lattice (namely, the constant function equal to ⊥ ). Example 2(Horizons, continued) For example, we can define: chaina=μX.(a∨F[0,1]◇[0,1]X). chain_a=μ X. (a F_[0,1]\,\, _[0,1]\,\,X ). Starting from the constant function f0f_0 equal to ⊥ and applying the function ⟦a∨F[0,1]◇[0,1]X⟧σ a F_[0,1]\, _[0,1]\,\>X _σ once, we obtain f1(t,h,ag)=⊤f_1(t,h,ag)= if ag=aag=a, and ⊥ otherwise. After another iteration, we obtain that, for example, f2(0,h,ag)f_2(0,h,ag) is ⊤ when ag=aag=a, or when ag=bag=b and h≥1h≥ 1. After enough iterations, we obtain that fk(0,h,e)f_k(0,h,e) is ⊤ if h≥2h≥ 2 and ⊤⊥ to0.0pt$ $ otherwise. This is actually the case for the least fixpoint as well, i.e., for ⟦chaina⟧σ(0,h,e) chain_a _σ(0,h,e). This means, in addition, that: ⟦H1chaina⟧σ(0,2,e)=⊥⟦H2chaina⟧σ(0,2,e)=⊤. H_1\> chain_a _σ(0,2,e)= H_2\> chain_a _σ(0,2,e)= . 3 Space horizon for μ-TGL In this section, we extend the syntax and the semantics of μ-TGL to be able to write specifications such that “agent a can send a message to agent b with a communication chain that costs less than p” or “agent a can send a message that will propagate to a distance more than p”. Those specifications are the Reach and Escape formulas that are part of the syntax of STRel [17]. To follow the line of μ-TGL, we will not have those specifications natively in our extension because they are global properties on the graph. Instead, we will define them thanks to our local modalities and the usage of a fixpoint. It turns out that the only piece missing in the syntax is a space horizon, similar to the modality HhH_h of vanilla μ-TGL. This has two advantages: 1) the modification of the logic is seemingly minimal (although some non-trivial work has to be done in the semantics) 2) this allows to defined Reach and Escape in a causal and timed way. Indeed, for the latter, in STRel, those constructions are untimed in the sense that they only look at the communication graph at a fixed time. Concretely, Definition 1(Agent Formulas) Agent formulas are given by the following grammar: φ::=⊤|p|¬φ|φ∧φ|◇Dφ|FTφ|X|μX.φ|Hhϕ|a|∃a.φ|∙sφ, ::= \>|\>p\>|\> \>|\> \>|\> _D\, \>|\>F_T\, \>|\>X\>|\>μ X. \>|\>H_hφ\>|\>a\>|\>∃ a. \>|\> [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0 _s , where the only addition to the syntax of μ-TGL is the modality ∙sφ _s , the space horizon. In this grammar: p is a predicate, D and T are closed intervals of non-negative reals, a is an agent variable, X is a fixpoint variable, and h and s are non-negative reals. Example 3(Horizons, continued) We have seen that for ⟦chaina⟧σ(0,h,e) chain_a _σ(0,h,e) to be true, we need a time budget of at least 2, so that we have a causal communication chain from e to a, meaning essentially that e satisfies H2chainaH_2\> chain_a but not H1chainaH_1\> chain_a at time 0. Now observe that the unique causal communication chain from e to a has length 44. The intention is then that e satisfies ∙sHhchaina _s\>H_h\> chain_a at time 0 if and only if s≥4s≥ 4 and h≥2h≥ 2. The goal now is to formalize this intention in the semantics. As for the time horizon, we need to keep track explicitly of the space horizon in the semantics. As such, the extended semantics will be a function of type ⟦φ⟧σ,ρe:ℝ≥0×ℝ×ℝ¯×→3 _σ,ρ^e\> \>R_≥ 0×R× R×A 3 where σ is a timed graph and ρ is a valuation mapping every non-binded agent variable to an agent and every non-binded fixpoint variable to a function of the same type as the extended semantics. The arguments of those functions are as follows: 1) the time t≥0t≥ 0 at which we check the satisfaction, 2) the time horizon h, 3) the space horizon s, and 4) the agent for which we are checking the satisfaction. Observe the crucial point that the space horizon is an extended real, meaning that it can be infinite. The reason is we need to keep track of the semantics when we have the full visibility of the graph at a given time, which is not necessarily the same as having the visibility with a large enough horizon as we will see later. Concretely, the extended semantics is defined by induction on the formula as follows (we only focus on the interesting cases) ⟦◇Dφ⟧σ,ρe(t,h,s,a,b) _D\,\> _σ,ρ^e(t,h,s,a,b) =⊤ if σ(t,a,b)∈D∧σ(t,a,b)≤s∧⟦φ⟧σ,ρe(t,h,s−σ(t,a,b),b)=⊤⊥ if (σ(t,a,b)>s∧max(D)>s)∨(s≥σ(t,a,b)∧σ(t,a,b)∈D⟦φ⟧σ,ρe(t,h,s−σ(t,a,b),b)=⊤⊥)⊥otherwise = \ array[]lr & if σ(t,a,b)∈ D\\ & \;σ(t,a,b)≤ s\\ & \; _σ,ρ^e(t,h,s-σ(t,a,b),b)= \\ &\\ to0.0pt$ $ & if (σ(t,a,b)>s (D)>s )~ \\ & (s≥σ(t,a,b) σ(t,a,b)∈ D\\ &\;\;\;\; _σ,ρ^e(t,h,s-σ(t,a,b),b)= to0.0pt$ $ )\\ &\\ &otherwise array . ⟦◇Dφ⟧σ,ρe(t,h,s,a) _D\,\> _σ,ρ^e(t,h,s,a) =⋁b∈A⟦◇Dφ⟧σ,ρe(t,h,s,a,b) if h≥0⊤⊥ otherwise = \ array[]lr _b∈ A _D\,\> _σ,ρ^e(t,h,s,a,b)& if h≥ 0\\ to0.0pt$ $ & otherwise array . ⟦∙s′φ⟧σ,ρe(t,h,s,a) _s \> _σ,ρ^e(t,h,s,a) =⊥ if ⟦φ⟧σ,ρe(t,h,s′,a)=⊤⊥∧s≥s′⟦φ⟧σ,ρe(t,h,min(s,s′),a) otherwise = \ array[]lr & if _σ,ρ^e(t,h,s ,a)= to0.0pt$ $ \\ &\;\;\;\; ~s≥ s \\ _σ,ρ^e(t,h, (s,s ),a)& otherwise array . ⟦μX.φ⟧σ,ρe μ X.\> _σ,ρ^e =lfp(f↦⟦φ⟧σ,ρ[X→f]e(σ,−,−,−,−)) =lfp(f _σ,ρ[X→ f]^e(σ,-,-,-,-)) Figure 1: Extended semantics. Definition 2(Extended Semantics) We define the extended semantics as in Figure 1 where the least fixpoint is taken in the complete lattice of functions of type ℝ≥0×ℝ×ℝ¯×→3R_≥ 0×R× R×A 3 with the pointwise order. The rest is defined as in vanilla μ-TGL. Observe that the semantics of the space-horizon modality is similar to the time-horizon. Most of the work is done in the semantics of the spatial modality ◇ . The intention of ◇Dφ _D\> is to check if there is another agent satisfying φ , for which the distance is within the interval D. In vanilla μ-TGL, that is where indeterminate can appear: this modality is where we actually have to have access to the graph, and if we do not have time budget anymore, we cannot access the graph, and we cannot know if there exists such an agent. In our extension, there is another case where this could happen because of the space budget. An edge between two agents a and b is valid for this modality if its weight is within the interval D and within the space budget. In that case, if furthermore b satisfies φ with the discounted space horizon, then b is a witness that a satisfies ◇Dφ _D\> . If no b satisfy these requirements, but if the space horizon s is smaller than the maximal value of D (meaning that the current space budget does not allow to cover the whole interval D) and if the weight of the transition between a and b is bigger than s (i.e., the current space horizon does not allow to see this transition), then b may be a witness but we cannot decide yet. Example 4(Horizons, continued) With this new semantic, the expression chainachain_a evaluates as follows: at the base step of the fixpoint construction, the formula holds for agent a only, and leaves the other agents either false or indeterminate due to lack of horizon: f1(t,h,s,ag)=⊤ if ag=a⊤⊥ if ag≠b and s<1∨h=0⊥ otherwise f_1(t,h,s,ag)= \ array[]l & if ag=a\\ to0.0pt$ $ & if ag≠ b and s<1 h=0\\ & otherwise \\ array . As the iteration count increases, the recursive application of the semantic allows other agents to be valid dependently on the budget allowed for space horizon. For example, agent b will satisfy the constraints as long as the time horizon permits to see the third graph and s≥1s≥ 1. After completing the full fixpoint computation, we end up with a semantic that confirms that: ⟦chaina⟧σ,ρe(0,2,4,e)=⊤⟦chaina⟧σ,ρe(0,2,s,e)=⊤⊥ chain_a _σ,ρ^e(0,2,4,e)= chain_a _σ,ρ^e(0,2,s,e)= to0.0pt$ $ for s<4s<4. This gives the following intended result: ⟦∙3H2chaina⟧σ,ρe(0,2,4,e)=⊥⟦∙4H2chaina⟧σ,ρe(0,2,4,e)=⊤ _3\>H_2\> chain_a _σ,ρ^e(0,2,4,e)= _4\>H_2\> chain_a _σ,ρ^e(0,2,4,e)= Also note that in this example, a naive computation of the fixpoint takes a infinite amount of time. See what is happening at time 0 and horizon 2: fn(1,1,s)f_n(1,1,s) keeps all agents either ⊤ or ⊤⊥ to0.0pt$ $ if s<ns<n. But when s≥ns≥ n, all indeterminate agents become ⊥ , hence determinizing all agent as if there were no restriction. Future iterations propagate these indeterminate agents, leading to an infinite computation if we don’t take that into account. In this case, the fixpoint result of ⟦chaina⟧σ,ρe(1,1,s) chain_a _σ,ρ^e(1,1,s) would give the agent e as indeterminate when s∈[5,∞)s∈[5,∞), and ⊥ at s=∞s=∞. As we saw, the semantics is not continuous: we cannot recover the semantics for s=+∞s=+∞ as the limit of a sequence of values of the semantics for finite values of the space horizon. However, it is monotone in the space horizon: Lemma 1 For all agent formula φ , monotone context ρ, timed graph σ, t∈ℝ≥0t _≥ 0, h∈ℝh , s≤s′∈ℝ¯s≤ s ∈ R, and a∈a : ⟦φ⟧σ,ρe(t,h,s,a)⪯⟦φ⟧σ,ρe(t,h,s′,a) _σ,ρ^e(t,h,s,a) _σ,ρ^e(t,h,s ,a) where ⪯ is the information partial order ⊤⊥⪯⊤,⊥ to0.0pt$ $ , and a context is monotone if for all fixpoint variable X ρ(X)ρ(X) is monotone in the space horizon as above. The value at infinity, which means that we do not put any restriction on the space horizon we can see, actually correspond to the vanilla semantics of μ-TGL: Lemma 2 For formula φ of μ-TGL, monotone context ρ, signal σ, t,h∈ℝ+t,h _+: ⟦φ⟧ρ(σ,t,h)=⟦φ⟧ρe(σ,t,h,∞) _ρ(σ,t,h)= _ρ^e(σ,t,h,∞) Example 5(Causal Reach and Escape) The Reach and Escape modalities are fundamental components of the STREL logic, showing their importance in spatio-temporal analysis. These operators allow the verification of connectivity and propagation of an agent network at a fixed time. For any propositions φ1 _1 and φ2 _2, Reach modality, denoted as φ1ℛsφ2 _1R_s _2, asserts the existence of a communication chain connecting a source and a destination with constrains on the chain’s agents and total weight. Formally, the property holds if there exists a communication chain ag1→d1ag2⋯→dn−1agnag_1 d_1ag_2·s d_n-1ag_n where φ1 _1 holds for all intermediate agents in the chain ag≤n−1ag_≤ n-1 and φ2 _2 is true at the final agent agnag_n and such that (∑i∈[0,n−1]di)≤s( _i∈[0,n-1]d_i)≤ s. In μ-TGL, it can be written as: φ1ℛsφ2=∃a.a≤∙sμX.(φ2∨(φ1∧◇≤sX)) _1R_s _2=∃ a.\>a≤ _s\>μ X.( _2 ( _1 _≤ s\;\,X)) Observe that we introduce the modality ϕ≤ϕ′φ≤φ , which is already defined in standard μ-TGL. It compares the values of each agents at ϕφ and ϕ′φ using the pointwise order. We use it the same way in our extension: ⟦φ≤φ′⟧σ,ρe(t,h,s)=⋀a∈A(⟦φ⟧σ,ρe(t,h,s,a)→⟦φ′⟧σ,ρe(t,h,s,a)) ≤ _σ,ρ^e(t,h,s)= _a∈ A ( _σ,ρ^e(t,h,s,a)→ _σ,ρ^e(t,h,s,a) ) Escape property is written ℰφE and checks if the property φ can be propagated enough in space. Formally, it means that there exists a destination agent agag where a communication chain in which φ holds can be created. In μ-TGL: ℰsφ=∃b.a≤(μX.(φ∧(b∨◇≤sX))∧¬(∙sμX.(b∨◇≤sX)))E_s =∃ b.\;a≤(μ X.( (b _≤ s\;\,X)) ( _s\;μ X.(b _≤ s\;\,X))) However, those standard formulations do not take into account the temporal dimension of message transmission. The extension proposed offers this possibility leading to these new formalization of reachability and escape: φ1ℛsφ2=a≤∙mHtμX.(φ2∨(φ1∧F[0,t]◇≤mX)) _1R_s _2=a≤ _m\;H_t\;μ X.( _2 ( _1 F_[0,t]\, _≤ m\;\,X)) ℰsφ=∃b.a≤(HtμX.(φ∧(b∨F[0,t]◇X))∧¬(Ht∙mμX.(b∨F[0,t]◇≤mX)))E_s =∃ b.\;a≤(H_t\;μ X.( (b F_[0,t]\, \,X)) (H_t _m\;μ X.(b F_[0,t]\, _≤ m\;\,X))) Corollary 1 Extended μ is strictly more expressive than μ-TGL. 4 Computing the Extended Semantics Computing the semantics of modal logics is always tricky because we may need infinite amount of information to be able to compute a local part of the semantics. For temporal logics, this translates in the following: to compute the semantics at a given time, we may need the semantics of subformulas for a unbounded amount of time. This can be overcome by ensuring that the intervals in the modalities are bounded. The fixpoint operator of μ-TGL brings additional complications: even if the intervals are bounded, the fixpoint may not converge in a finite number of iterations (which is a problem in itself) and we may have to apply the modality arbitrary many times, and so, we may need unbounded amount of information again. To overcome this problem, the monitoring algorithm of μ-TGL is only dealing with formulas that only need a finite horizon of time, meaning that any fixpoint which contains a FTF_T\, modality, must be guarded by a time horizon modality HhH_h. When the timed graph is assumed piecewise-constant with finitely many changes of values within a time window bounded by this horizon, we can then compute the semantics, and in particular, the fixpoints terminate after finitely many iterations. Concretely, after computing this horizon hϕh_φ, what is computed is a restriction of the semantics, namely ⟦φ⟧σ,ρ:ℝ≥0×[0,hϕ]×→3 _σ,ρ\> \>R_≥ 0×[0,h_φ]×A 3. In our extension, we would like something similar, however, we do not want to make additional restrictions on the set of formulas we can monitor: asking that fixpoint are guarded by space-horizon modalities means we could not monitor formulas from vanilla μ-TGL, seen as formulas of this extensions. It turns out such restrictions are not needed: 1) either we are under the scope of a space-horizon, in which case we can bound the amount of information we need, similarly to the time horizon 2) or we are not, and what we need is the value at infinity, which can be computed similarly to the semantics of vanilla μ-TGL. 4.1 Bounding the Information To make this statement concrete, we introduce a new semantics, which defines the needed (bounded) information of the semantics by induction: Definition 3(Concrete Semantics) Fix φ and define sϕs_φ to be the maximal s∈ℝ≥0s _≥ 0 seen as ∙s _s in φ . We define the concrete semantics as a function of type: ⟦φ⟧σ,ρc:ℝ≥0×[0,hϕ]×([0,sφ]∪+∞)×→3 _σ,ρ^c\, \,R_≥ 0×[0,h_φ]× ([0,s_ ]∪\+∞\ )×A 3 by induction on the formula φ , using the same definition as for ⟦φ⟧σ,ρe _σ,ρ^e, except that least fixpoints and context ρ(X)ρ(X) are over functions of type ℝ≥0×[0,hϕ]×([0,sφ]∪+∞)×→3R_≥ 0×[0,h_φ]× ([0,s_ ]∪\+∞\ )×A 3. Lemma 3 For every context ρ with ρ(X):ℝ≥0×ℝ×ℝ¯×→3ρ(X)\, \,R_≥ 0×R× R×A 3, we have: ⟦φ⟧σ,ρ¯c=⟦φ⟧σ,ρe¯ _σ, ρ^c= _σ,ρ^e where f¯ f is the restriction to ℝ≥0×[0,hϕ]×([0,sφ]∪+∞)×→3R_≥ 0×[0,h_φ]× ([0,s_ ]∪\+∞\ )×A 3 of a function or a context. The intuition of this lemma is that computing the whole semantics and then restricting to the part we really need is the same as doing the computation with restricting all the intermediate results to the part we need. This means that one can always bound the amount of information that is needed to compute the needed part of the semantics. 4.2 Data Structure Still, bounded information does not mean that the computation – particularly the fixpoints – will terminate. For simplicity, and as it is usually done for monitoring algorithms of temporal logics, we will assume that the timed graph is given by samples at runtime, and that the timed graph is constant between two samples. This introduces imprecisions in the analysis, but remains a reasonable assumption if the signal is sufficiently sampled and the dynamics not too wild. In this context (and modulo some mild non-Zeno conditions) we will prove that computing samples of the semantics terminates, and that we can then perform monitoring. Concretely, the monitoring algorithm works with timed graphs represented by a sequence of samples of the form x=((t0,σ0),…,(tn,σn),…)x=((t_0, _0),…,(t_n, _n),…), where t0<t1<…t_0<t_1<… is an increasing sequence of ℝ≥0R_≥ 0 and where σi _i is a weighted graph whose vertices are agents A which denotes the state of the timed graphs at times [ti,ti+1)[t_i,t_i+1). Accordingly, we process the signal using the piecewise constant functions defined by σ(t,a,b)=σi(a,b)σ(t,a,b)= _i(a,b) if t∈[ti,ti+1)t∈[t_i,t_i+1). We assume that the sequence (tn)n∈ℕ(t_n)_n does not converge to a finite value. This implies that 1) the sequence diverges to infinity and 2) in any given bounded interval of ℝ≥0R_≥ 0, there will be only a finite number of tnt_n. This data structure is used both for the input timed graph, but also for the semantics to be computed. Indeed, the semantics depends on three real values: the time t, the time horizon h, and the space horizon s. That is, up to currying, the semantics is of type: ⟦φ⟧σ,ρe:ℝ≥0→ℝ→ℝ¯→3. _σ,ρ^e\> \>R_≥ 0 → R 3. Therefore, the result will be a signal of signals of signals of uncertain sets of the form: for i,j,k∈ℕi,j,k , w=(ti,(hi,j,(si,j,k,Useti,j,k)))w=\\;(t_i,\\;(h_i,j,\\;(s_i,j,k,Uset_i,j,k)\;\)\;\)\;\. We call such a data structure a discrete signal. The last model to represent is the uncertain sets: using the same data structure as [9], the uncertain sets Uset : A→3A→ 3 are represented by a pair [U,V](U,V∈(A))[U,V]\;(U,V (A)) such that [U,V](a)=⊤ if a∈U⊤⊥ if a∉U∧a∈V⊥ if a∉V[U,V](a)= \ array[]l & if a∈ U\\ to0.0pt$ $ & if a∉ U a∈ V\\ & if a∉ V\\ array . Finally, given such a data structure, we obtain a continuous-time function: w¯(t,h,s,a)=⊤ if a∈Ui,j,k⊤⊥ if a∉Ui,j,k∧a∈Vi,j,k⊥ if a∉Vi,j,k w(t,h,s,a)= \ array[]l & if a∈ U_i,j,k\\ to0.0pt$ $ & if a∉ U_i,j,k a∈ V_i,j,k\\ & if a∉ V_i,j,k\\ array . whenever ti≤t<ti+1, hi,j≤h−(t−ti)<hi,j+1 and si,j,k≤s<si,j,k+1t_i≤ t<t_i+1, h_i,j≤ h-(t-t_i)<h_i,j+1 and s_i,j,k≤ s<s_i,j,k+1. 4.3 Termination of the Computation What remains to be done is to prove that the computation of the semantics for a bounded amount of time T, that is, the function ⟦φ⟧σ,ρc _σ,ρ^c restricted to [0,T]×[0,hφ]×([0,sφ]∪+∞)×[0,T]×[0,h_ ]× ([0,s_ ]∪\+∞\ )×A can be computed. In particular, this requires to prove that all the fixpoints involved in the computation terminate in a finite number of iterations. To prove this, we construct finite sets T, ℋH, and S of reals, that only depend on σ(t′,−,−)σ(t ,-,-) with t′∈[0,T+hϕ]t ∈[0,T+h_φ] and φ . We would then prove by induction that the computation terminates and that there is a discrete signal w=(t,(h,(s,Usett,h,s)))w=\\;(t,\\;(h,\\;(s,Uset_t,h,s)\;\)\;\)\;\ (1) such that ⟦φ⟧σ,ρc=w¯ _σ,ρ^c= w, t∈t , h∈ℋh , and s∈s . Now, fix T. By assumption, there is a finite number of 0=t0,…,tn0=t_0,…,t_n in [0,T+hϕ][0,T+h_φ]. We build T, ℋH, and S as follows. They are the smallest sets satisfying: • 1) ti∈t_i , for i≤ni≤ n and 2) if t∈t , then t+at+a, t+b∈t+b , for every [a,b][a,b] appearing in F[a,b]F_[a,b]\, • 1) 0∈ℋ0 , 2) hϕ∈ℋh_φ , 3) h∈ℋh for every h appearing as HhH_h, and 4) if h∈ℋh , then h−ah-a, h−b∈ℋh-b , for every [a,b][a,b] appearing in F[a,b]F_[a,b]\, • 1) 0∈0 , 2) s∈s for every s appearing as ∙s _s 3) b∈b for every b appearing as ◇[a,b] _[a,b], and 4) for i≤ni≤ n, a,b∈a,b , and s∈s , then s−σ(ti,a,b)∈s-σ(t_i,a,b) . intersected by [0,T+hφ][0,T+h_ ], [0,hφ][0,h_ ], and [0,sφ][0,s_ ] respectively. Finally, we add +∞+∞ to S. Those sets are finite as basically finite unions of finitely generated sub-monoids of (ℝ,+)(R,+) intersected with bounded intervals. Lemma 4 For every subformula ψ of ϕφ and every context ρ where every ρ(X)ρ(X) is obtained as w¯ w for some w as in (1), then ⟦ψ⟧σ,ρc ψ _σ,ρ^c is also such a function. Furthermore, if ψ≡μX.ψ′ψ≡μ X.ψ , then the fixpoint defining its semantics terminates. 4.4 Computing semantics As in [9], in order to manipulate the data structure, we need to implement a way to zip two signals together, that is construct a procedure ZipZip that takes two signals x and y, and produces a composite signal x×yx× y satisfying: x×y¯(t)=(x¯(t),y¯(t)). x× y(t)=( x(t), y(t)). In particular, the union of two signals requires zipping corresponding each layer of signals of the semantic, and then merging the associated uncertain sets: [Ui,j,kx,Vi,j,kx],[Ui,j,ky,Vi,j,ky][U^x_i,j,k,V^x_i,j,k],[U^y_i,j,k,V^y_i,j,k] to get [Ui,j,kx∪Ui,j,ky,Vi,j,kx∪Vi,j,ky][U^x_i,j,k∪ U^y_i,j,k,V^x_i,j,k∪ V^y_i,j,k]. For most operators, the semantic computing is not too different from the constructions in [9]. One operator interesting to explain is the diamond. The semantics of the diamond operator ◇Dφ _D\, is computed according to Algorithm 1. For each tit_i and hi,jh_i,j constituting the semantic wφw_ of φ , we construct subsets wa,bw_a,b of the final semantics, parameterized by each weight d=σ(ti,a,b)d=σ(t_i,a,b). If d∉Dd∉ D, the value wa,b(ti,hi,j,0,b)w_a,b(t_i,h_i,j,0,b) will be ⊤⊥ to0.0pt$ $ (l.6, left). It remains unchanged until the space horizon reaches min(d,max(D)) (d, (D)), at which point the values for agent b is confirmed to be ⊥ (l.6, right). If d∈Dd∈ D, we initialize wa,b(ti,hi,j,0,b)w_a,b(t_i,h_i,j,0,b) at ⊤⊥ to0.0pt$ $ (l.8). The semantics at space horizon s depends on the value of wφ(ti,ti,j,s−d)w_ (t_i,t_i,j,s-d). By leveraging the monotonicity of space horizon, it suffices to find the first space horizon value in which agent b becomes determinized to compute its semantics (l.9–14). If the agent remains indeterminate, we only add the ⊤⊥ to0.0pt$ $ value at space horizon +∞+∞ (l.16). The result is obtained by zipping and unifying (l.17). Algorithm 1 Diamond semantic 1:a formula ◇[d1,d2]φ _[d_1,d_2]\, , a signal σ 2:semantic ⟦◇[d1,d2]φ⟧ρ(σ,t,h,s) _[d_1,d_2]\, _ρ(σ,t,h,s) for all t,h,st,h,s 3:resres ← empty semantic; semφ←sem_ ← semantic of φ 4:for all t,h in the data structure of semφsem_ do 5: for all edge a→ba db do 6: tmp←⊥tmp← 7: if d∉[d1,d2]d ∈[d_1,d_2] then 8: tmp(t,h,0)←[∅,b]tmp(t,h,0)←[ ,\b\]; tmp(t,h,min(d,d2))←[∅,∅]tmp(t,h, (d,d_2))←[ , ] 9: if d∈[d1,d2]d∈[d_1,d_2] then 10: tmp (t,h,0)←[∅,b]tmp (t,h,0)←[ ,\b\] 11: if ∃s,a∈semφ(t,h,s)[U]∃ s,a∈ sem_ (t,h,s)[U] then 12: smin←mins,a∈semφ(t,h,s)[U]s_min← \;\s,a∈ sem_ (t,h,s)[U]\ 13: tmp(t,h,smin+d)←[b,b]tmp(t,h,s_min+d)←[\b\,\b\]; tmp(t,h,+∞)←[b,b]tmp(t,h,+∞)←[\b\,\b\] 14: else if ∃s,a∉semφ(t,h,s)[V]∃ s,a∉ sem_ (t,h,s)[V] then 15: smin←mins,a∉semφ(t,h,s)[V]s_min← \;\s,a∉ sem_ (t,h,s)[V]\ 16: tmp(t,h,smin+d)←[∅,∅]tmp(t,h,s_min+d)←[ , ]; tmp(t,h,+∞)←[∅,∅]tmp(t,h,+∞)←[ , ] 17: else 18: (tmp(t,h,+∞)←[∅,b](tmp(t,h,+∞)←[ ,\b\] 19: res(t,h)=Union(Zip(res(t,h),tmp))res(t,h)=Union(Zip(res(t,h),tmp)) 5 Case Study To illustrate the feasibility of our monitoring algorithm, we analyze specifications related to bounding the causal communication graph of a collection of agents collaborating to visit specified positions in a 2D-area. To dynamically allocate which agent should visit which position, they execute a Consensus-Based Bundle Algorithm (CBBA) as in [7]. Roughly, every connected component of the communication graph (or bundle) run a bidding protocol where each agent bids on specific positions, depending on how difficult or far it is for them to reach the position. After some rounds of communications, the agent with the best bid on a particular position can start going towards this position to visit it. Crucially, the number of rounds of communications needed for a bundle to reach a consensus depends on the diameter of the communication graph. This is then a suitable problem for monitoring that the diameter of the causal communication graph be bounded to ensure the protocol runs efficiently. 5.1 Simulation and Monitoring Framework To obtain traces of simulation on which to run our monitoring algorithm, we will rely on the simulator [12], based on [11], and implementing the CBBA protocol of [7] in Python. In this simulation framework, we can choose the number of agents, the number of positions to visit, the size of the area, and the communication radius, and the various positions are then drawn randomly. It is then easy to extract the position of each agent during the simulation, compiled in a CSV file. The code of our monitoring algorithm, together with some experiment setups to interact with the simulator is available on github [4]. Our code is in Ocaml 5.3.0, compiled with Dune, and ran on a Apple M4 Pro with 24GB RAM. 5.2 Monitoring the Diameter of the Causal Communication Graph We ran the simulator with the following parameters: 10 agents, visiting 100 positions, in a 1400×10001400× 1000 area, with a 500500 communication radius (the specific unit does not matter). This produced a trace with ∼12 \!12K time steps. Figure 2: Bounds on the diameter (left) and the communication chains (right) of the causal communication graph over time. On this specific trace, we monitored a specification describing that the causal communication graph within 10 time units has a diameter bounded by a constant d, namely: ∀a.⊤≤∙dH10μX.(a∨F≤10◇≤1X),∀ a.\, ≤ _d\,H_10\,μ X.\, (a F_≤ 10\,\, _≤ 1\,\,X ), (2) very similar to the causal reach specification of Example 5. We ran the monitoring algorithm for all possible values of d=1,…,9d=\1,...,9\, for an average of 267267s per run (or 0.0220.022s per time step), without significant difference in time between runs. This allows to draw the Figure 2 (left), showing the connectivity of the causal communication graph. For example, this shows that it is fully connected only on [988,1830]∪[3786,7137]∪[7186,7385]∪[10114,12243][988,1830]∪[3786,7137]∪[7186,7385]∪[10114,12243], in which case the diameter is at most 66. The diameter goes down to 22 on [5210,5498]∪[5686,6201][5210,5498]∪[5686,6201], but never down to 11, meaning it is never a clique. Another interesting property to monitor is to bound the chains of communications of agents that have at least one chain of communication to an agent a, namely ∀a.H10μX.(a∨F≤10◇≤1X)≤∙dH10μX.(a∨F≤10◇≤1X),∀ a.\,H_10\,μ X.\, (a F_≤ 10\,\, _≤ 1\,\,X )≤ _d\,H_10\,μ X.\, (a F_≤ 10\,\, _≤ 1\,\,X ), (3) This specification is slightly stronger than the fact that each bundle is bounded. The Figure 2 (right) gives more information as for when the graph is not fully connected: we recover some information on bounds of communication chains. Observe that, for simplicity, we monitored one specification for each value of the bound, and in both cases of (2) and (3), while all the necessary information is already available in the computation of the semantics of the formulas ∙9H10μX.(a∨F≤10◇≤1X) _9\,H_10\,μ X.\, (a F_≤ 10\,\, _≤ 1\,\,X ), for every agent a. 5.3 Scalabity w.r.t. the Number of Agents We ran our monitoring algorithm on traces where the parameters are: the number of agents n is in [3,5,10,20,30,40,50][3,5,10,20,30,40,50], the number of positions is m=3nm=3n, the area is 500×500500× 500, and the communication radius is 100100. Figure 3: Length of traces and statistics on normalized times of computation (actual time divided by the trace length). This set up allowed us to have traces of similar lengths, even with different number of agents, so that we can focus on the scalability w.r.t. this number. We monitored the specification: ⊤≤∙n/2H10μX.(a∨F≤10◇≤1X), ≤ _n/2\,H_10\,μ X.\, (a F_≤ 10\,\, _≤ 1\,\,X ), (4) that is, we only check that the causal communication chains towards one specific agent a has a length bounded by n/2n/2. To recover the specification (2), we would have to check this for every agent, adding roughly a linear factor in the number of agents. This specification is relevant as it would be enough in a decentralized monitoring algorithm, and is more realistic in the sense that this would not require a central agent to know the whole situation of the communication, while each agent can monitor the specification (4) based only on the communication it receives. We ran 5050 times for each number of agents, and compile the results in Figure 3. In this setup, the traces are ∼2K \!2K time step long. The monitoring scales nicely up to 30 agents: it takes an average of 1717ms per time step. For 50 agents, the monitoring of the specification (4) already takes 142142ms per time step in average. This is fine for physical systems with low velocity, for which we would not need to monitor the specification at high frequency, while the additional factor necessary to monitor the specification (2) would make it impractical. 6 Conclusion We have provided an offline monitoring algorithm with allows to monitor information about the diameter of causal communication graphs, which was not possible with previous spatio-temporal logics. The next step is to make this algorithm online, which will be allowed by the careful semantics crafted in the present paper. To do so, we would like however to integrate it in a more general framework, and particularly in a control loop, as a shielding. To go further in that direction, we would like to develop a quantitative semantics of μ-TGL, allowing to better discriminate control prediction and help the control synthesis. Acknowledgements This work is partially supported by the Agence de l’Innovation de Défense (AID) via the Centre Interdisciplinaire Mers et Océan (CIMO) project 2025 CHRoMM. J.D. is partially funded by the Academic and Research Chaire “Architecture des Systèmes Complexes” Dassault Aviation, Naval Group, Dassault Systèmes, KNDS France, Agence de l’Innovation de Défense, Institut Polytechnique de Paris. References [1] M. Alshiekh, R. Bloem, R. Ehlers, B. Könighofer, S. Niekum, and U. Topcu (2018) Safe reinforcement learning via shielding. In Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence and Thirtieth Innovative Applications of Artificial Intelligence Conference and Eighth AAAI Symposium on Educational Advances in Artificial Intelligence, ACM (Ed.), Cited by: §1. [2] R. Alur, T. A. Henzinger, and O. Kupferman (2002) Alternating-time temporal logic. Journal of the ACM 49 (5). Cited by: §1. [3] R. Alur and T. A. Henzinger (1994) A theory of timed automata. Theoretical Computer Science 126 (2), p. 183–235. Cited by: §1. [4] L. Bakiri, J. Dubut, and S. Mover (2026) ExtMuTgl-monitoring. Note: https://github.com/Lydia-bak/ExtMuTgl-MonitoringGitHub repository, accessed 2026-06-14 Cited by: §5.1. [5] M. Bergmann (2012) An Introduction to Many-Valued and Fuzzy Logic: Semantics, Algebras, and Derivation Systems. Cambridge University Press. Cited by: §1. [6] C. H. Caicedo-Nunez and M. Zefran (2008) Consensus-based rendezvous. In Proceedings of 2008 the IEEE International Conference on Control Applications, Cited by: §1. [7] H. Choi, L. Brunet, and J. P. How (2009) Consensus-based decentralized auctions for robust task allocation. IEEE Transactions on Robotics 25 (4), p. 912–926. Cited by: §1, §5.1, §5. [8] P. Cousot and R. Cousot (1979) Constructive versions of Tarski’s fixed point theorems. Pacific Journal of Mathematics 81 (1), p. 43–57. Cited by: §2. [9] C. Eberhart, J. Haydon, J. Dubut, A. Cetinkaya, and S. Pruekprasert (2022) Logic for timed agent network topologies. In 61st IEEE Conference on Decision and Control, CDC 2022, Cancun, Mexico, December 6-9, 2022, p. 2870–2877. External Links: Link, Document Cited by: §1, §1, §4.2, §4.4. [10] I. Haghighi, A. Jones, Z. Kong, E. Bartocci, R. Gros, and C. Belta (2015) 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, ACM (Ed.), Cited by: §1. [11] I. Jang (2024) SPACE: a python-based simulator for evaluating decentralized multi-robot task allocation algorithms. arXiv preprint arXiv:2409.04230. Cited by: §5.1. [12] I. Jang (2026) SPACE. Note: https://github.com/inmo-jang/space-simulatorGitHub repository, accessed 2026-06-12 Cited by: §5.1. [13] D. Kozen (1983) Results on the propositional μ-calculus. Theoretical Computer Science 27 (3), p. 333–354. Cited by: §1. [14] H. J. LeBlanc, H. Zhang, X. Koutsoukos, and S. Sundaram (2013) Resilient Asymptotic Consensus in Robust Networks. IEEE Journal on Selected Areas in Communications 31 (4), p. 766–781. Cited by: §1. [15] M. W. Maier (1998) Architecting principles for systems-of-systems. Systems Engineering 1 (4), p. 267–284. Cited by: §1. [16] L. Nenzi, L. Bortolussi, V. Ciancia, M. Loreti, and M. Massink (2018) Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL. Logical Methods in Computer Science 14 (4). Cited by: §1. [17] L. Nenzi, E. Bartocci, L. Bortolussi, and M. Loreti (2022) A logic for monitoring dynamic networks of spatially-distributed cyber-physical systems. Logical Methods in Computer Science 18 (1), p. 4:1–4:30. Cited by: §1, §1, §2, §3. [18] L. Nenzi, E. Bartocci, L. Bortolussi, S. Silveti, and M. Loreti (2020) MoonLight: a lightweight tool for monitoring spatio-temporal properties. International Journal on Software Tools for Technology Transfer 25, p. 503–517. Cited by: §1, §1. [19] M. Pease, R. Shostak, and L. Lamport (1980) Reaching Agreement in the Presence of Faults. Journal of the ACM 27 (2), p. 228–234. Cited by: §1. [20] T. S. Rappaport (2002) Wireless communications: principles and practice. 2 edition, Prentice Hall. Cited by: §2. [21] Y. E. Sahin, P. Nilsson, and N. Ozay (2020) Multirobot Coordination With Counting Temporal Logics. IEEE Transactions on Robotics 36 (4). Cited by: §1. [22] D. Seto, B. Krogh, and A. Chutinan (1998) The Simplex architecture for safe online control system upgrades. In Proceedings of the 1998 American Control Conference, IEEE (Ed.), Cited by: §1. [23] R. Tulcan, R. Bohrer, Y. Montacute, K. Zhou, Y. Kawamoto, and I. Hasuo (2026) Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking. Note: arXiv:2603.24443 Cited by: §1. Appendix 0.A Full Semantics of Our Extension ⟦⊤⟧ρe(σ,t,h,s) _ρ^e(σ,t,h,s) =⊤ = ⟦p⟧ρ(σ,t,h,s) p _ρ(σ,t,h,s) =⋁b∈A(p(σ(a,t)) if h≥0⊤⊥ otherwise = \ array[]l _b∈ A (p(σ(a,t))& if h≥ 0\\ to0.0pt$ $ & otherwise array . ⟦¬φ⟧ρe(σ,t,h,s) _ρ^e(σ,t,h,s) =¬⟦φ⟧ρ(σ,t,h,s) = _ρ(σ,t,h,s) ⟦φ∧ψ⟧ρe(σ,t,h,s) ψ _ρ^e(σ,t,h,s) =⟦φ⟧ρ(σ,t,h,s)∧⟦ψ⟧ρ(σ,t,h,s) = _ρ(σ,t,h,s) ψ _ρ(σ,t,h,s) ⟦a⟧ρe(σ,t,h,s) a _ρ^e(σ,t,h,s) =ρ(a) =\ρ(a)\ ⟦◇Dφ⟧ρe(σ,t,h,s)(a,b) _D\,\> _ρ^e(σ,t,h,s)(a,b) =⊤ if d(σ(a,t),σ(b,t))∈D∧d(σ(a,t),σ(b,t))≤s∧⟦φ⟧ρe(σ,t,h,s−d(σ(a,t),σ(b,t)))(b)=⊤⊥ if d(σ(a,t),σ(b,t))>s∧max(D)>p∨p≥d(σ(a,t),σ(b,t))∧⟦φ⟧ρe(σ,t,h,s−d(σ(a,t),σ(b,t)))(b)=⊤⊥ if p≥max(D)∧d(σ(a,t),σ(b,t))>max(D)∨(p≥min(D)∧max≥d(σ(a,t),σ(b,t))∧⟦φ⟧ρe(σ,t,h,s−d(σ(a,t),σ(b,t)))(b)=⊤) = \ array[]l & if d(σ(a,t),σ(b,t))∈ D\\ & \;d(σ(a,t),σ(b,t))≤ s\\ & \; _ρ^e(σ,t,h,s-d(σ(a,t),σ(b,t)))(b)= \\ &\\ to0.0pt$ $ & if d(σ(a,t),σ(b,t))>s (D)>p\\ & p≥ d(σ(a,t),σ(b,t)) _ρ^e(σ,t,h,s-d(σ(a,t),σ(b,t)))(b)= to0.0pt$ $ \\ &\\ & if p≥ (D) d(σ(a,t),σ(b,t))> (D)\\ & (p≥ (D) ≥ d(σ(a,t),σ(b,t))\\ &\;\;\;\; _ρ^e(σ,t,h,s-d(σ(a,t),σ(b,t)))(b)= ) array . ⟦◇Dφ⟧ρe(σ,t,h,s)(a) _D\,\> _ρ^e(σ,t,h,s)(a) =⋁b∈A⟦◇Dφ⟧ρe(σ,t,h,s)(a,b) = _b∈ A _D\,\> _ρ^e(σ,t,h,s)(a,b) ⟦FTφ⟧ρe(σ,t,h,s)(a) F_T\,\> _ρ^e(σ,t,h,s)(a) =⋁t′∈T⟦φ⟧ρ(σ,t+t′,h−t′,s) = _t ∈ T _ρ(σ,t+t ,h-t ,s) ⟦∃a.φ⟧ρe(σ,t,h,s) ∃ a.\> _ρ^e(σ,t,h,s) =⋁b∈A⟦φ⟧ρ[a→b](σ,t,h,s) = _b∈ A _ρ[a→ b](σ,t,h,s) ⟦Hh′φ⟧ρe(σ,t,h,s) H_h \> _ρ^e(σ,t,h,s) =⊥ if ⟦φ⟧ρ(σ,t,h′,s)=⊤⊥ and h≥h′⟦φ⟧ρ(σ,t,min(h,h′),s) otherwise = \ array[]l & if _ρ(σ,t,h ,s)= to0.0pt$ $ and h≥ h \\ _ρ(σ,t, (h,h ),s)& otherwise array . ⟦∙s′φ⟧ρe(σ,t,h,s) _s \> _ρ^e(σ,t,h,s) =⟦φ⟧ρe(σ,t,h,min(s,s′)) = _ρ^e(σ,t,h, (s,s )) ⟦X⟧ρe(σ,t,h,s) X _ρ^e(σ,t,h,s) =ρ(X)(t,h,s) =ρ(X)(t,h,s) ⟦μX.φ⟧ρe(σ,t,h,s) μ X.\> _ρ^e(σ,t,h,s) =lfp(f↦⟦φ⟧ρ[X→f]e(σ,−,−,−))(t,h,s) if s<∞lfp(f↦⟦φ⟧ρ[X→f](σ,−,−))(t,h) if s=∞ = \ array[]llfp(f _ρ[X→ f]^e(σ,-,-,-))(t,h,s)& if s<∞\\ lfp(f _ρ[X→ f](σ,-,-))(t,h)& if s=∞ array . ⟦φ≤ψ⟧ρe(σ,t,h,s) ≤ψ _ρ^e(σ,t,h,s) =⋀a∈A(⟦φ⟧ρ(σ,t,h,s)(a)→⟦ψ⟧ρ(σ,t,h,s)(a)) = _a∈ A( _ρ(σ,t,h,s)(a)→ ψ _ρ(σ,t,h,s)(a)) ⟦φ1ℛDTφ2⟧ρe(σ,t,h,s) _1\,R^T_D\, _2 _ρ^e(σ,t,h,s) =lfp(f↦⟦φ2∨(φ1∧FT◇DX)⟧ρ[X→f]e(σ,−,−,−))(t,h,s) =lfp(f _2 ( _1 F_T\, _D\,X) _ρ[X→ f]^e(σ,-,-,-))(t,h,s) ⟦φ1ℰDTφ2⟧ρe(σ,t,h,s) _1\,E^T_D\, _2 _ρ^e(σ,t,h,s) =lfp(f↦⟦…⟧ρ[X→f]e(σ,−,−,−))(t,h,s) =lfp(f ... _ρ[X→ f]^e(σ,-,-,-))(t,h,s) Appendix 0.B Omitted Proofs Proof(of Lemma 1) We prove the stated lemma by induction on φ : Base cases: • if φ=X =X is a fixpoint variable, the result holds because the context is monotone, • for other base cases, the semantics function is constant in the space horizon. Induction step: Let φ be a formula and assume the lemma is true for φ . This means that for all ρ,σ,t,h,s1,s2,aρ,σ,t,h,s_1,s_2,a with s1≤s2s_1≤ s_2, we have ⟦φ⟧σ,ρe(t,h,s1,a)⪯⟦φ⟧ρe(σ,t,h,s2) _σ,ρ^e(t,h,s_1,a) _ρ^e(σ,t,h,s_2) • ∧,∨,¬,∃,H,∙ , , ,∃,H, preserves ⪯ -monotonicity trivially • FTφF_T\, : case disjunction on the value of FTφF_T\, : – if ⟦FTφ⟧σ,ρe(t,h,s1,a)=⊤⊥ F_T\, _σ,ρ^e(t,h,s_1,a)= to0.0pt$ $ : trivial – ⟦FTφ⟧σ,ρe(t,h,s1,a)=⊤⟹∃t′∈T⟦φ⟧σ,ρe(t+t′,h−t′,s1,a)=⊤ F_T\, _σ,ρ^e(t,h,s_1,a)= \\ ∃ t ∈ T\> _σ,ρ^e(t+t ,h-t ,s_1,a)= . By induction hypothesis, ⟦φ⟧σ,ρe(t+t′,h−t′,s2,a)=⊤ _σ,ρ^e(t+t ,h-t ,s_2,a)= . Therefore: ⟦FTφ⟧σ,ρe(t,h,s2,a)=⊤ F_T\, _σ,ρ^e(t,h,s_2,a)= – ⟦FTφ⟧σ,ρe(t,h,s1,a)=⊥⟹∀t′∈T⟦φ⟧σ,ρe(t+t′,h−t′,s1,a)=⊥ F_T\, _σ,ρ^e(t,h,s_1,a)= \\ ∀ t ∈ T\> _σ,ρ^e(t+t ,h-t ,s_1,a)= . By induction hypothesis, ∀t′∈T⟦φ⟧σ,ρe(t+t′,h−t′,s2,a)=⊥∀ t ∈ T\> _σ,ρ^e(t+t ,h-t ,s_2,a)= . Therefore, ⟦FTφ⟧ρe(σ,t,h,s2)(a)=⊥ F_T\, _ρ^e(σ,t,h,s_2)(a)= • ◇Dφ(a) _D\, (a): case disjunction on the value of ◇Dφ(a) _D\, (a) for any a∈Aa∈ A: – if ⟦◇Dφ⟧ρe(σ,t,h,s1)(a)=⊤⊥ _D\, _ρ^e(σ,t,h,s_1)(a)= to0.0pt$ $ , trivial. – if ⟦◇Dφ⟧σ,ρe(t,h,s1,a)=⊤ _D\, _σ,ρ^e(t,h,s_1,a)= , then 1) h≥0h≥ 0 and there is b∈b such that 2) σ(t,a,b)∈Dσ(t,a,b)∈ D, 3) σ(t,a,b)≤s1σ(t,a,b)≤ s_1 and 4) ⟦φ⟧σ,ρe(t,h,s1−σ(t,a,b),b)=⊤ _σ,ρ^e(t,h,s_1-σ(t,a,b),b)= . Since s1≤s2s_1≤ s_2, 3) implies 3’) σ(t,a,b)≤s2σ(t,a,b)≤ s_2. The induction hypothesis together with 4) implies 4’) ⟦φ⟧σ,ρe(t,h,s2−σ(t,a,b),b)=⊤ _σ,ρ^e(t,h,s_2-σ(t,a,b),b)= . Altogether, 1+2+3’+4’ implies ⟦◇Dφ⟧σ,ρe(t,h,s2,a)=⊤ _D\, _σ,ρ^e(t,h,s_2,a)= – if ⟦◇Dφ⟧σ,ρe(t,h,s1,a)=⊥ _D\, _σ,ρ^e(t,h,s_1,a)= , then h≥0h≥ 0 and for all b∈Ab∈ A, one of the following statements holds: σ(t,a,b)>max(D)∧s1≥max(D) σ(t,a,b)> (D) s_1≥ (D) (5) s1≥σ(t,a,b)∧min(D)>σ(t,a,b) s_1≥σ(t,a,b) (D)>σ(t,a,b) (6) s1≥σ(t,a,b)∧max(D)∈D∧⟦φ⟧σ,ρe(t,h,s1−σ(t,a,b),b)=⊥ s_1≥σ(t,a,b) (D)∈ D _σ,ρ^e(t,h,s_1-σ(t,a,b),b)= (7) (1) and (2) keep the same value by substituting s1s_1 with s2s_2. By induction hypothesis, ⟦φ⟧σ,ρe(t,h,s2−σ(t,a,b),b)=⊥ _σ,ρ^e(t,h,s_2-σ(t,a,b),b)= , (3) keep the same value as well. • μX.φμ X. : By Cousot-Cousot theorem, we know that the least fixpoint is obtained by transfinite applications of the functional we are taking the least fixpoint of, starting with the constant function equal to ⊥ . To show that the least fixpoint is monotone in the space horizon, it is enough to show the following properties: – (base case) the constant function is monotone – (successor case) if f is function monotone in the space horizon, then ⟦φ⟧σ,ρ[X→f]e _σ,ρ[X→ f]^e is also monotone in the space horizon. This is just by induction hypothesis, with the fact that ρ[X→f]ρ[X→ f] is a monotone context. – (limit case) the supremum of a chain of functions monotone in the space horizon is monotone too. Here, we have to be careful, because the orders on 3 used for the supremum (⊥≤⊤⊥≤⊤ ≤ to0.0pt$ $ ≤ ) is not the same as the one used for the monotonicity (information order). Let (fi)i∈I(f_i)_i∈ I be a chain for the pointwise extension of ≤ where each fif_i is monotone in the space horizon for the information order, f its supremum and fix t,h,s1≤s2,at,h,s_1≤ s_2,a. Since (fi)i∈I(f_i)_i∈ I is a chain for the pointwise order, then (fi(t,h,s1,a))i∈I(f_i(t,h,s_1,a))_i∈ I and (fi(t,h,s2,a))i∈I(f_i(t,h,s_2,a))_i∈ I are chains for ≤. Since 3 is finite, those chains are ultimately constant, that is there are i1i_1 and i2i_2 such that for all i≥iji≥ i_j, fi(t,h,sj,a)=fij(t,h,sj,a)f_i(t,h,s_j,a)=f_i_j(t,h,s_j,a). Then, if i=maxi1,i2i= \i_1,i_2\, f(t,h,s1,a)=fi(t,h,s1,a)⪯fi(t,h,s2,a)=f(t,h,s2,a)f(t,h,s_1,a)=f_i(t,h,s_1,a) f_i(t,h,s_2,a)=f(t,h,s_2,a). ∎ Proof(of Lemma 2) We proceed by induction on the formula. The base cases are trivial, as the space horizon value has no effect on the value. For the inductive cases, we assume that the lemma holds for a formula φ . The non-trivial cases are the following: • ◇D _D\,: We do a case disjunction on the value of ◇[d1,d2]φ _[d_1,d_2]\, for agent a: – ⟦◇[d1,d2]φ⟧ρe(σ,t,h,∞)(a)=⊤⇔∃b∈Ad∈[d1,d2]∧⟦φ⟧ρe(σ,t,h,∞)(b)=⊤⇔∃b∈Ad∈[d1,d2]∧⟦φ⟧ρ(σ,t,h)(b)=⊤⇔⟦◇[d1,d2]φ⟧ρ(σ,t,h)(a)=⊤ _[d_1,d_2]\, _ρ^e(σ,t,h,∞)(a)= \\ ∃ b∈ A\>d∈[d_1,d_2] _ρ^e(σ,t,h,∞)(b)= \\ ∃ b∈ A\>d∈[d_1,d_2] _ρ(σ,t,h)(b)= \\ _[d_1,d_2]\, _ρ(σ,t,h)(a)= – ⟦◇[d1,d2]φ⟧ρe(σ,t,h,∞)=⊥⇔∀b∈Ad∈[d1,d2]∨⟦φ⟧ρe(σ,t,h,∞)(b)=⊥⇔∀b∈A:d∈[d1,d2]∨⟦φ⟧ρe(σ,t,h)(b)=⊥⇔⟦◇[d1,d2]φ⟧ρ(σ,t,h)(a)=⊥ _[d_1,d_2]\, _ρ^e(σ,t,h,∞)= \\ ∀ b∈ A\>d∈[d_1,d_2] _ρ^e(σ,t,h,∞)(b)= \\ ∀ b∈ A:d∈[d_1,d_2] _ρ^e(σ,t,h)(b)= \\ _[d_1,d_2]\, _ρ(σ,t,h)(a)= – if ⟦◇[d1,d2]φ⟧ρe(σ,t,h,∞)(a)=⊤⊥⇔∀b∈Ad∈[d1,d2]∧⟦φ⟧ρe(σ,t,h,∞)(b)=⊤⊥⇔∀b∈Ad∈[d1,d2]∧⟦φ⟧ρe(σ,t,h)(b)=⊤⊥⇔⟦◇[d1,d2]φ⟧ρ(σ,t,h)(a)=⊤⊥ _[d_1,d_2]\, _ρ^e(σ,t,h,∞)(a)= to0.0pt$ $ \\ ∀ b∈ A\>d∈[d_1,d_2] _ρ^e(σ,t,h,∞)(b)= to0.0pt$ $ \\ ∀ b∈ A\>d∈[d_1,d_2] _ρ^e(σ,t,h)(b)= to0.0pt$ $ \\ _[d_1,d_2]\, _ρ(σ,t,h)(a)= to0.0pt$ $ • μX.φμ X. : obvious since we use the pointwise order on functions. Proof(of Lemma 3) Once again, the proof proceeds by induction on the formula φ . The base cases are again trivial, as the space horizon parameter does not influence their value. For the inductive cases, we assume that the lemma is true for a subformula φ′ . For most operators, the inductive step is straightforward:the value at a given space horizon s is independent of the results at larger horizons. We detail less trivial cases below: • Space horizon modality ∙s _s: noticing that sϕs_φ is the maximal value that s can take makes the proof trivial. • Diamond modality is easy as well: – For any finite space horizon s∈[0,sϕ]s∈[0,s_φ], the valuation does not depend on any s′s greater than s. – For the infinite space horizon case s=+∞s=+∞, the result is determined by ⟦φ⟧σ,ρ¯c(t,h,+∞,a) _σ, ρ^c(t,h,+∞,a), which, by induction hypothesis, equals ⟦φ⟧σ,ρe¯(t,h,+∞,a) _σ,ρ^e(t,h,+∞,a). • The fixpoint construction is preserved under restriction. Indeed, it is sufficient to say that the restriction function is continuous, and, by induction hypothesis, it also commutes with the abstract semantic. The fixpoint is therefore preserved.∎ Proof(of Lemma 4) The statement about the fixpoint is obvious because there are only finitely many w as in (1). For the first statement, we reason by induction on ψ, and let’s do only the interesting cases. Assume ψ≡∙s′ψ′ψ≡ _s \>ψ . By induction hypothesis, ⟦ψ′⟧σ,ρc=w′¯ ψ _σ,ρ^c= w for some w′=(t,(h,(s,Usett,h,s′)))w =\\;(t,\\;(h,\\;(s,Uset_t,h,s )\;\)\;\)\;\ as in (1). We define w as follows. First observe that s′∈s by 2). For s<s′∈s<s and every t,ht,h, define Usett,h,s=Usett,h,s′Uset_t,h,s=Uset_t,h,s . Now, for every t,ht,h and every a∈a , since the semantics is monotone in the space horizon, either there is st,h,a∈s_t,h,a such that, for s<st,h,as<s_t,h,a, Usett,h,s′(a)=⊤⊥Uset_t,h,s (a)= to0.0pt$ $ and for s≥st,h,as≥ s_t,h,a, Usett,h,s′(a)≠⊤⊥Uset_t,h,s (a)≠ to0.0pt$ $ , or Usett,h,s′(a)=⊤⊥Uset_t,h,s (a)= to0.0pt$ $ for all s. With this in mind, define for s≥s′s≥ s the uncertain set Usett,h,sUset_t,h,s obtained from Usett,h,s′Uset_t,h,s by changing Usett,h,s′(a)Uset_t,h,s (a) to ⊥ if st,h,as_t,h,a does not exist, or if it exists and s<st,h,as<s_t,h,a. The case ϕ≡Hh′ψ′φ≡ H_h \>ψ is similar. Assume ψ≡◇Dψ′ψ≡ D\>ψ . It is enough to construct one discrete signal wbw^b as in (1) for each agent b to correspond to what we denoted ⟦◇Dψ′⟧σ,ρe(t,h,s,a,b) D\>ψ _σ,ρ^e(t,h,s,a,b) since taking the supremum of such discrete signals is also a discrete signal of the same shape. Now each of these wbw^b can be describe as a supremum (depending on the value ⊤ , ⊤⊥ to0.0pt$ $ , or ⊥ ) of a Boolean combinations of such discrete signals. For example, since σ(t,a,b)∈σ(t,a,b) by 1) and 4). for every t∈t such that σ(t,a,b)≥sϕσ(t,a,b)≥ s_φ, the condition σ(t,a,b)∈D∧σ(t,a,b)≤sσ(t,a,b)∈ D σ(t,a,b)≤ s can be seen as the discrete signal such that Usett,h,s(a)=⊤Uset_t,h,s(a)= if σ(t,a,b)≥sσ(t,a,b)≥ s and ⊥ otherwise. Similarly for σ(t,a,b)>sσ(t,a,b)>s and max(D)>s (D)>s (by 3). Now, the condition ⟦ψ′⟧σ,ρc(t,h,s−σ(t,a,b),b)=⊤ ψ _σ,ρ^c(t,h,s-σ(t,a,b),b)= is obtained from the discrete signal w′w by induction hypothesis on ψ′ψ , by setting Usett,h,s(a)=⊤Uset_t,h,s(a)= if Usett,h,s−σ(t,a,b)′(b)=⊤Uset _t,h,s-σ(t,a,b)(b)= , and ⊥ otherwise, observing that s−σ(t,a,b)∈s-σ(t,a,b) if s∈s by 4). Similarly for the ⊤⊥ to0.0pt$ $ case. The case for ψ=FTψ′ψ=F_T\,\>ψ is similar.∎