{'fraction_non_alphanumeric': 0.038399911597325816, 'fraction_numerical': 0.0073484722912868115, 'mean_word_length': 4.6943526820827435, 'pattern_counts': {'":': 0, '<': 2, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Quantified Differential Temporal Dynamic Logic for Verifying Properties of Distributed Hybrid Systems

We combine quantified differential dynamic logic (QdL) for reasoning about the possible behavior of distributed hybrid systems with temporal logic for reasoning about the temporal behavior during their operation. Our logic supports verification of temporal and non-temporal properties of distributed hybrid systems and provides a uniform treatment of discrete transitions, continuous evolution, and dynamic dimensionality-changes. For our combined logic, we generalize the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of QdL for distributed hybrid systems. On this basis, we provide a modular verification calculus that reduces correctness of temporal behavior of distributed hybrid systems to non-temporal reasoning, and prove that we obtain a complete axiomatization relative to the non-temporal base logic QdL. Using this calculus, we analyze temporal safety properties in a distributed air traffic control system where aircraft can appear dynamically.


Introduction
Ensuring correct functioning of cyber-physical systems is among the most challenging and most important problems in computer science, mathematics, and engineering. Hybrid systems are common mathematical models for cyber-physical systems with interacting discrete and continuous behavior [6,13]. Their behavior combines continuous evolution (called flow) characterized by differential equations and discrete jumps. However, not all relevant cyber-physical systems can be modeled as hybrid systems. Hybrid systems cannot represent physical control systems that are distributed or form a multi-agent system, e.g., distributed car control systems [15] and distributed air traffic control systems [8]. Such systems form distributed hybrid systems [7,16,21,22] with discrete, continuous, structural, and dimension-changing dynamics. Distributed hybrid systems combine the challenges of hybrid systems and distributed systems. Correctness of safety-critical real-time and distributed hybrid systems depends on a safe operation throughout all states of all possible trajectories, and the behavior at intermediate states is highly relevant [1,4,6,11,13].
Temporal logics (TL) use temporal operators to talk about intermediate states [1,9,10,23]. They have been used successfully in model checking [1,3,13,14,18] of finite-state system abstractions. State spaces of distributed hybrid systems, however, often do not admit equivalent finite-state abstractions [13,18]. Instead of model checking, TL can also be used deductively to prove validity of formulas in calculi [5,6]. Valid TL formulas, however, only express very generic facts that are true for all systems, regardless of their actual behavior. Hence, the behavior of a specific system first needs to be axiomatized declaratively to obtain meaningful results. Then, however, the correspondence between actual system operations and a declarative temporal representation may be questioned.
Very recently, a dynamic logic, called quantified differential dynamic logic (QdL) has been introduced as a successful tool for deductively verifying distributed hybrid systems [21,22]. QdL can analyze the behavior of actual distributed hybrid system models, which are specified operationally. Yet, operational distributed hybrid system models are internalized within QdL formulas, and QdL is closed under logical operators. However, QdL only considers the behavior of distributed hybrid systems at final states, which is insufficient for verifying safety properties that have to hold all the time.
We close this gap of expressivity by combining QdL with temporal logic [9,10,23]. In this paper, we introduce a logic, called quantified differential temporal dynamic logic (QdTL), which provides modalities for quantifying over traces of distributed hybrid systems based on QdL. We equip QdTL with temporal operators to state what is true all along a trace or at some point during a trace. In this paper, we modify the semantics of the dynamic modality [α] to refer to all traces of α instead of all final states reachable with α (similarly for α ). For instance, the formula [α] φ expresses that φ is true at each state during all traces of the distributed hybrid system α. With this, QdTL can also be used to verify temporal statements about the behavior of α at intermediate states during system runs. As in our non-temporal dynamic logic QdL [21,22], we use quantified hybrid programs as an operational model for distributed hybrid systems, since they admit a uniform compositional treatment of interacting discrete transitions, continuous evolutions, and structural/dimension changes in logic.
As a semantical foundation for combined temporal dynamic formulas, we introduce a hybrid trace semantics for QdTL. We prove that QdTL is a conservative extension of QdL: for non-temporal specifications, trace semantics is equivalent to the non-temporal transition semantics of QdL [21,22].
As a means for verification, we introduce a sequent calculus for QdTL that successively reduces temporal statements about traces of quantified hybrid programs to non-temporal QdL formulas. In this way, we make the intuition formally precise that temporal safety properties can be checked by augmenting proofs with appropriate assertions about intermediate states. Like in [21,22], our calculus works compositionally. It decomposes correctness statements about quantified hybrid programs structurally into corresponding statements about its parts by symbolic transformation.
Our approach combines the advantages of QdL in reasoning about the behaviour of operational distributed hybrid system models with those of TL to verify tempo-ral statements about traces. We show that QdTL is sound and relatively complete. We argue that QdTL can verify practical systems and demonstrate this by studying temporal safety properties in distributed air traffic control. Our primary contributions are as follows: -We introduce a logic for specifying and verifying temporal properties of distributed hybrid systems. -We present a proof calculus for this logic, which, to the best of our knowledge, is the first verification approach that can handle temporal statements about distributed hybrid systems. -We prove that this compositional calculus is a sound and complete axiomatization relative to differential equations. -We verify temporal safety properties in a collision avoidance maneuver in distributed air traffic control, where aircraft can appear dynamically.

Related Work
Multi-party distributed control has been suggested for car control [15] and air traffic control [8]. Due to limits in verification technology, no formal analysis of temporal statements about the distributed hybrid dynamics has been possible for these systems yet. Analysis results include discrete message handling [15] or collision avoidance for two participants [8].
The importance of understanding dynamic/reconfigurable distributed hybrid systems was recognized in modeling languages SHIFT [7] and R-Charon [16]. They focused on simulation/compilation [7] or the development of a semantics [16], so that no verification is possible yet.
Other process-algebraic approaches, like χ [27], have been developed for modeling and simulation. Verification is still limited to small fragments that can be translated directly to other verification tools like PHAVer or UPPAAL, which do not support distributed hybrid systems.
Our approach is completely different. It is based on first-order structures and dynamic logic. We focus on developing a logic that supports temporal and nontemporal statements about distributed hybrid dynamics and is amenable to automated theorem proving in the logic itself.
Our previous work and other verification approaches for static hybrid systems cannot verify distributed hybrid systems. Distributed hybrid systems may have an unbounded and changing number of components/participants, which cannot be represented with any fixed number of dimensions of the state space.
Based on [24], Beckert and Schlager [2] added separate trace modalities to dynamic logic and presented a relatively complete calculus. Their approach only handles discrete state spaces. In contrast, QdTL works for hybrid programs with continuous and structural/dimensional dynamics.
Davoren and Nerode [6] extended the propositional modal µ-calculus with a semantics in hybrid systems and examine topological aspects. In [5], Davoren et al. gave a semantics in general flow systems for a generalisation of CTL * [10]. In both cases, the authors of [6] and [5] provided Hilbert-style calculi to prove formulas that are valid for all systems simultaneously using abstract actions.
The strength of our logic primarily is that it is a first-order dynamic logic: it handles actual hybrid programs rather than only abstract actions of unknown effect. Our calculus directly supports verification of quantified hybrid programs with continuous evolution and structural/dimensional changes. First-order dynamic logic is more expressive and calculi are deductively stronger than other approaches [2,17].

Syntax of Quantified Differential Temporal Dynamic Logic
As a formal logic for verifying temporal specifications of distributed hybrid systems, we introduce quantified differential temporal dynamic logic (QdTL). QdTL extends dynamic logic for reasoning about system runs [12] with many-sorted first-order logic for reasoning about all (∀i : A φ) or some (∃i : A φ) objects of a sort A, e.g., the sort of all aircraft, and three other concepts: Quantified hybrid programs. The behavior of distributed hybrid systems can be described by quantified hybrid programs [21,22], which generalize regular programs from dynamic logic [12] to distributed hybrid changes. The distinguish feature of quantified hybrid programs is that they provide uniform discrete transitions, continuous evolutions, and structural/dimension changes along quantified assignments and quantified differential equations, which can be combined by regular control operations.
Modal operators. Modalities of dynamic logic express statements about all possible behavior ([α]π) of a system α, or about the existence of a trace ( α π), satisfying condition π. Unlike in standard dynamic logic, α is a model of a distributed hybrid system. We use quantified hybrid programs to describe α as in [21,22]. Yet, unlike in standard dynamic logic [12] or quantified differential dynamic logic (QdL) [21,22], π is a trace formula in QdTL, and π can refer to all states that occur during a trace using temporal operators.
Temporal operators. For QdTL, the temporal trace formula φ expresses that the formula φ holds all along a trace selected by [α] or α . For instance, the state formula α φ says that the state formula φ holds at every state along at least one trace of α. Dually, the trace formula ♦φ expresses that φ holds at some point during such a trace. It can occur in a state formula α ♦φ to express that there is such a state in some trace of α, or as [α]♦φ to say that, along each trace, there is a state satisfying φ. In this paper, the primary focus of attention is on homogeneous combinations of path and trace quantifiers like [α] φ or α ♦φ.

Quantified Hybrid Programs
QdTL supports a (finite) number of object sorts, e.g., the sort of all aircraft, or the sort of all cars. For continuous quantities of distributed hybrid systems like positions or velocities, we add the sort R for real numbers. Terms of QdTL are built from a set of (sorted) function/variable symbols as in many-sorted first-order logic. For representing appearance and disappearance of objects while running QHPs, we use an existence function symbol E(·) that has value E(o) = 1 if object o exists, and has value E(o) = 0 when object o disappears or has not been created yet. We use 0, 1, +, −, · with the usual notation and fixed semantics for real arithmetic. For n ≥ 0 we abbreviate f (s 1 , . . . , s n ) by f (s) using vectorial notation and we use s = t for element-wise equality. As a system model for distributed hybrid systems, QdTL uses quantified hybrid programs (QHP) [21,22]. The quantified hybrid programs occurring in dynamic modalities of QdTL are regular programs from dynamic logic [12] to which quantified assignments and quantified differential equation systems for distributed hybrid dynamics are added. QHPs are defined by the following grammar (α, β are QHPs, θ a term, i a variable of sort A, f is a function symbol, s is a vector of terms with sorts compatible to f , and χ is a formula of first-order logic): The effect of quantified assignment ∀i : A f (s) := θ is an instantaneous discrete jump assigning θ to f (s) simultaneously for all objects i of sort A. The QHP ∀i : C a(i) := a(i)+1, for example, expresses that all cars i of sort C simultaneously increase their acceleration a(i). The effect of quantified differential equation ∀i : A f (s) ′ = θ & χ is a continuous evolution where, for all objects i of sort A, all differential equations f (s) ′ = θ hold and formula χ holds throughout the evolution (the state remains in the region described by χ). The dynamics of QHPs changes the interpretation of terms over time: f (s) ′ is intended to denote the derivative of the interpretation of the term f (s) over time during continuous evolution, not the derivative of f (s) by its argument s. For f (s) ′ to be defined, we assume f is an R-valued function symbol. For simplicity, we assume that f does not occur in s. In most quantified assignments/differential equations s is just i. For instance, the following QHP expresses that all cars i of sort C drive by ∀i : C x(i) ′′ = a(i) such that their position x(i) changes continuously according to their respective acceleration a(i).
The effect of test ?χ is a skip (i.e., no change) if formula χ is true in the current state and abort (blocking the system run by a failed assertion), otherwise. Nondeterministic choice α ∪ β is for alternatives in the behavior of the distributed hybrid system. In the sequential composition α; β, QHP β starts after α finishes (β never starts if α continues indefinitely). Nondeterministic repetition α * repeats α an arbitrary number of times, possibly zero times.
Structural dynamics of distributed hybrid systems corresponds to quantified assignments to function terms and we model the appearance of new participants in the distributed hybrid system, e.g., new aircraft appearing into the local flight scenario, by a program n := new A (see [21,22] for details).

State and Trace Formulas
The formulas of QdTL are defined similarly to first-order dynamic logic plus manysorted first-order logic. However, the modalities [α] and α accept trace formulas that refer to the temporal behavior of all states along a trace. Inspired by CTL and CTL * [9,10], we distinguish between state formulas, which are true or false in states, and trace formulas, which are true or false for system traces.
The state formulas of QdTL are defined by the following grammar (φ, ψ are state formulas, π is a trace formula, θ 1 , θ 2 are terms of the same sort, i is a variable of sort A, and α is a QHP): We use standard abbreviations to define ≤, >, <, ∨, →. Sorts A = R have no ordering and only θ 1 = θ 2 is allowed. For sort R, we abbreviate ∀x : R φ by ∀xφ.
The trace formulas of QdTL are defined by the following grammar (π is a trace formula and φ is a state formula): Formulas without and ♦ are non-temporal QdL formulas. Unlike in CTL, state formulas are true on a trace if they hold for the last state of a trace, not for the first. Thus, [α]φ expresses that φ is true at the end of each trace of α. In contrast, [α] φ expresses that φ is true all along all states of every trace of α. This combination gives a smooth embedding of non-temporal QdL into QdTL and makes it possible to define a compositional calculus. Like CTL, QdTL allows nesting with a branching time semantics [9], e.g., [α] ((∀i : C x(i) ≥ 2) → β ♦(∀i : C x(i) ≤ 0)). In the following, all formulas and terms have to be well-typed. For short notation, we allow conditional terms of the form if φ then θ 1 else θ 2 fi (where θ 1 and θ 2 have the same sort). This term evaluates to θ 1 if the formula φ is true and to θ 2 otherwise. We consider formulas with conditional terms as abbreviations, e.g., Example 1. Let C be the sort of all cars. By x(i), we denote the position of car i, by v(i) its velocity and by a(i) its acceleration. Then the QdTL formula says that, if all cars start at a point to the right of the origin and we only allow them to evolve as long as all of them have nonnegative velocity, then they always stay up to the right of the origin. In this case, the QHP just consists of a quantified differential equation expressing that the position x(i) of car i evolves over time according to the velocity v(i), which evolves according to its acceleration a(i). The constraint v(i) ≥ 0 expresses that the cars never move backwards, which otherwise would happen eventually in the case of braking a(i) < 0. This formula is indeed valid, and we would be able to use the techniques developed in this paper to prove it.

Semantics of Quantified Differential Temporal Dynamic Logic
In standard dynamic logic [12] and the logic QdL [21,22], modalities only refer to the final states of system runs and the semantics is a reachability relation on states: State τ is reachable from state σ using α if there is a run of α which terminates in τ when started in σ. For QdTL, however, formulas can refer to intermediate states of runs as well. Thus, the semantics of a distributed hybrid system α is the set of its possible traces, i.e., successions of states that occur during the evolution of α.

Trace Semantics of Quantified Hybrid Programs
A state σ associates an infinite set σ(A) of objects with each sort A, and it associates a function σ(f ) of appropriate type with each function symbol f , including E(·).
For simplicity, σ also associates a value σ(i) of appropriate type with each variable i. The domain of R and the interpretation of 0, 1, +, −, · is that of real arithmetic. We assume constant domain for each sort A: all states σ, τ share the same infinite The set of all states is denoted by S. The state σ e i agrees with σ except for the interpretation of variable i, which is changed to e. In addition, we distinguish a state Λ to denote the failure of a system run when it is aborted due to a test ?χ that yields false. In particular, Λ can only occur at the end of an aborted system run and marks that there is no further extension.
Distributed hybrid systems evolve along piecewise continuous traces in multidimensional space, structural changes, and appearance or disappearance of agents as time passes. Continuous phases are governed by differential equations, whereas discontinuities are caused by discrete jumps. Unlike in discrete cases [2,24], traces are not just sequences of states, since distributed hybrid systems pass through uncountably many states even in bounded time. Beyond that, continuous changes are more involved than in pure real-time [1,14], because all variables can evolve along different differential equations. Generalizing the real-time traces of [14], the following definition captures hybrid behavior by splitting the uncountable succession of states into periods ν i that are regulated by the same control law. For discrete jumps, some periods are point flows of duration 0.
The (trace) semantics of quantified hybrid programs is compositional, that is, the semantics of a complex program is defined as a simple function of the trace semantics of its parts.
Unlike in [1,14], the definition of traces also admits finite traces of bounded duration, which is necessary for compositionality of traces in α; β. The semantics of quantified hybrid programs α as the set µ(α) of its possible traces depends on valuations σ · of formulas and terms at intermediate states σ. The valuation of formulas will be defined in Definition 3. Especially, we use σ e i · to denote the valuations of terms and formulas in state σ e i , i.e., in state σ with i interpreted as e.
For trace formulas, the valuation ν · with respect to trace ν is defined as follows: As usual, a (state) formula is valid if it is true in all states. Further for (state) formula φ and state σ we write σ |= φ iff σ φ = true. We write σ |= φ iff σ φ = false. Likewise, for trace formula π and trace ν we write ν |= π iff ν π = true and ν |= π iff ν π = false. In particular, we only write ν |= π or ν |= π if ν π is defined, which it is not the case if π is a state formula and ν does not terminate.

Conservative Temporal Extension
The following result shows that the extension of QdTL by temporal operators does not change the meaning of non-temporal QdL formulas. The trace semantics given in Definition 3 is equivalent to the final state reachability relation semantics [21,22] for the sublogic QdL of QdTL. Proposition 1. The logic QdTL is a conservative extension of non-temporal QdL, i.e., the set of valid QdL formulas is the same with respect to transition reachability semantics of QdL [21,22] as with respect to the trace semantics of QdTL (Definition 3).

Safety Properties in Distributed Air Traffic Control
In air traffic control, collision avoidance maneuvers [8,26] are used to resolve conflicting flight paths that arise during free flight. We consider the roundabout collision avoidance maneuver for air traffic control [26]. In the literature, formal verification of the hybrid dynamics of air traffic control focused on a fixed number of aircraft, usually two. In reality, many more aircraft are in the same flight corridor, even if not all of them participate in the same maneuver. They may be involved in multiple distributed maneuvers at the same time, however. Perfect global trajectory planning quickly becomes infeasible then. The verification itself also becomes much more complicated for three aircraft already. Explicit replication of the system dynamics n times is computationally infeasible for larger n. Yet, collision avoidance maneuvers need to work for an (essentially) unbounded number of aircraft. Because global trajectory planning is infeasible, the appearance of other aircraft into a local collision avoidance maneuver always has to be expected and managed safely. See Fig. 1 for a general illustration of roundabout-style collision avoidance maneuvers and the phenomenon of dynamic appearance of some new aircraft z into the horizon of relevance. The resulting flight control system has several characteristics of hybrid dynamics. But it is not a hybrid system and does not even have a fixed finite number of variables in a fixed finite-dimensional state space. The system forms a distributed hybrid system, in which all aircraft fly at the same time and new aircraft may appear from remote areas into the local flight scenario. Let A be the sort of all aircraft. Each aircraft i has a position x(i) = (x 1 (i), x 2 (i)) and a velocity vector d(i) = (d 1 (i), d 2 (i)). We model the continuous dynamics of an aircraft i that follows a flight curve with an angular velocity ω(i) by the (function) differential equation: This differential equation, which we denote by F ω(i) (i), is the standard equation for curved flight from the literature [26], but lifted to function symbols that are parameterized by aircraft i. Now the quantified differential equation ∀i : A F ω(i) (i) characterizes that all aircraft i fly along their respective (function) differential equation F ω(i) (i) according to their respective angular velocities ω(i) at the same time. This quantified differential equation captures what no finite-dimensional differential equation system could ever do. It characterizes the simultaneous movement of an unbounded, arbitrary, and even growing or shrinking set of aircraft. Two aircraft i and j have violated the safe separation property if they falsify the following formula which says that aircraft i and j are either identical or separated by at least the protected zone p (usually 5mi). For the aircraft control system to be safe, all aircraft have to be safely separated, i.e., need to satisfy ∀i, j : A P(i, j). It is crucial that this formula holds at every point in time during the system evolution, not only at its beginning or at its end. Hence, we need to consider temporal safety properties. For instance, QdTL can analyze the following temporal safety properties of a part of the distributed roundabout collision avoidance maneuver for air traffic control: t is a clock variable, and T is some bounded time.
The temporal safety invariant in (1) expresses that the circle phase of roundabout maneuver always stays collision-free indefinitely for an arbitrary number of aircraft. That is the most crucial part because we have to know the aircraft always remain safe during the actual roundabout collision avoidance circle. The condition ∀i, j : A T (i, j) characterizes compatible tangential maneuvering choices. Without a condition like T (i, j), roundabouts can be unsafe [20]. For a systematic derivation of how to construct T (i, j), we refer to the work [20]. As a variation of (1), the temporal safety property in (2) states that, for an arbitrary number of aircraft, the circle procedure of roundabout maneuver cannot produce collisions at any point in its bounded duration T . This variation restricts the continuous evolution to take exactly T time units (the evolution domain region restricts the evolution to t ≤ T and the subsequent test to ?(∀i : A t = T )) and no intermediate state is visible as a final state anymore. Thus, the temporal modality in (2) is truly necessary. We will use the techniques developed in this paper to verify these temporal safety properties in the distributed roundabout flight collision avoidance maneuver.

Proof Calculus for Temporal Properties
In this section, we introduce a sequent calculus for verifying temporal specifications of distributed hybrid systems in QdTL. With the basic idea being to perform a symbolic decomposition, the calculus transforms quantified hybrid programs successively into simpler logical formulas describing their effects. Statements about the temporal behavior of a quantified hybrid program are successively reduced to corresponding non-temporal statements about the intermediate states.

Proof Rules
In Fig. 2, we present a proof calculus for QdTL that inherits the proof rules of QdL from [21,22] and adds new proof rules for temporal modalities. We use the sequent notation informally for a systematic proof structure. A sequent is of the form Γ → ∆, where the antecedent Γ and succedent ∆ are finite sets of formulas. The semantics of Γ → ∆ is that of the formula φ∈Γ φ → ψ∈∆ ψ and will be treated as an abbreviation. As usual in sequent calculus, the proof rules are applied backwards from the conclusion (goal below horizontal bar) to the premises (subgoals above bar).
Inherited Non-temporal Rules The QdTL calculus inherits the (non-temporal) QdL proof rules. For propositional logic, standard rules ax-cut are listed in Fig. 2. Rules [; ]-? work similar to those in [12]. Rules [ ′ ], ′ handle continuous evolutions for quantified differential equations with first-order definable solutions. Rules [:=]-: * handle discrete changes for quantified assignments. Axiom ex expresses that, for sort A = R, there always is a new object n that has not been created yet (E(n) = 0), because domains are infinite. The quantifier rules ∀r-i∃ combine quantifier handling of many-sorted logic based on instantiation with theory reasoning by quantifier elimination (QE) for the theory of reals. The global rules []gen, gen are Gödel generalization rules and ind is an induction schema for loops with inductive invariant φ [12]. Similarly, con generalizes Harel's convergence rule [12] to the hybrid case with decreasing variant ϕ [19]. DI and DC are rules for quantified differential equations with quantified differential invariants [21,22]. Notice that [∪], ∪ can be generalized to apply to formulas of the form [α ∪ β]π where π is an arbitrary trace formula, and not just a state formula as in QdL. Thus, π may begin with and ♦, which is why the rules are repeated in this generalized form as [∪] and ∪ ⋄ in Fig. 2.

Temporal Rules
The new temporal rules in Fig. 2   ys(t) of the (injective) differential equations and f (s) as initial values. See [21,22] for the definition of a injective quantified assignment or quantified differential equation. 2 Occurrence f (u) in φ(f (u)) is not in scope of a modality (admissible substitution) and we abbreviate assignment ∀i : A f (s) := θ by A, which is assumed to be injective. . . , Xn are all free logical variables of ∀x φ(x). 5 θ is an abbreviate term, often a new logical variable. 6 X, Y are new variables of sort R. QE needs to be applicable in the premises. 7 Among all open branches, the free (existential) logical variable X of sort R only occurs in the branch Φi → Ψi. QE needs to be defined for the formula in the premises, especially, no Skolem dependencies on X occur. 8 logical variable v does not occur in α. 9 The operator D, as defined in [21,22], is used to computer syntactic total derivations of formulas algebraically. 10 π is a trace formula, whereas φ and ψ are (state) formulas. Unlike φ and ψ, the trace formula π may thus begin with a temporal modality or ♦. The dual rules ∪ ⋄, ; ⋄, := ⋄, ? ⋄, ′ ⋄, * n ⋄ work similarly. Rules for handling [α]♦φ and α φ are discussed in Section 8.
The inductive definition rules [ * ] and * ⋄ completely reduce temporal properties of loops to QdTL properties of standard non-temporal QdL modalities such that standard induction (ind) or convergence (con) rules, as listed in Fig. 2, can be used for the outer non-temporal modality of the loop. Hence, after applying the inductive loop definition rules [ * ] and * ⋄, the standard QdL loop invariant and variant rules can be used for verifying temporal properties of loops without change, except that the postcondition contains temporal modalities.

Soundness and Completeness
The following result shows that verification with the QdTL calculus always produces correct results about the safety of distributed hybrid systems, i.e., the QdTL calculus is sound.
Theorem 1 (Soundness of QdTL). The QdTL calculus is sound, i.e., every QdTL (state) formula that can be proven is valid.
The verification for temporal safety ([α] φ or α ♦φ), temporal liveness ([α]♦φ or α φ), and non-temporal ([α]φ or α φ) fragments of distributed hybrid systems has three independent sources of undecidability. Thus, no verification technique can be effective. Hence, QdTL cannot be effectively axiomatizable. Both its discrete and its continuous fragments alone are subject to Gödel's incompleteness theorem [19]. The fragment with only structural and dimension-changing dynamics is not effective either, because it can encode two-counter machines.
QdL has been proved to be complete relative to quantified differential equations [21,22]. Due to the modular construction of the QdTL calculus, we can lift the relative completeness result from QdL to QdTL. We essentially show that QdTL is complete relative to QdL, which directly implies that QdTL calculus is even complete relative to an oracle for the fragment of QdTL that has only quantified differential equations in modalities. Again, we restrict our attention to homogeneous combinations of path and trace quantifiers like [α] φ or α ♦φ.
Theorem 2 (Relative Completeness of QdTL). The calculus in Fig. 2 is a complete axiomatization of QdTL relative to quantified differential equations.
This result shows that both temporal and non-temporal properties of distributed hybrid systems can be proven to exactly the same extent to which properties of quantified differential equations can be proven. It also gives a formal justification that the QdTL calculus reduces temporal properties to non-temporal QdL properties.

Verification of Distributed Air Traffic Control Safety Properties
Continuing the distributed air traffic control study from Section 5, the QdTL proofs of the temporal safety invariant in (1) and the temporal safety property in (2) are presented in Fig. 3 and Fig. 4, respectively (for the purpose of simplifying the presentation, we ignore typing information A for aircraft in the proof, because it is clear from the context). Note that temporal and non-temporal properties of the maneuver cannot be proven using any hybrid systems verification technique, because the dimension is parametric and unbounded and may even change dynamically during the remainder of the maneuver. The single proof in Fig. 3 or Fig. 4 corresponds to infinitely many proofs for systems with n aircraft for all n.
Our proofs show that the distributed roundabout maneuver always safely avoids collisions for arbitrarily many aircraft (even with dynamic appearance of new aircraft). The above maneuver still requires all aircraft in the horizon of relevance to participate in the collision avoidance maneuver. In fact, we can show that this is unnecessary for aircraft that are far enough away and that may be engaged in other roundabouts. Yet, this is beyond the scope of this paper.

Liveness by Quantifier Alternation
Liveness specifications of the form [α]♦φ or α φ are sophisticated (Σ 1 1 -hard because they can express infinite occurrence in Turing machines). Beckert and Schlager [2], for instance, note that they failed to find sound rules for a discrete case that corresponds to [α; β]♦φ.
For finitary liveness semantics, we can still find proof rules. In this section, we modify the meaning of [α]♦φ to refer to all terminating traces of α. Then, the straightforward generalization [; ]⋄ in Fig. 5 is sound, even in the hybrid case. But [; ]⋄ still leads to an incomplete axiomatization as it does not cover the case where, in some traces, φ becomes true at some point during α, and in other traces, φ only becomes true during β. To overcome this limitation, we use a program transformation approach. We instrument the quantified hybrid program to monitor the Abbreviations: . The latter is a continuous evolution restricted to the region that satisfies χ and φ → t = 1. The effect is that t detects whether φ has occurred during any change in α. In particular, t is guaranteed to be 1 after all runs if φ occurs at least once along all traces of α.

Conclusions and Future Work
For reasoning about distributed hybrid systems, we have introduced a temporal dynamic logic, QdTL, with modal path quantifiers over traces and temporal quantifiers along the traces. It combines the capabilities of quantified differential dynamic logic to reason about possible distributed hybrid system behavior with the QdTL. This theoretical result shows that the QdTL calculus is a sound and complete axiomatization of the temporal behavior of distributed hybrid systems relative to differential equations. As an example, we demonstrate that our logic is suitable for reasoning about temporal safety properties in a distributed air traffic control system.
Proof (of Proposition 1). The formulas of QdL are a subset of the QdTL formulas. In the course of this proof, we use the notation σ QdL · to indicate that the QdL valuation from Definition 5 is used. For QdL formulas ψ, we show that the valuations with respect to Definition 3 and with respect to Definition 5 are the same for all states σ: σ ψ = σ QdL ψ for all σ.

B.1 Proof of Soundness
Proof (Proof of Theorem 1). We show that all rules of the QdTL calculus are locally sound, i.e., for all states σ, the conclusion of a rule is true in state σ when all premisses are true in σ. Let σ be any state. For each rule we have to show that the conclusion is true in σ assuming the premisses are true in σ. Inductively, the soundness of the non-temporal rules follows from Proposition 1 and local soundness of the corresponding rules in QdL [21,22]. The proof for the generalization in [∪] and ∪ to path formulas π is a straightforward extension.