File preview

A COMPLETE AXIOMATIZATION OF QUANTIFIED DIFFERENTIAL DYNAMIC LOGIC FOR DISTRIBUTED HYBRID SYSTEMS
´ ANDRE PLATZER Carnegie Mellon University, Computer Science Department, Pittsburgh, PA, USA e-mail address: aplatzer@cs.cmu.edu

Abstract. We address a fundamental mismatch between the combinations of dynamics that occur in cyber-physical systems and the limited kinds of dynamics supported in analysis. Modern applications combine communication, computation, and control. They may even form dynamic distributed networks, where neither structure nor dimension stay the same while the system follows hybrid dynamics, i.e., mixed discrete and continuous dynamics. We provide the logical foundations for closing this analytic gap. We develop a formal model for distributed hybrid systems. It combines quantiﬁed diﬀerential equations with quantiﬁed assignments and dynamic dimensionality-changes. We introduce a dynamic logic for verifying distributed hybrid systems and present a proof calculus for this logic. This is the ﬁrst formal veriﬁcation approach for distributed hybrid systems. We prove that our calculus is a sound and complete axiomatization of the behavior of distributed hybrid systems relative to quantiﬁed diﬀerential equations. In our calculus we have proven collision freedom in distributed car control even when an unbounded number of new cars may appear dynamically on the road.

1. Introduction Many safety-critical computers are embedded in cyber-physical systems like cars [HESV91, SRS+ 06] and aircraft [DMC05]. How do we know that their designs will work as intended? Most initial designs do not. And some deployed systems still do not. Ensuring the correct functioning of cyber-physical systems is a central challenge in computer science, mathematics, and engineering, because it is the key to designing smart and reliable control. Scientists
1998 ACM Subject Classiﬁcation: F.3.1 Logics and Meanings of Programs: Specifying and Verifying and Reasoning about Programs, F.4.1 Mathematical Logic and Formal Languages: Mathematical Logic, D.2.4 Software Engineering: Software/Program Veriﬁcation, C.1.m: Hybrid Systems, C.2.4 ComputerCommunication Networks: Distributed Systems, D.4.7 Organization and Design: Distributed Systems. Key words and phrases: Diﬀerential dynamic logic, Distributed hybrid systems, Axiomatization, Theorem proving, Quantiﬁed diﬀerential equations, Proof theory. An extended abstract has appeared at CSL’10 [Pla10c]. This material is based upon work supported by the National Science Foundation under NSF CAREER Award CNS-1054246, NSF EXPEDITION CNS-0926181, and under Grant Nos. CNS-1035800 and CNS0931985, by the NASA grant NNG-05GF84H, and by the ONR award N00014-10-1-0188.

LOGICAL METHODS IN COMPUTER SCIENCE

DOI:10.2168/LMCS-???

c Andre Platzer ´ Creative Commons

1

2

´ ANDRE PLATZER

and engineers need analytic tools to understand and predict the behavior of their systems. As systems become ever more complex, it becomes prohibitively expensive or impossible to test all possible interactions and rule out unsafe behavior by simulation. Formal veriﬁcation techniques are used routinely to overcome this for ﬁnite systems. But for cyber-physical systems, there is not even a foundation for veriﬁcation that would cover all required behavior. There is a fundamental mismatch between the actual dynamics of cyber-physical system applications and the limits imposed by current modeling and analysis. Cyber-physical systems in automotive, aviation, railway, and power grids combine communication, computation, and control. Combining computation and control leads to hybrid systems [ACHH92, Bra95, Hen96, BBM98, Pla10b], whose behavior involves both discrete and continuous dynamics originating, e.g., from discrete control decisions and diﬀerential equations of motion. Combining communication and computation leads to distributed systems [Lyn96, AL01, AdBO10], whose dynamics are discrete transitions of system parts that communicate with each other. They may form dynamic distributed systems, where the structure of the system is not ﬁxed but evolves over time and agents may appear or disappear during the system evolution. Combinations of all three aspects (communication, computa( ) ( ) tion, and control) are used in sophisticated applications, e.g., co(2) (2) (3) (3) (4) (4) (1) (1) operative distributed car control [HESV91] and decentralized aircraft control [PSFB07]. Neither the structure nor dimension of the system stay the same, because new Figure 1: Distributed car control. cars can appear on the street or leave it; see Fig. 1. These systems are (dynamic) distributed hybrid systems, i.e., systems that combine the dynamics of distributed systems with the discrete and continuous dynamics of hybrid systems. More generally, distributed hybrid systems are multi-agent hybrid systems that interact through remote communication or physical interaction. They cannot be considered just as a distributed system (because, e.g., the continuous evolution of positions and velocities matters crucially for collision freedom in car control) nor just as a hybrid system (because the evolving system structure and appearance of new agents can make an otherwise collision-free system unsafe). It is generally impossible to split the analysis of distributed hybrid systems soundly into an analysis of a distributed system (without continuous movement) and an analysis of a hybrid system (without structural changes or appearance), because all kinds of dynamics interact. Just like hybrid systems are diﬀcult to analyze from a purely discrete or a purely continuous perspective [Hen96, Pla12]. Distributed hybrid systems have been considered to varying degrees in modeling languages [DGV96, Rou04, KSPL06, MS06]. In order to build these systems, however, scientists and engineers also need analytic tools to understand and predict their behavior. But formal veriﬁcation and proof techniques do not yet support the required combination of dynamical eﬀects—which is not surprising given the numerous sources of undecidability for distributed hybrid systems veriﬁcation.

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

3

In this article, we provide the logical foundations to close this fundamental analytic gap. We develop quantiﬁed hybrid programs (QHPs) as a formal model for distributed hybrid systems, which combine dynamical eﬀects from multiple sources: discrete transitions, continuous evolution, dimension changes, and structural dynamics. In order to account for changes in the dimension and for co-evolution of an unbounded and evolving number of participants, we generalize the notion of states from assignments for primitive system variables like x to full ﬁrst-order structures. In a QHP, function term x(i) may denote the position of car i of type C, the term f (i) could be the car registered by communication as the car following car i, and the term d(i, f (i)) could denote the minimum safety distance negotiated between car i and its follower f (i). The values of all these terms may evolve for all i as time progresses according to interacting laws of discrete and continuous dynamics, because all cars evolve simultaneously. They are also aﬀected by changing the system dimension as new cars appear, disappear, or by reconﬁguring the system structure dynamically, e.g., by remote communication or physical interaction. The deﬁning characteristic of QHPs is that they allow quantiﬁed hybrid dynamics in which variables like i that occur in function arguments of the system dynamics are quantiﬁed over, such that the system co-evolves, e.g., for all cars i of type C. This quantiﬁcation is necessary to characterize the distributed hybrid systems dynamics with an unbounded and possibly evolving number of participants. Quantiﬁcation is also necessary to represent structural dynamics when the number of participants is not ﬁxed. There is a crucial diﬀerence between a primitive system variable x and a ﬁrst-order function term x(i), where i is quantiﬁed over. Hybrid dynamics of primitive system variables can model a concrete number of, say, four cars (putting scalability issues aside), but neither a parametric number of n cars nor systems with a variable number of cars (a number n that may change over time). With ﬁrst-order function symbols x(i) and hybrid dynamics quantifying over all cars i, a single QHP can represent any number of cars at once. QHPs can even represent (dis)appearance of cars by changing the domain that quantiﬁers range over dynamically at runtime. QHPs are thus a formal model for general (dynamic) distributed hybrid systems. Veriﬁcation of distributed hybrid systems is challenging. We show that they have three independent sources of undecidability: discrete dynamics, continuous dynamics, and structural/dimensional dynamics. As an analysis tool for distributed hybrid systems, we introduce a speciﬁcation and veriﬁcation logic for QHPs that we call quantiﬁed diﬀerential dynamic logic (QdL). QdL provides dynamic logic [Pra76, HKT00] modal operators [α] and α that refer to the states reachable by QHP α and can be placed in front of any formula. Formula [α]φ expresses that all states reachable by system α satisfy formula φ, while α φ expresses that there is at least one reachable state satisfying φ. These modalities can express necessary or possible properties of the transition behavior of QHP α. With its ability to specify and verify properties of (dynamic) distributed hybrid systems and quantiﬁed dynamics, QdL is a major extension of prior work for static hybrid systems [Pla08a, Pla10a] and conventional discrete programs [BP06, R¨m06]. u Our primary contributions are: • We introduce a formal system model and semantics that succinctly captures the logical quintessence of (dynamic) distributed hybrid systems with joint discrete, continuous, structural, and dimension-changing dynamics. • We introduce a speciﬁcation and veriﬁcation logic for (dynamic) distributed hybrid systems.

4

´ ANDRE PLATZER

• We present a proof calculus for this logic, which, to the best of our knowledge, is the ﬁrst veriﬁcation approach that can handle distributed hybrid systems with their hybrid dynamics and unbounded (and evolving) dimensions and structure. • We prove that this compositional calculus is a sound and complete axiomatization of (dynamic) distributed hybrid systems relative to quantiﬁed diﬀerential equations. • We have used our proof calculus to verify collision freedom in a distributed car control system, where an unbounded number of new cars may appear dynamically on the road. In particular, we extend our previous extended abstract [Pla10c] by 28 pages worth of • soundness and relative completeness proofs • new results on ineﬀective fragments • more detailed explanations and more examples • new derived proof rules • new formal proofs illustrating the interaction of quantiﬁers, ﬁrst-order function symbols, and quantiﬁed system dynamics in detail • a proof of collision avoidance in a simple distributed car control system, and a new result about a more advanced distributed car control system. This work constitutes the logical foundation for analysis of distributed hybrid systems. Since distributed hybrid control is the key to control numerous advanced systems, analytic approaches have signiﬁcant potential for applications. With a theorem prover based on our approach, we have veriﬁed collision avoidance in a distributed car control system, which is out of scope for other approaches. The approach presented here has been used subsequently for verifying distributed adaptive cruise control systems for highways [LPN11] and distributed air traﬃc control [Pla11]. Our veriﬁcation approach for distributed hybrid systems is a fundamental extension compared to previous approaches. In much the same way as ﬁrst-order logic increases the expressive power over propositional logic (quantiﬁers and function symbols are required to express properties of unbounded structures), QdL increases the expressive power over its predecessors (because ﬁrst-order functions and quantiﬁers in the dynamics of QHPs are required to characterize systems with unbounded and changing dimensions). 2. Related Work Multi-party distributed control has been suggested for car control [HESV91] and air traﬃc control [DMC05]. Due to limits in veriﬁcation technology, no formal analysis of the distributed hybrid dynamics has been possible for these systems yet. Analysis results include discrete message handling [HESV91] or collision avoidance for two participants [DMC05]. In distributed car control and air traﬃc control systems, appearance of new participants is a major unsolved challenge for formal veriﬁcation. Ad-hoc informal arguments have been used to discuss distribution eﬀects away, e.g., assuming that at most 4 cars are close to one another. These arguments are treacherous, though. They are very case-speciﬁc and do not lend themselves to formal veriﬁcation within one proof system because they need arguments outside the proof system to work. In distributed car control, for instance, it might, at ﬁrst sight, be convincing to suspect that it would be enough to consider every possible constellation of, say, four cars. This breaks down at second thought, though, because, without a formal proof, there is no reason to believe that a locally consistent and safe system would be globally safe and consistent. Consider

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

5

an example for the situation in Fig. 1, for instance. Even if hybrid systems veriﬁcation techniques could show that local patterns consisting of the four cars {1, 2, n, 3} are safe and that local patterns consisting of the four cars {2, n, 3, 4} are safe, the full system consisting of all cars {1, 2, n, 3, 4} still does not have to be safe. For example, the local pattern {1, 2, n, 3} could be safe, because it will ask car n to change lanes and ask car 2 to keep speed and car 3 to speed up. But the pattern {2, n, 3, 4} could be safe, because it will ask car n to change lanes but, instead, ask car 2 to slow down and car 3 to keep speed. Those two locally safe patterns still lead to a globally incompatible maneuver choice resulting in a crash, because both cars 2 and 3 would be forced to keep the speed (for they would otherwise collide with car 1 or 4, respectively) and, henceforth, collide with car n during its lane change. More generally, independent actions in diﬀerent parts of a system may still end up interacting by rippling eﬀects. It is, thus, crucial to understand and verify the emergent behavior resulting from local control principles. The full distributed hybrid systems dynamics needs to be considered and we cannot generally hope to prove meaningful properties by simply ignoring part of the dynamics. The importance of understanding dynamic / reconﬁgurable distributed hybrid systems was recognized in modeling languages SHIFT [DGV96] and R-Charon [KSPL06] before. They focused on simulation and compilation [DGV96] or the development of a semantics [KSPL06], so that no veriﬁcation is possible yet. For stochastic simulation, see [MS06], where soundness has not been proven, because ensuring coverage is diﬃcult by a random simulation. See [ZPC10] for a discussion of statistical evidence that can be obtained for randomized discrete-time hybrid systems by fair (i.i.d. sampled) simulation. This technique neither covers distributed hybrid systems nor continuous-time hybrid systems nor nondeterministic dynamics, all of which we cover in this article. For distributed hybrid systems, even giving a formal semantics is very challenging [CJR95, Rou04, KSPL06, vBMR+ 06]! Zhou et al. [CJR95] gave a semantics for a hybrid version of CSP in the Extended Duration Calculus [ZRH92]. Rounds [Rou04] gave a semantics in a rich set theory for a spatial logic for a hybrid version of the π-calculus. In the hybrid π-calculus, processes interact with a continuously changing environment, but cannot themselves evolve continuously, which would be crucial to capture the physical movement of traﬃc agents. From the semantics alone, no veriﬁcation is possible in these approaches, except perhaps by manual reasoning in the semantics. Other process-algebraic approaches, like χ [vBMR+ 06], have been developed for modeling and simulation purposes. Veriﬁcation is still limited to small fragments that can be translated directly to other veriﬁcation tools like PHAVer or UPPAAL, which have ﬁxed dimensions and restricted dynamics (thus no distributed hybrid systems). Our approach is completely diﬀerent. It is based on ﬁrst-order structures and dynamic logic. We focus on developing a logic that supports distributed hybrid dynamics directly and that is amenable to automated theorem proving in the logic itself. For a detailed discussion of veriﬁcation approaches for static real-time and hybrid systems, we refer to previous work [Pla08a, Pla10a, Pla08b, Pla10b]. Our previous work and other veriﬁcation 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 ﬁxed ﬁnite number of dimensions of the state space. In distributed car control, for instance, there is no prior limit on the number of cars on the street. Even when there is a limit, explicit replication of the

6

´ ANDRE PLATZER

system, say, 100 times, does not yield a scalable veriﬁcation approach, because most hybrid systems veriﬁcation approaches scale exponentially in the number of participants or worse. Approaches for distributed systems [AL01] do not cover hybrid systems, because the addition of diﬀerential equations to distributed systems is even more challenging than the addition of diﬀerential equations to discrete dynamics has been when forming hybrid systems. There is not even a bound on the number of diﬀerential equations that would need to be added to faithfully hybridize a distributed system. In summary, previous approaches to distributed hybrid systems are limited to modeling, simulation, or the deﬁnition of a semantics. No formal veriﬁcation technique was known for distributed hybrid systems before. 3. Syntax As a formal logic for specifying and verifying correctness properties of distributed hybrid systems, we introduce quantiﬁed diﬀerential dynamic logic (QdL). QdL combines dynamic logic for reasoning about all ([α]φ) or some ( α φ) system runs of a system α [Pra76, HKT00] with many-sorted ﬁrst-order logic for reasoning about all (∀i : C φ) or some (∃i : C φ) objects of a sort C, e.g., the sort of all cars. The most important deﬁning characteristic of QdL is that α can be a distributed hybrid system, because the QdL system model of quantiﬁed hybrid programs (QHP) supports quantiﬁed operations that aﬀect all objects of a sort C at once. If C is the sort of cars, the quantiﬁed assignment ∀i : C a(i) := a(i) + 1 increases the respective accelerations a(i) of all cars i at once by a single instantaneous discrete jump. It can be used to model simultaneous discrete changes in multiple agents at once. Discrete changes where only some of the cars change their acceleration, others do not, are easy to model with quantiﬁed assignments by masking. The quantiﬁed diﬀerential equation ∀i : C v(i) = a(i) represents a continuous evolution of the respective velocities v(i) of all cars i at the same time according to their acceleration by their respective diﬀerential equations v(i) = a(i). Again, continuous evolutions where only some of the cars evolve, others remain stopped, are easy to model with quantiﬁed diﬀerential equations by masking. These quantiﬁed assignments and quantiﬁed diﬀerential equation systems of QHPs are crucial for representing distributed hybrid systems where an unbounded number of objects co-evolve simultaneously, because no ﬁnite set of classical assignments and classical diﬀerential equations could represent that. Note that, because of the close semantical relationship, we use the same quantiﬁer notation ∀i : C for quantiﬁed operations in programs and for quantiﬁers in logical formulas, instead of a separate notation Πi:C for parallel products in programs. Interaction by communication can be modeled by (possibly quantiﬁed) discrete assignments to share data between agents i and j in QHPs. Physical interaction, instead, may be modeled either by (possibly quantiﬁed) discrete assignments when an agent i activates a response in agent j by an instantaneous discrete action (e.g., pushing a physical button) or by a (possibly quantiﬁed) diﬀerential equation involving multiple agents i and j when they come into physical contact and act jointly over a (nonzero) period of time (e.g., both agents jointly lifting and pulling on a rigid object). Observe that the cyber structure of the system reconﬁgures dynamically when discrete communication topologies change, whereas the physical structure reconﬁgures dynamically when agents engage in physical contact. QHPs for the latter case may involve structural changes in the quantiﬁed diﬀerential equation. We model the appearance of new participants in the distributed hybrid system, e.g., new cars entering the road, by a QHP n := new C. It creates a new object of type C, thereby

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

7

extending the range of all subsequent quantiﬁed assignments or quantiﬁed diﬀerential equations ranging over created objects of type C. With quantiﬁers and function terms, new can be handled in an entirely modular way. In order to reduce the conceptual complexity, we ﬁrst focus on the syntax and semantics of QdL and postpone the discussion of actual existence and creation until Section 5. We will see that actual existence and creation are completely modular extensions. The model of QHPs is of independent interest as a formal model for distributed hybrid systems. Inside a QHP, logical formulas can occur in state tests for conditional execution. We thus explain logical formulas, terms, and sorts ﬁrst. Conversely, however, a QHP α occurs inside the modalities ([α] and α ) of QdL formulas, which state properties of the behavior of α. Hence, QHPs may occur inside QdL formulas yet formulas may occur inside QHPs. The subsequent deﬁnitions of QdL and QHP are thus to be understood by simultaneous induction. It is easier to start with sorts, terms, and logical formulas ﬁrst and then explain the QHP model subsequently. 3.1. Quantiﬁed Diﬀerential Dynamic Logic. We introduce quantiﬁed diﬀerential dynamic logic (QdL), which is the ﬁrst formal logic for specifying and verifying correctness properties of distributed hybrid systems. QdL is a combination of many-sorted ﬁrst-order logic with dynamic logic, generalized to a system model (QHPs) for distributed hybrid systems. Sorts. QdL supports a (ﬁnite) number of object sorts, e.g., the sort of all cars and that of all aircraft. For continuous quantities of distributed hybrid systems like positions or velocities, we add the sort R of real numbers. It would be easy to add subtyping of sorts; see previous work [BP06] for details. We refrain from doing so, because that just obscures the logical essence of our approach. The primary purpose of the sorts is to distinguish diﬀerent kinds of objects in multiagent hybrid systems in which diﬀerent kinds of agents occur, e.g., cars of sort C, traﬃc lights of sort T , lanes of sort L, and aircraft of sort A. Terms. QdL terms are built from a set of (sorted) function and variable symbols as in many-sorted ﬁrst-order logic. In particular, each function symbol f has a ﬁxed type C1 × · · · × Cn → D for some n ∈ N and some sorts D, C1 , . . . , Cn such that f only accepts argument terms θ1 , . . . , θn of the respective sorts C1 , . . . , Cn and then f (θ1 , . . . , θn ) is a term of sort D. We use these function symbols to represent the state of the system or other parameters. In a car control scenario like that in Fig. 1, for instance, we could use function symbol x to represent the positions of cars, i.e., the term x(i) could represent the position of car i and x(j) the position of car j. Similarly, the term v(i) could represent the velocity of car i and a(i) its acceleration. These terms have sort R, whereas a term l(i) that represents the car in front of car i has sort C. Unlike in ﬁrst-order logic, the interpretation of function symbols can change when transitioning from one state to the other while following the dynamics of a distributed hybrid system. The value of position x(i) will change over time as car i drives down the street. The value of x(i) would also change if the argument term i changes its value and now refers to a diﬀerent car than before. Even objects may appear or disappear as the distributed hybrid system evolves. We use function symbol (·) to distinguish between objects i that actually exist ( (i) = 1) and those that have not been created yet or exist no ∃ ∃

8

´ ANDRE PLATZER

longer ( (i) = 0), depending on the value of (i), which may also change its interpretation from state to state. We use 0, 1, +, −, · with the usual notation and ﬁxed semantics for nonlinear real arithmetic. Divisions can be added when guarding against divisions by zero [Pla08a]. For n ≥ 0 we abbreviate f (s1 , . . . , sn ) by f (s) using vectorial notation and we use s = t for component-wise equality. Formulas. The formulas of QdL are deﬁned as in ﬁrst-order dynamic logic plus many-sorted ﬁrst-order logic . Deﬁnition 3.1. (QdL formulas).The formulas of QdL are deﬁned by the following grammar (φ, ψ are formulas, θ1 , θ2 are terms of the same sort, i is a variable of sort C, and α is a QHP as deﬁned in Section 3.2): φ, ψ ::= θ1 = θ2 | θ1 ≥ θ2 | ¬φ | φ ∧ ψ | ∀i : C φ | ∃i : C φ | [α]φ | α φ We use standard abbreviations to deﬁne ≤, >, <, ∨, →. Sorts C = R have no ordering and only θ1 = θ2 is allowed, not θ1 ≥ θ2 . For sort R, we abbreviate ∀x : R φ by ∀x φ and ∃x : R φ by ∃x φ. In the following, all formulas and terms have to be well-typed. For instance, x(i) = l(i) is no formula if x has type C → R and l has type C → C for a sort C = R or if i has a sort D = C. QdL formula [α]φ expresses that all states reachable by QHP α satisfy formula φ. Likewise, α φ expresses that there is at least one state reachable by α for which φ holds. For short notation, we allow conditional terms of the form if φ then θ1 else θ2 ﬁ (where θ1 and θ2 have the same sort). This term evaluates to θ1 if the formula φ is true and to θ2 otherwise. We generally consider formulas with conditional terms as abbreviations, e.g., ψ(if φ then θ1 else θ2 ﬁ) abbreviates (φ → ψ(θ1 )) ∧ (¬φ → ψ(θ2 )). Conditional terms can be understood as an additional operator for terms and formulas as well. Example. A major challenge in distributed car control systems [HESV91] is that they do not follow ﬁxed, static setups. Instead, new situations can arise dynamically that change structure and dimension of the system whenever new cars appear on the road from onramps or leave it; see Fig. 1. As a running example, we model a distributed car control system DCCS . First, we consider desirable QdL properties of the system DCCS for which we will later develop a series of increasingly more realistic models as QHPs. If i is a term of type C (for cars), let x(i) denote the position of car i, v(i) its current velocity, and a(i) its current acceleration; see Fig. 1. A car control system is collision-free at a state if all cars are at diﬀerent positions, i.e., ∀i=j : C x(i)=x(j). Without a quantiﬁer we could not describe that all cars on a highway are in a collision-free state, because there is a large number of cars on the highway and we may not know how many. The car control system is globally collision-free if it will always stay collision-free. The following QdL formula expresses that the system DCCS controls cars in a way that is always collision-free: (∀i, j : C M(i, j)) → [DCCS] ∀i=j : C x(i)=x(j) (3.1) It says that cars following the distributed hybrid systems dynamics of DCCS are always collision-free (postcondition), provided that DCCS starts in an initial state satisfying a formula M(i, j) for all cars i, j (precondition). In particular, the modality [DCCS] expresses that all states reachable by following the distributed hybrid system DCCS satisfy the postcondition ∀i=j : C x(i)=x(j). The simple-most choice for the formula M(i, j) in

∃

∃

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

9

the precondition is a formula that characterizes a simple compatibility condition: for different cars i = j, the car that is further down the road (i.e., with greater position) neither moves slower nor accelerates slower than the other car, i.e.: M(i, j) ≡ i = j → (x(i) < x(j) ∧ v(i) ≤ v(j) ∧ a(i) ≤ a(j)) ∨ (x(i) > x(j) ∧ v(i) ≥ v(j) ∧ a(i) ≥ a(j)) (3.2) Even though this monotonicity condition is not the only safe choice for M(i, j), some precondition like ∀i, j : C M(i, j) is necessary, because car control is unsafe if the cars start with incompatible velocities or acceleration choices initially. In fact, we may suspect that a corresponding condition like this may have to hold all the time for the system to remain safe. The car controllers will thus have to make sure they maintain ∀i, j : C M(i, j) always. And formal veriﬁcation will have to make sure that formula (3.1) is actually valid for the appropriate choices of DCCS . How do we design the distributed hybrid system DCCS that satisﬁes the QdL formula (3.1)? What is an appropriate model for distributed hybrid systems? How can we then prove that (3.1) is true? Next, we introduce QHPs as a general model for distributed hybrid systems and then discuss possible choices of QHPs for DCCS . The reader should note that more sophisticated combinations of nested quantiﬁers and modalities are possible with QdL as well. 3.2. Quantiﬁed Hybrid Programs. As a formal model for distributed hybrid systems, we introduce quantiﬁed hybrid programs (QHPs). These are regular programs from dynamic logic [HKT00] to which we add quantiﬁed assignments and quantiﬁed diﬀerential equation systems for distributed hybrid dynamics. From these quantiﬁed assignments and quantiﬁed diﬀerential equations, QHPs are built like a Kleene algebra with tests [Koz97]. Deﬁnition 3.2. (Quantified hybrid programs).QHPs are deﬁned by the following grammar (α, β are QHPs, i a variable of sort C, f is a function symbol, s is a vector of terms with sorts compatible to the arguments of f , θ is a term with sort compatible to the result of f , and χ is a formula of many-sorted ﬁrst-order logic): α, β ::= ∀i : C f (s) := θ | ∀i : C f (s) = θ & χ | ?χ | α ∪ β | α; β | α∗ In order to simplify technical diﬃculties, we impose regularity assumptions on f (s) in quantiﬁed assignments and quantiﬁed diﬀerential equations. We assume s to be either a vector of length 0 or that the mapping from the quantiﬁed variable i to s is injective. That is, each value of s can be exhibited by at most one choice of i. A system is injective, e.g., when at least one component of s is the quantiﬁed variable i. These assumptions can be relaxed, but are suﬃcient for our purposes; see Section 4 for a discussion of injectivity. For quantiﬁed diﬀerential equations, we further assume that f is an R-valued function symbol so that derivatives can be deﬁned. Quantiﬁed State Change. The eﬀect of quantiﬁed assignment ∀i : C f (s) := θ is an instantaneous discrete jump assigning θ to f (s) simultaneously for all objects i of sort C. Hence all f (s) that are aﬀected by ∀i : C f (s) := θ will change their value to the respective θ simultaneously for all choices of i in a single discrete instant of time. Usually, i occurs in term θ, but does not have to. The eﬀect of quantiﬁed diﬀerential equation ∀i : C f (s) = θ & χ is a continuous evolution where, for all objects i of sort C, all differential equations f (s) = θ hold at the same time and formula χ holds throughout the

10

´ ANDRE PLATZER

evolution (the state always remains in the region described by χ, i.e., the evolution stops at any arbitrary time before it leaves χ). Again, i usually occurs in term θ. For the trivial evolution domain restriction χ ≡ true, which is always satisﬁed, we also write ∀i : C f (s) = θ instead of ∀i : C f (s) = θ & true. 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 deﬁned, we assume f is an R-valued function symbol. Although our approach can be extended, we assume that f does not occur in s. The most common choice of s in quantiﬁed assignments and quantiﬁed diﬀerential equations is just i. Other choices are possible for s, e.g., s = (i, f (i)) 1 in ∀i : C d(i, f (i)) := 2 a(i) + 1 a(f (i)). The latter QHP could be used to model that, for 2 each car i, the average acceleration of a car i and its follower f (i) is assigned to a data ﬁeld d(i, f (i)) that car i and its follower use to determine their safe distance. Time itself is not special but implicit. If a clock variable t is needed in a QHP, it can be axiomatized by t = 1, which is equivalent to ∀i : C t = 1 where i does not occur in t. For such vacuous quantiﬁcation (i does not occur anywhere), we may omit ∀i : C from assignments and diﬀerential equations, which are then classical assignments and ordinary diﬀerential equations. Similarly, we may omit vectors s of length 0. Regular Programs. The test action ?χ is used to deﬁne conditions. Its eﬀect is that of a no-op if the formula χ is true in the current state; otherwise, like abort, it allows no transitions. That is, if the test succeeds because formula χ holds in the current state, then the state does not change, and the system execution continues normally. If the test fails because formula χ does not hold in the current state, then the system execution cannot continue, is cut oﬀ and not considered any further. The nondeterministic choice α ∪ β, sequential composition α; β, and nondeterministic repetition α∗ of programs are as in regular expressions but generalized to a semantics in distributed hybrid systems. Nondeterministic choice α ∪ β is used to express behavioral alternatives between the transitions of α and β. That is, the QHP α ∪ β can choose nondeterministically to follow the transitions of QHP α, or, instead, to follow the transitions of QHP β. The sequential composition α; β says that the QHP β starts executing after QHP α has ﬁnished (β never starts if α does not terminate). In α; β, the transitions of α take eﬀect ﬁrst, until α terminates (if it does), and then β continues. Observe that, like repetitions, continuous evolutions within α can take more or less time, which causes uncountable nondeterminism. This nondeterminism is inherent in distributed hybrid systems, because they can operate in so many diﬀerent ways, which is as such reﬂected in QHPs. Nondeterministic repetition α∗ is used to express that the QHP α repeats any number of times, including zero times. When following α∗ , the transitions of QHP α can be repeated over and over again, any nondeterministic number of times (≥0). QHPs (with their semantics and our proof rules) can be extended to systems of quantiﬁed diﬀerential equations, systems of simultaneous assignments to multiple functions f, g, and statements with multiple quantiﬁers (∀i : C ∀j : D . . . ). This includes the quantiﬁed diﬀerential equation system ∀i : C (x(i) = v(i), v(i) = a(i)), which we can understand as a second-order quantiﬁed diﬀerential equation ∀i : C (x(i) = a(i)) or as a vectorial ﬁrst-order quantiﬁed diﬀerential equation ∀i : C z(i) = θ with z(i) = (x(i), v(i)) and θ = (v(i), a(i)); see [Pla08a] for details on how to handle vectorial diﬀerential equations. It is similarly simple to extend our approach to quantiﬁed assignments with multiple function symbols

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

11

like ∀i : C (a(i) := a(i) + 1, t(i) := 0), which is a vectorial extension that can be handled like parallel updates in programs [BP06]. Our approach can also be extended to multiple quantiﬁers like in the quantiﬁed diﬀerential equation ∀i : C ∀j : D f (i, j) = a(i) − d(i, j) or the quantiﬁed assignment ∀i : C ∀j : D d(i, j) := d(i, j) + a(i) + 1. These quantiﬁer blocks correspond to ∀i : C with a vectorial variable i and a vectorial sort C. Since these simple vectorial extensions [Pla08a, BP06] are a diversion from the logical essence of our approach, we simplify notation and do not consider these cases formally. Example. Continuous movement of position x(i) of car i with acceleration a(i) is expressed by diﬀerential equation x(i) = a(i), which corresponds to the ﬁrst-order diﬀerential equation system x(i) = v(i), v(i) = a(i) where v(i) is the velocity of car i. Simultaneous movement of all cars with their respective accelerations a(i) is expressed by the quantiﬁed differential equation ∀i : C (x(i) = a(i)) where quantiﬁer ∀i : C ranges over all cars, such that all cars co-evolve along their respective diﬀerential equations at the same time. In addition to continuous dynamics, cars have discrete control. In the following QHP, discrete and continuous dynamics interact (repeatedly because of the ∗ repetition operator): ∀i : C (a(i) := if ∀j : C far(i, j) then a else −b ﬁ); ∀i : C (x(i) = a(i))
∗

(3.3)

First, all cars i control their acceleration a(i). Each car i chooses maximum acceleration a ≥ 0 for a(i) if its distance to all other cars j is far enough (some condition far(i, j)). Otherwise, i chooses full braking −b < 0. After all accelerations have been set, all cars move continuously along ∀i : C (x(i) = a(i)). Accelerations may change repeatedly, because the repetition operator ∗ can repeat the QHP when the continuous evolution stops at any time. Note that the presence of the function argument i in x(i), v(i), a(i) is a decisive diﬀerence when comparing the QHP in (3.3) to hybrid systems and when comparing the QdL formula in (3.1) to hybrid systems properties. In hybrid systems, we are limited to using variables x, v, a of a single car. If we want to add a second car to a hybrid system model, new state variables y, w, c, new dynamics y = w, w = c, and new control need to be added for the second car. We can keep on adding any ﬁxed ﬁnite number of state variables that way, but we need to know exactly how many cars there are on the street. This does not work when we want to model and verify situations with arbitrarily many cars or in distributed car control scenarios like Fig. 1, where new cars appear or disappear during the evolution of the system. A quantiﬁed diﬀerential equation like ∀i : C (x(i) = v(i), v(i) = a(i)), for example, cannot be expressed in hybrid systems, because we do not know how many cars i ranges over. If i did range over exactly 3 cars, called 1, 2, and 3, we could replace it by x(1) = v(1), v(1) = a(1), x(2) = v(2), v(2) = a(2), x(3) = v(3), v(3) = a(3) and change notation to obtain primitive state variables x1 , v1 , a1 , x2 , v2 , a2 , x3 , v3 , a3 in an ordinary diﬀerential equation system x1 = v1 , v1 = a1 , x2 = v2 , v2 = a2 , x3 = v3 , v3 = a3 But this replacement does not work unless we know exactly how many cars are in the system. Even for systems with a ﬁxed known but large number of participants, such ﬂat representations as (non-distributed) hybrid systems are ineﬃcient, because the system dimension is exponential in the number of participants and all reasoning needs to be repeated for each participant, or even for each pair of participants (collision freedom requires each pair of cars to remain safely separated). This is why we beneﬁt from studying distributed hybrid systems.

12

´ ANDRE PLATZER

One remaining issue with QHP (3.3) is that cars could still move backwards by braking long enough. But this does not capture braking. In order to say that cars can accelerate or brake but may never move backwards, we reﬁne QHP (3.3) to the following QHP in which the evolution domain of the quantiﬁed diﬀerential equation is restricted (by &) to stay in the region v(i) ≥ 0 where each car i has a nonnegative velocity: ∀i : C a(i) := (if ∀j : C far(i, j) then a else if v(i) > 0 then −b else 0 ﬁ ﬁ); ∀i : C (x(i) = v(i), v(i) = a(i) & v(i) ≥ 0)
∗

Observe that this controller is also smarter about the acceleration choices of cars than that in (3.3). It will choose 0 for a(i) if car i does not move (v(i) = 0) but car i cannot accelerate safely either, because not all cars j are far enough away. System Structure. The communication model that QdL supports is that of shared variable communication. Suppose a car i has direct control over the acceleration of car j. Then, when i decides to brake, it could directly change the acceleration of car j as well using the QHP a(j) := a(j) − 2. In most system designs, control variables of other agents are not directly accessible but communication has to be used instead. In QdL, communication can be implemented by assigning to shared variables (delays in communication are easy to model by combining assignments with diﬀerential equations). Suppose s(i) is the data ﬁeld that car i queries periodically to track how much distance it is supposed to maintain relative to its leader car. Then the QHP ∀i : C s(f (i)) := s(f (i)) + 10 would cause each car i to tell its respective follower car f (i) to increase the safety distance s(i) by 10, e.g., when the road conditions are slippery. Shared (ﬁrst-order) variables are suﬃcient to model discrete structural dynamics, e.g., of changing communication links. If, for example, the car f (i) following car i has left the street, car i may update its communication link to reﬂect this change in the structure of the system by running the QHP f (i) := f (f (i)) that updates the follower of i to the follower of f (i), i.e., the follower of the follower of i. Other discrete structural changes in the system and communication patterns as well as all data structures can be modeled easily, since a complete object-oriented programming language [BP06] can be deﬁned in QdL. Shared (ﬁrst-order) variables are suﬃcient to model continuous structural dynamics, since structural changes in the continuous dynamics can be modeled by quantiﬁed diﬀerential equations that change their connectivity, i.e., which parts of the quantiﬁed diﬀerential equation depend on which other parts. For example, in QHP ∀i : C (x(i) = a(i) + c(i, f (i))a(f (i))) the connectivity term c(i, f (i)) models whether or not the follower f (i) of car i has physical bumper-tobumper contact with car i, such that the acceleration a(f (i)) of car f (i) also pushes car i forwards, not just car f (i). The change of c(i, f (i)) from zero to non-zero represents a structural change in the physical dynamics structurally, because it structurally changes the eﬀect of the continuous dynamics. These examples illustrate how the discrete dynamics, continuous dynamics, and discrete and continuous structural dynamics of distributed hybrid systems with an arbitrary parametric number of participants can be modeled as a QHP. We defer the explanation of dimensional dynamics, i.e., dynamic appearance and disappearance of agents, to Section 5.

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

13

4. Semantics The QdL semantics is a constant domain Kripke semantics [FM99] with ﬁrst-order structures as states that associate total functions of appropriate type with function symbols. In constant domain, all states share the same domain for quantiﬁers. In particular, we choose to represent object creation not by changing the domain of states, but by changing the interpretation of the createdness ﬂag (i) of the object denoted by i. With (i), object creation is deﬁnable in a modular way (as we elaborate in Section 5). States. A state σ associates an (inﬁnite) set σ(C) of objects with each sort C, and it associates a function σ(f ) of appropriate type with each function symbol f , including (·). We assume (·) to have (unbounded but) ﬁnite support, i.e., each state only has a ﬁnite number of positions i at which (i) = 1. This makes sense in practice, because there is a varying and possibly large but still ﬁnite numbers of participants (e.g., cars). 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 C: all states σ, τ share the same domains σ(C) = τ (C) for C. Sorts C = D e are disjoint: σ(C) ∩ σ(D) = ∅. The set of all states is denoted by S. The state σi agrees with σ except for the interpretation of variable i, which is changed to e. Formulas. We use σ[[θ]] to denote the value of term θ at state σ, which is deﬁned as in e e ﬁrst-order logic. Especially, σi [[θ]] denotes the value of θ in state σi , i.e., in state σ with i interpreted as e. Further, ρ(α) ⊆ S × S denotes the state transition relation of QHP α, which we deﬁne below. Deﬁnition 4.1. (Semantics of QdL).The interpretation σ |= φ of QdL formula φ with respect to state σ is deﬁned inductively as: (1) σ |= (θ1 = θ2 ) iﬀ σ[[θ1 ]] = σ[[θ2 ]]; accordingly for ≥ (greater or equal). (2) σ |= φ ∧ ψ iﬀ σ |= φ and σ |= ψ; accordingly for ¬ (not). e (3) σ |= ∀i : C φ iﬀ σi |= φ for all objects e ∈ σ(C). e |= φ for some object e ∈ σ(C). (4) σ |= ∃i : C φ iﬀ σi (5) σ |= [α]φ iﬀ τ |= φ for all states τ with (σ, τ ) ∈ ρ(α). (6) σ |= α φ iﬀ τ |= φ for some τ with (σ, τ ) ∈ ρ(α). We say that φ is true at σ if σ |= φ. QdL formula φ is valid, written φ, iﬀ σ |= φ for all σ. ∃ ∃ ∃ ∃ ∃

Programs. QHPs have a compositional semantics. The semantics of a QHP is its reachability relation. Deﬁnition 4.2. (Transition semantics of QHP).The transition relation, ρ(α) ⊆ S × S, of QHP α speciﬁes which state τ ∈ S is reachable from σ ∈ S by running QHP α. It is deﬁned inductively: (1) (σ, τ ) ∈ ρ(∀i : C f (s) := θ) iﬀ state τ is identical to σ except that at each position e e e o of f : if σi [[s]] = o for some object e ∈ σ(C), then τ (f ) σi [[s]] = σi [[θ]]. If there e [[s]] = o, then all of the resulting are multiple objects e giving the same position σi states τ are reachable. (2) (σ, τ ) ∈ ρ(∀i : C f (s) = θ & χ) iﬀ there is a function ϕ:[0, r] → S for some r ≥ 0 with ϕ(0) = σ and ϕ(r) = τ satisfying the following conditions. At each time t ∈ [0, r], e state ϕ(t) is identical to σ, except that at each position o of f : if σi [[s]] = o for some object e ∈ σ(C), then, at each time ζ ∈ [0, r]:

14

´ ANDRE PLATZER

(3) (4) (5) (6)

• All diﬀerential equations hold and corresponding derivatives exist (trivial for r = 0): d (ϕ(t)e [[f (s)]]) i (ζ) = (ϕ(ζ)e [[θ]]) i dt e • The evolution domain is respected: ϕ(ζ)i |= χ. e If there are multiple objects e giving the same position σi [[s]] = o, then all of the resulting states τ are reachable. ρ(?χ) = {(σ, σ) : σ |= χ} ρ(α ∪ β) = ρ(α) ∪ ρ(β) ρ(α; β) = ρ(β) ◦ ρ(α) = {(σ, τ ) : (σ, z) ∈ ρ(α) and (z, τ ) ∈ ρ(β) for a state z} (σ, τ ) ∈ ρ(α∗ ) iﬀ there is an n ∈ N with n ≥ 0 and there are states σ = σ0 , . . . , σn = τ such that (σi , σi+1 ) ∈ ρ(α) for all 0 ≤ i < n.

The semantics is explicit change: nothing changes unless an assignment or diﬀerential equation speciﬁes how. In cases 1–2, only f changes and only at positions of the form e σi [[s]] for some interpretation e ∈ σ(C) of i. If there are multiple such e that aﬀect the same position o, any of those changes can take eﬀect by a nondeterministic choice. QHP ∀i : C x := a(i) may change x to any a(i). Hence, [∀i : C x := a(i)]φ(x) ≡ ∀i : C φ(a(i)), because that modality considers all possibilities of changing x to any a(i). In contrast, ∀i : C x := a(i) φ(x) ≡ ∃i : C φ(a(i)), because that modality considers some possibility of changing x to any a(i). Similarly, x can evolve along ∀i : C x = a(i) with any of the slopes a(i). But evolutions cannot start with slope a(c) and then switch to a diﬀerent slope a(d) later. Any choice for the quantiﬁed variable i is possible but i remains unchanged during each evolution. We call a quantiﬁed assignment ∀i : C f (s) := θ or a quantiﬁed diﬀerential equation ∀i : C f (s) = θ & χ injective iﬀ there is at most one e satisfying cases 1–2. For injective quantiﬁed assignments and injective quantiﬁed diﬀerential equations, conditions 1–2 can be simpliﬁed as follows: (1 ) (σ, τ ) ∈ ρ(∀i : C f (s) := θ) iﬀ state τ is identical to σ except that for each e ∈ σ(C): e e τ (f ) σi [[s]] = σi [[θ]]. (2 ) (σ, τ ) ∈ ρ(∀i : C f (s) = θ & χ) iﬀ there is a function ϕ:[0, r] → S for some r ≥ 0 with ϕ(0) = σ and ϕ(r) = τ such that for each e ∈ σ(C) and each time ζ ∈ [0, r]: • All diﬀerential equations hold and corresponding derivatives exist (trivial for r = 0): d (ϕ(t)e [[f (s)]]) i (ζ) = (ϕ(ζ)e [[θ]]) i dt e • The evolution domain is respected: ϕ(ζ)i |= χ. We call quantiﬁed assignments and quantiﬁed diﬀerential equations schematic iﬀ s is i (thus injective) and the only arguments to function symbols in θ are i. Schematic quantiﬁed differential equations like ∀i : C f (i) = a(i) & χ are very common, because distributed hybrid systems often have a family of similar diﬀerential equations replicated for multiple participants i. Their synchronization often comes from discrete communication on top of their continuous dynamics. Physically coupled diﬀerential equations are possible as well. They correspond to continuous physical interactions, e.g., if a car bumps into another car from the side, it radically changes the structure of the diﬀerential equations that determine its movement. Either case can be represented in QHPs, even if the schematic case is more common.

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

15

Cases 1–2 can be deﬁned accordingly for vectorial extensions. These vectorial extensions are simple, just notationally cumbersome. For quantiﬁed assignments to multiple function symbols like in ∀i : C (f (s) := θ, g(t) := ϑ) all changes to f and g according to case 1 are performed simultaneously when transitioning from state σ to τ [Pla08a, Pla10a, R¨m06]. u The only diﬀerence to the sequential composition (∀i : C f (s) := θ); (∀i : C g(t) := ϑ) is that in the quantiﬁed assignment to multiple functions, the change is simultaneous, hence t and ϑ are evaluated in the original state σ, not in the intermediate state that is reached after f has already been modiﬁed by ∀i : C f (s) := θ. For quantiﬁed diﬀerential equation systems with multiple function symbols like in ∀i : C (Df (s) = θ, g(t) = ϑ & χ) the changes to f and g according to case 2 are again simultaneous and all diﬀerential equations of the diﬀerential equation system need to hold at the same time. Multiple quantiﬁers like ∀i : C ∀j : D in the quantiﬁed diﬀerential equation and quantiﬁed assignment are vectorial, i.e., “for some object e ∈ σ(C)” in cases 1–2 is replaced by “for some object e ∈ σ(C) and some object e e c ∈ σ(D)”, which are for i and j, respectively. That is, we replace σi with σi c and ϕ(t)e i j with ϕ(t)e c as well as ϕ(ζ)e with ϕ(ζ)e c in cases 1–2. ij i ij Note that existence/uniqueness theorems for solutions of diﬀerential equations [Wal98] carry over to quantiﬁed diﬀerential equations. In particular, existence/uniqueness of solutions by Picard-Lindel¨f / Cauchy-Lipschitz theorem [Wal98, Theorem 10.VI] and by Peano o theorem [Wal98, Theorem 10.IX] carry over to case 2 of the semantics ρ(α) if it only aﬀects a ﬁnite subdomain of σ(C), because the quantiﬁer then corresponds to a ﬁnite set of classical diﬀerential equations. (The number of diﬀerential equations may still change dynamically over time, though, so that the quantiﬁed diﬀerential equation system cannot be replaced with an unquantiﬁed diﬀerential equation system in the QHP). For inﬁnite σ(C), the theorems carry over to schematic ∀i : C f (i) = θ & χ, which give an (inﬁnite) set of disconnected classical diﬀerential equations. In all these cases, Picard-Lindel¨f’s theorem implies that o the solution is unique, when terms are continuously diﬀerentiable (on the open domain where divisors are non-zero). For an overview of results about general inﬁnite-dimensional diﬀerential equations, see [Bog95]. 5. Actual Existence and Object Creation Up to now, we have been neglecting the eﬀects of object creation and just pretended that the domain of objects would never change. In this section, we consider object creation and distinguish objects that actually exist physically from those that have not been created yet (or are not physically present in the part of the world reﬂected in the model). We will see that this distinction does not require any change of QdL. It is just a conceptual change of our understanding. Actual Existence. For the QdL semantics, we chose constant domain semantics, i.e., all states share the same domains. Thus quantiﬁers range over all possible objects (possibilist quantiﬁcation in constant domain semantics) not just over active existing objects (actualist quantiﬁcation in varying domain semantics) [FM99]. In order to distinguish between actual objects that exist in a state, because they have already been created and can now actively take part in its evolution, versus possible objects that still passively await creation, we use function symbol (·). Function symbol (·) is similar to existence predicates in ﬁrst-order modal logic [FM99], except that its value can be assigned to in QHPs. ∃ ∃

16

´ ANDRE PLATZER

Object Creation. For a term i of type C = R, we use (i) = 1 to represent that the object denoted by i has been created and actually exists. We use (i) = 0 to represent that i has not been created or does not exist any longer. Object creation amounts to changing the interpretation of (i). For an object denoted by i that has not been created ( (i) = 0), object creation corresponds to the state change caused by assignment (i) := 1. With quantiﬁed assignments and function symbols, object creation is deﬁnable by a QHP: n := new C ≡ (∀j : C n := j); ?( (n) = 0); ∃ ∃ (n) := 1 This QHP assigns an arbitrary j of type C to n (∀j : C n := j) that did not exist before (subsequent test ? (n) = 0) and adjusts existence ( (n) := 1). Disappearance of object i corresponds to (i) := 0. Our choice of constant domain semantics avoids semantic subtleties of varying domains about the meaning of free variables denoting non-existent objects as in free logics [FM99]. Denotation is standard in QdL. Terms may just denote objects that have not been activated yet. This is even useful to initialize new objects (e.g., x(n) := 8) before activation ( (n) := 1). Actualist Quantiﬁers. We deﬁne abbreviations for actualist quantiﬁers in formulas, quantiﬁed assignments, and quantiﬁed diﬀerential equations that range only over previously created objects, similar to relativization in modal logic [FM99] by masking: ∀i : C! φ ≡ ∀i : C ( (i) = 1 → φ) ∃i : C! φ ≡ ∃i : C ( (i) = 1 ∧ φ) ∀i : C! f (s) := θ ≡ ∀i : C f (s) := (if (i) = 1 then θ else f (s) ﬁ) ∀i : C! f (s) = θ ≡ ∀i : C f (s) = (if (i) = 1 then θ else 0 ﬁ) ≡ ∀i : C f (s) = (i)θ The ﬁrst two cases deﬁne quantiﬁers for actually existing objects. The last two cases deﬁne quantiﬁed state change for actually existing objects using conditional terms that choose eﬀect θ if (i) = 1 and choose no eﬀect, retaining the old value f (s) or evolving with slope 0, if (i) = 0. The conditional terms can be avoided as indicated in the last column of the last row (similarly for quantiﬁed assignments). In all cases, the notation C! signiﬁes that the quantiﬁer domain is restricted to actually existing objects of type C. Hence, ∀i : C ranges over all objects of sort C, existent or not, whereas ∀i : C! ranges only over those objects of sort C that actually exist in the current state. We generally assume that QHPs involve only quantiﬁed assignments and diﬀerential equations that are restricted to created objects, because real systems only aﬀect objects that are physically present, not those that will be created later. We still treat actualist quantiﬁcation over C! as a deﬁned notion, in order to simplify the semantics and proof calculus by separating object creation from quantiﬁed state change rules in a modular way. If only ﬁnitely many objects have been created in the initial state (say 0), then it is easy to see that only ﬁnitely many new objects will be created with ﬁnitely many such QHP transitions, because each quantiﬁed state change for C! only ranges over a ﬁnite domain then. Recall that we assume (·) to have (unbounded but) ﬁnite support, i.e., each state only has a ﬁnite number of positions i at which (i) = 1. This makes sense in practice, because there is a varying and possibly large but still ﬁnite numbers of participants (e.g., cars). ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ (5.1)

∃

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

17

Example. The car control examples in Section 3 were unaware of the distinction between actual existing and possible objects. Car control, of course, only aﬀects created cars that are physically present, not the possible cars that have not been built yet or that are not present yet. To reﬂect this, the dynamics and properties, we only need to replace each occurrence of ∀i : C with ∀i : C! in the car control examples of Section 3. For instance the QdL formula (3.1) will be restricted to actual cars by adding C! as follows: (∀i, j : C! M(i, j)) → [DCCS] ∀i=j : C! x(i)=x(j) (5.2) In the precondition, we only demand that all cars that actually exist (∀i, j : C! . . . ) start from compatible positions with compatible velocities and accelerations, because we do not care about non-existent cars. In the postcondition, we only guarantee that all existing cars are at diﬀerent positions, because we cannot really say what happens with cars that do not yet exist and that are beyond our control. The controller and dynamics in the QHP DCCS can be restricted to actual cars in the same way, e.g., in the following variant of (3.3): ∀i : C! (a(i) := if ∀j : C! far(i, j) then a else −b ﬁ); ∀i : C! (x(i) = a(i))
∗

(5.3)

Except conceptually, this restriction to created cars does not really aﬀect the speciﬁcation (nor its veriﬁcation). This gets much more involved as soon as we create new objects at runtime or let them disappear again. When we create a new car that joins the system, or when a new car appears from an on-ramp (Fig. 1), then one more set of positions x(n), velocities v(n), and accelerations a(n) comes out of nowhere and starts evolving along with the distributed car control dynamics. That new car n has not even been considered in the dynamics before it has been created. A real system cannot control what is not part of the system yet and thus must deal with new agents dynamically whenever they arrive. A fairly challenging feature of distributed car control, thus, is that new cars may appear dynamically from on-ramps (Fig. 1) changing the set of active objects dynamically at runtime. To model this, we consider the following QHP: DCCS ≡ (n := new C; ?∀i : C! M(i, n); ∀i : C! (x(i) = a(i)))
∗

(5.4)

Before following the continuous dynamics, this QHP creates a new car n at an arbitrary position x(n) satisfying compatibility condition M(i, n) with respect to all other created cars i. Hence DCCS allows new cars to appear, but not drop right out of the sky in front of a fast car or run at the speed of light only 2 meters away. When cars appear into the horizon from on-ramps, this condition captures that a car is only allowed to join the lane (“appear” into the model world) if it cannot cause a crash with other existing cars (Fig. 1). Unboundedly many cars may appear during the operation of DCCS and change the system dimension arbitrarily, because of the repetition operator ∗ . DCCS is simple but shows how properties of distributed hybrid systems can be expressed in QdL. Joint dynamics of multiple components corresponds to compositions of quantiﬁed diﬀerential equation systems, quantiﬁed assignments, and object (dis)appearance. Structural dynamics corresponds to assignments to function terms. Say, f (i) is the car registered by communication as the car following car i. Then a term d(i, f (i)), which denotes the minimum safety distance negotiated between car i and its follower, is a crucial part of the system dynamics. Restructuring the system in response to lane change corresponds to assigning a new value to f (i), which impacts the value of d(i, f (i)) in the system dynamics.

18

´ ANDRE PLATZER

[α]φ ∧ [β]φ [α][β]φ χ→ψ ([;]) ([?]) [α ∪ β]φ [α; β]φ [?χ]ψ α φ∨ β φ α β φ χ∧ψ (∪) (;) (?) α∪β φ α; β φ ?χ ψ ˜≤t [∀i : C f (s) := ys (t)]χ) → [∀i : C f (s) := ys (t)]φ ˜ ∀t≥0 (∀0≤t 1 ([ ]) [∀i : C f (s) = θ & χ]φ ˜ ˜ ∃t≥0 (∀0≤t≤t ∀i : C f (s) := ys (t) χ) ∧ ∀i : C f (s) := ys (t) φ 1 ( ) ∀i : C f (s) = θ & χ φ if ∃i : C s = [A]u then ∀i : C (s = [A]u → φ(θ)) else φ(f ([A]u)) ﬁ 2 ([:=]) φ([∀i : C f (s) := θ]f (u)) if ∃i : C s = A u then ∃i : C (s = A u ∧ φ(θ)) else φ(f ( A u)) ﬁ 2 ( := ) φ( ∀i : C f (s) := θ f (u)) ∀j : C φ(θ) Υ ([∀i : C f (s) := θ]u) 3 ∃j : C φ(θ) ([:∗]) ([:]) ( :∗ ) [∀i : C f (s) := θ]Υ (u) [∀j : C n := θ]φ(n) ∀j : C n := θ φ(n) true ( ) ∃n : C (n) = 0 Γ→φ(θ), ∃x : C φ(x), ∆ 4 Γ→φ(f (X1 , . . , Xn )), ∆ 5 (∃r) (∀r) Γ→∃x : C φ(x), ∆ Γ→∀x : C φ(x), ∆ Γ, φ(θ), ∀x : C φ(x)→∆ 4 Γ, φ(f (X1 , . . , Xn ))→∆ 5 (∀l) (∃l) Γ, ∀x : C φ(x)→∆ Γ, ∃x : C φ(x)→∆ ([∪]) (i∀) QE(∀X, Y (if s = t then Φ(X)→Ψ(X) else Φ(X)→Ψ(Y ) ﬁ)) 6 Φ(f (s))→Ψ(f (t)) ∃ ∃ QE(∃X i (Φi →Ψi )) 7 Φ1 →Ψ1 . . . Φn →Ψn φ→[α]φ (ind) Γ, φ→[α∗ ]φ, ∆ (i∃)

φ→ψ φ→ψ ( gen) Γ, [α]φ→[α]ψ, ∆ Γ, α φ→ α ψ, ∆ v > 0 ∧ ϕ(v) → α ϕ(v − 1) 8 (con) Γ, ∃v ϕ(v)→ α∗ ∃v≤0 ϕ(v), ∆ ([]gen)

1t, t are new logical variables and y (t) the simultaneous solutions of the (injective) diﬀerential equations ˜ s ∀i : C f (s) = θ with f (s) as symbolic initial values. 2The occurrence of f (u) in φ(f (u)) is not in scope of a modality (admissible substitution) and we abbreviate assignment ∀i : C f (s) := θ by A, which is assumed to be injective. 3f = Υ and the quantiﬁed assignment ∀i : C f (s) := θ is injective. The same rule applies for ∀i : C f (s) := θ instead of [∀i : C f (s) := θ]. 4θ is an arbitrary term of sort C, often a new logical variable X. 5f is a new (Skolem) function of appropriate type and X , . . , X are all free logical variables of ∀x φ(x). 1 n 6X, Y are new logical variables of sort R. QE needs to be applicable to the formula in the premise. 7among all branches, the free (existential) logical variable X of sort R only occurs in the branches Φ →Ψ . i i QE needs to be deﬁned for the formula in the premise, especially, no Skolem dependencies on X occur. 8logical variable v does not occur in α.

Figure 2: Rule schemata of the proof calculus for quantiﬁed diﬀerential dynamic logic.

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

19

(¬r)

Γ, φ→∆ Γ→φ, ψ, ∆ Γ→φ, ∆ Γ→ψ, ∆ Γ, φ→ψ, ∆ (∨r) (∧r) (→r) Γ→¬φ, ∆ Γ→φ ∨ ψ, ∆ Γ→φ ∧ ψ, ∆ Γ→(φ → ψ), ∆ Γ→φ, ∆ Γ, φ→∆ Γ, ψ→∆ Γ, φ, ψ→∆ Γ→φ, ∆ Γ, ψ→∆ (¬l) (∨l) (∧l) (→l) Γ, ¬φ→∆ Γ, φ ∨ ψ→∆ Γ, φ ∧ ψ→∆ Γ, (φ → ψ)→∆ Γ, φ→φ, ∆ (cut) Γ→φ, ∆ Γ, φ→∆ Γ→∆ Figure 3: Propositional rule schemata 6. Proof Calculus

(ax)

In Fig. 2, we present a proof calculus for QdL formulas. The basic principle behind the proof rules is that they transform a QHP into structurally simpler logical formulas by symbolic decomposition. For our purposes, it is suﬃcient to understand the sequent notation informally, just for a systematic proof structure. With ﬁnite sets of formulas for the antecedent Γ and succedent ∆, sequent Γ→∆ is an abbreviation for the formula φ∈Γ φ → ψ∈∆ ψ. Our calculus uses standard proof rules for propositional logic with the cut rule; see Fig. 3. The proof rules are used backwards from the conclusion (goal below horizontal bar) to the premises (subgoals above bar). In the QdL calculus, we use substitutions that take eﬀect within formulas and programs (deﬁned as usual). Only admissible substitutions are applicable, however, which is crucial for soundness. An application of a substitution σ is admissible if no replaced term θ occurs in the scope of a quantiﬁer or modality binding a symbol in θ or in its replacement σθ. A modality binds a symbol f iﬀ it contains an assignment to f (like ∀i : C f (s) := θ) or a diﬀerential equation containing an f (s) (like ∀i : C f (s) = θ). The substitutions in Fig. 2 that insert a term θ into φ(θ) also have to be admissible for the proof rules to be applicable. We explain the QdL proof rules in the sequel. Regular Rules. The ﬁrst proof rules in Fig. 2 axiomatize sequential compositions ([;], ; ), nondeterministic choices ([∪], ∪ ), and tests ([?], ? ) of regular programs as in dynamic logic [HKT00]. Like most other rules in Fig. 2, these rules do not contain sequent symbol →, i.e., they can be applied to any subformula. These rules represent (directed) equivalences: conclusion and premise are equivalent. The equivalences are directed in the sense that we only use them to replace occurrences of the conclusion with the premise (which is structurally simpler), not the other way around. Nondeterministic choices split into their alternatives ([∪], ∪ ). For rule [∪]: If all α transitions lead to states satisfying φ (i.e., [α]φ holds) and all β transitions lead to states satisfying φ (i.e., [β]φ holds), then, all transitions of QHP α ∪ β, which choose between following α and following β, also lead to states satisfying φ (i.e., [α ∪ β]φ holds). Dually for rule ∪ , if there is an α transition to a φ state ( α φ) or a β-transition to a φ state ( β φ), then, in either case, there is a transition of α ∪ β to φ ( α ∪ β φ holds), because α ∪ β can choose which of those transitions to follow. A general principle behind the QdL proof rules is most noticeable in [∪], ∪ : these proof rules symbolically decompose the reasoning into two separate parts and analyze the fragments α and β separately, which makes the problem tractable and is good for scalability. For these symbolic structural decompositions, it is very helpful that QdL is a full logic that is closed under all logical operators, including

20

´ ANDRE PLATZER

disjunction and conjunction, for then the premises in [∪], ∪ are QdL formulas again (unlike in Hoare logic [Hoa69]). Sequential compositions are proven using nested modalities ([;], ; ). For rule [;]: If after all α-transitions, all β-transitions lead to states satisfying φ (i.e., [α][β]φ holds), then also all transitions of the sequential composition α; β lead to states satisfying φ (i.e., [α; β]φ holds). The dual rule ; uses the fact that if there is an α-transition, after which there is a β-transition leading to φ (i.e., α β φ), then there is a transition of α; β leading to φ (that is, α; β φ), because the transitions of α; β are just those that ﬁrst do any α-transition, followed by any β-transition (Section 4). Again, it is crucial that QdL is a full logic that considers reachability statements as modal operators, which can be nested, for then the premises in [;], ; are QdL formulas again (unlike in Hoare logic [Hoa69]). Tests are proven by assuming (with an implication in rule [?]) or showing (with a conjunction in rule ? ) that the test succeeds, because test ?χ can only make a transition when condition χ actually holds true (Section 4). Thus, for QdL formula ?χ φ, rule ? is used to prove that formula χ holds true (otherwise there is no transition and thus the reachability property is false) and that formula φ holds after the resulting no-op. Dually, rule [?] for QdL formula [?χ]φ assumes that formula χ holds true (otherwise there is no transition and thus nothing to show) and shows that φ holds after the resulting no-op. Quantiﬁed Diﬀerential Equations. Rules [ ], handle continuous evolutions for quantiﬁed diﬀerential equations with ﬁrst-order deﬁnable solutions. Given a solution for the quantiﬁed diﬀerential equation system with symbolic initial values f (s), continuous evolution along diﬀerential equations can be replaced with a quantiﬁed assignment ∀i : C f (s) := ys (t) corresponding to the simultaneous solution (of the diﬀerential equations ∀i : C f (s) = θ with f (s) as symbolic initial values) and an additional quantiﬁer for the evolution time t. In rule [ ], postcondition φ needs to hold for all evolution durations t ≥ 0. In rule , it needs to hold after some duration t ≥ 0. The constraint on χ restricts the continuous evo˜ lution such that its solution f (s) := ys (t) remains in the evolution domain region χ at all ˜ intermediate times t ≤ t. This constraint simpliﬁes to true if χ is true. For schematic cases like ∀i : C f (i) = a(i), ﬁrst-order deﬁnable solutions can be obtained by adding argument i to ﬁrst-order deﬁnable solutions of the deparametrized version f = a. For example, the following proof step uses rule [ ] to turn a quantiﬁed diﬀerential equation system into a quantiﬁed assignment with an extra quantiﬁer for the duration t of the evolution.
b ∀i=j x(i)=x(j) →∀t≥0 [∀i x(i) := − 2 t2 + v(i)t + x(i)] ∀j=k x(j)=x(k) []

∀i=j x(i)=x(j) →[∀i x(i) = v(i), v(i) = −b] ∀j=k x(j)=x(k)

b The quantiﬁed assignment ∀i x(i) := − 2 t2 + v(i)t + x(i) solving the above quantiﬁed diﬀerb ential equation system can be obtained easily from the solution x := − 2 t2 + vt + x of the deparametrized diﬀerential equation system x = v, v = −b, just by adding the parameter i back in and checking whether this gives a solution. We only present proof rules for ﬁrst-order deﬁnable solutions of quantiﬁed diﬀerential equations here. We refer to previous work [Pla10a] for induction techniques that handle diﬀerential equations without solving them and that work for nondeterministic diﬀerential equations with disturbances. We have shown recently that these diﬀerential induction techniques extend to quantiﬁed diﬀerential equations using quantiﬁed diﬀerential invariants [Pla11].

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

21

Quantiﬁed Assignments. Rules [:=], := ,[:] handle quantiﬁed assignments. Rule [:] characterizes the fact that quantiﬁed assignments to f have no eﬀect on all other operators Υ = f (including other function symbols, ∧, if then else ﬁ), so that Υ will not be aﬀected by the quantiﬁed assignment and can be skipped over. The argument u may still be aﬀected by the quantiﬁed assignment, hence [:] preﬁxes u (component-wise) by ∀i : C f (s) := θ. Hence, the [:] rule maps a quantiﬁed assignment over all arguments homomorphically. For example, if Υ is an operator taking two arguments and is not the function symbol f , then rule [:] derives the proof step
[:]

Υ ([∀i : C f (s) := θ]u1 , [∀i : C f (s) := θ]u2 ) [∀i : C f (s) := θ]Υ (u1 , u2 )

Rules [:=], := characterize how a quantiﬁed assignment to f aﬀects the value of a term f (u) (these rules are equivalent for the injective case, i.e., a match for at most one i). Their eﬀect depends on whether the quantiﬁed assignment ∀i : C f (s) := θ matches f (u), i.e., there is a choice for i such that f (u) is aﬀected by the assignment, because u is of the form s for some i. Whether it matches or not cannot always be decided statically, because it may depend on the particular interpretations. Hence, the premises of rules [:=], := make a case distinction on matching by yielding an if-then-else formula. The formula if φ then φ1 else φ2 ﬁ is short notation for (φ → φ1 ) ∧ (¬φ → φ2 ). If the quantiﬁed assignment does not match (else part), the occurrence of f in φ(f (u)) will be left unchanged, because f is not changed at position u. If it matches (then part), the premise uses the term θ assigned to f (s) instead of f (u), either for all possible i : C that match f (u) in case of [:=], or for some of those i : C in case of := . The universal and existential quantiﬁers pick the same unique i, because the quantiﬁed assignment needs to be injective for [:=], := . In all cases, the original quantiﬁed assignment ∀i : C f (s) := θ, which we abbreviate by A, will be applied to u in the premise, because the value of argument u may also be aﬀected by A, recursively. A special case of [:=] applies to the schematic case where s is of the form i, which matches trivially: ∀i : C (i = [∀i : C f (i) := θ]u → φ(θ)) [:=] φ([∀i : C f (i) := θ]f (u)) If f does not occur in u, then [:] simpliﬁes this proof step further: ∀i : C (i = u → φ(θ)) φ([∀i : C f (i) := θ]f (u)) u is the term θ with i replaced by u. Standard ﬁrst-order reasoning simpliﬁes Recall that θi the above to a derived rule that we again denote by [:=] (where f does not occur in u)
[:=],[:] [:=] u φ(θi ) φ([∀i : C f (i) := θ]f (u))

Together with [:] to propagate the change to both arguments of =, this derived rule proves, for example, the following proof step:
b b ∀i=j x(i)=x(j) →∀j=k (− 2 s2 + v(j)s + x(j) = − 2 s2 + v(k)s + x(k)) [:=],[:] b ∀i=j x(i)=x(j) →∀j=k [∀i x(i) := − 2 s2 + v(i)s + x(i)] x(j)=x(k)

Rules [:=], := ,[:] also apply for assignments without quantiﬁers, which correspond to vacuous quantiﬁcation ∀i : C where i does not occur anywhere. The following rule, for

22

´ ANDRE PLATZER

example, is a special case of [:=]
if s = [f (s) := θ]k then φ(θ) else φ(f ([f (s) := θ]k)) ﬁ
[:=]

φ([f (s) := θ]f (k))
if s = k then φ(θ) else φ(f (k)) ﬁ
[:=]

If f does not occur in term k, then this special case of [:=] simpliﬁes further to φ([f (s) := θ]f (k))

Note that the if-then-else case distinction is necessary in general, because the eﬀect of the (vacuously quantiﬁed) assignment depends on whether s = k holds, which may depend on what value k has at the moment. Rules [:∗], :∗ reduce nondeterministic assignments to universal or existential quantiﬁcation. For the handling of other general nondeterministic assignments and nondeterministic diﬀerential equations, also see previous work [Pla10a]. It is easy, just notationally cumbersome, to extend rules [:=], := ,[:] to vectorial extensions including systems of quantiﬁed assignments to multiple function symbols like ∀i : C (a(i) := a(i) + 1, t(i) := 0) following the ideas of parallel updates [BP06, R¨m06]. u With those, it is also easy to extend rules [ ], to quantiﬁed diﬀerential equation systems like ∀i : C (x(i) = v(i), v(i) = a(i)) where the solution is a system of quantiﬁed assignments. Object Creation. Given our deﬁnition of new C as a QHP from Section 5, object creation can be proven by the other proof rules in Fig. 2. With this deﬁnition of new C, we obtain, for example, the following derived rule using [;],[:∗],[?] ∀n : C ( (n) = 0 → [ (n) := 1]φ) [n := new C]φ In addition, axiom expresses that, for sort C = R, there always is a new object n that has not been created yet ( (n) = 0), because domains are inﬁnite. This is the only place where we are using the assumption about inﬁnite domains. The primary purpose is to simplify technicalities that would arise if object creation could run out of objects and may thus fail if, e.g., no more cars can be created. If this resource limitation is intended in a particular system, it can be modeled easily using patterns like n := new C ∪ fail. Quantiﬁers. For quantiﬁers, we cannot just use standard rules [Fit96], because these are for uninterpreted ﬁrst-order logic and work by instantiating quantiﬁers, eagerly as in ground tableaux or lazily by uniﬁcation as in free variable tableaux [Fit96]. QdL is based on ﬁrstorder logic interpreted over the reals [Tar51, CH91]. A formula like ∃a : R ∀x : R (x2 + a > 0) cannot be proven by the instantiation rules for the quantiﬁers but it is still valid for reals. Thus, for handling quantiﬁers over the reals, we would like to use the standard decision procedure for ﬁrst-order real arithmetic (i.e., real-closed ﬁelds) instead, which is quantiﬁer elimination [Tar51, CH91]. Deﬁnition 6.1. (Quantifier elimination). A ﬁrst-order theory admits quantiﬁer elimination if, with each formula φ, a quantiﬁer-free formula QE(φ) can be associated eﬀectively that is equivalent (i.e., φ ↔ QE(φ) is valid) and has no additional free variables or function symbols. The operation QE is further assumed to evaluate formulas without variables, yielding a decision procedure for closed formulas of this theory (i.e., formulas without free variables). ∃ ∃ ∃ ∃

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

23

Unfortunately, we cannot use quantiﬁer elimination of the theory of real-closed ﬁelds [Tar51, CH91] either, because it cannot be applied to QdL formulas with modalities, since these are quantiﬁed reachability statements. Even in discrete dynamic logic, quantiﬁers plus modalities make validity Π1 -complete [HKT00, Theorem 13.1]. QE cannot handle sorts 1 C = R. Instead, our QdL proof rules combine quantiﬁer handling of many-sorted logic based on instantiation with theory reasoning by QE for the theory of reals. Figure 2 shows proof rules for quantiﬁers that combine with decision procedures for real-closed ﬁelds. Classical instantiation is sound for sort R, just incomplete. For example, rule ∃r can solve the following arithmetic by instantiation:
∃r

a > 0 →(a + 1)2 > a, ∃x x2 > a a > 0 →∃x x2 > a

Rules ∃r and ∀l instantiate x with arbitrary terms θ, including a new free variable X, in which case ∃r and ∀l become the usual γ-rules of free-variable proof calculi [Fit96, FM99]: Γ→φ(X), ∃x : C φ(x), ∆ Γ, φ(X), ∀x : C φ(x)→∆ (∃r) (∀l) Γ→∃x : C φ(x), ∆ Γ, ∀x : C φ(x)→∆ Rules ∀r and ∃l correspond to the liberalized δ + -rule [HS94] that is a reﬁnement of the classical δ-rule of free-variable tableaux [Fit96]. As in our previous work [Pla08a], rules i∀ and i∃ reintroduce and eliminate quantiﬁers over R once QE is applicable, because the remaining constraints are ﬁrst-order real arithmetical in the respective variables. In particular, the quantiﬁer rules can be used to postpone quantiﬁer elimination until the remaining constraints are ﬁrst-order, where the quantiﬁer can be reintroduced by i∀ and i∃ [Pla08a]. Unlike in previous work, however, functions and diﬀerent argument vectors can occur in QdL. If the argument vectors s and t in i∀ have the same value, the same variable X can be reintroduced for f (s) and f (t), otherwise diﬀerent variables X = Y have to be used. Whether s and t have the same value cannot always be decided statically, so rule i∀ makes a case distinction by an if-then-else. Rule i∀ works accordingly for multiple occurrences of f (s), f (t), f (u) and so on in arbitrary positions in the formula, where more variables X, Y, Z are introduced to quantify over. It is easy to turn rule i∀ into a rule that successively substitutes one term f (s) by a fresh variable X everywhere at a time instead of handling all f (s), f (t), f (u) at once. Rule i∃ can reintroduce an existential quantiﬁer for a free (existential) logical variable X and merges all proof branches containing X, because X has to satisfy all branches simultaneously. It thus has multiple conclusions. Rule i∃ reintroduces an existential quantiﬁer and performs quantiﬁer elimination for a free (existential) logical variable X that has been introduced by ∃r,∀l before by choosing a fresh variable X for θ. We use the same rule i∃ as in previous work and refer to that work [Pla08a] for further explanations of merging. Rules i∀ and i∃ require that quantiﬁer elimination (QE) is applicable to the resulting formula. If the resulting formulas still have occurrences of the quantiﬁed variables in the scope of modalities, then QE is not applicable and rules i∀ and i∃ have to be postponed until the modalities have been dealt with by other proof rules from Fig. 2. Even for ﬁrstorder formulas, we cannot just apply classical quantiﬁer elimination in real-closed ﬁelds [Tar51], because the ﬁrst-order theory of real-closed ﬁelds does not include function symbols. For example, ∀i (a(i) ≥ 0) is a formula of ﬁrst-order real arithmetic augmented with function symbols, hence quantiﬁer elimination in real-closed ﬁelds due to Tarski [Tar51] is

24

´ ANDRE PLATZER

not applicable. It cannot even be expressed in quantiﬁer-free form, because its truth-value depends on the value of function a at unboundedly many positions. This makes sense. QE is a decision procedure for ﬁrst-order real arithmetic. But ﬁrst-order logic (even without arithmetic) is only semidecidable, so we cannot handle it by QE and need to rely on the instantiation rules ∀r,∀l,∃r,∃l, which are complete for ﬁrst-order logic. Nevertheless, from previous work [Pla08a], we obtain the following result on how to lift QE to the presence of function symbols: Lemma 6.2. ( Quantifier elimination lifting [Pla08a]). Quantiﬁer elimination can be lifted to instances of formulas of ﬁrst-order theories that admit quantiﬁer elimination, i.e., to formulas that result from the base theory by substitution. For example, ∀y (a(i) < y 2 ) is a formula of ﬁrst-order real arithmetic augmented with function symbols such that quantiﬁer elimination in real-closed ﬁelds due to Tarski [Tar51] is not (directly) applicable. By Lemma 6.2, however, QE can be lifted to this formula, because it is an instance of ∀y (Z < y 2 ), for Z replaced with a(i). Hence, QE(∀y (a(i) < y 2 )) ≡ (QE(∀y (Z < y 2 )))Z
a(i)

≡ (Z < 0)Z

a(i)

≡ a(i) < 0

Global Rules. The proof rules in the last block of Fig. 2 depend on the truth of their premises in all states, thus the context Γ, ∆ cannot be used in the premise, because it may be speciﬁc to the current state. The rules are given in a form that best displays their underlying logical principles. The general pattern for applying these rules to prove that the succedent of their conclusion holds is to prove that both their premise and the antecedent of their conclusion hold. In particular, the antecedent can be thought of as holding in the current state, whereas the premise can be thought of as holding in all states because the context Γ, ∆ is gone. Rules []gen, gen are G¨del generalization rules and can be used to strengthen posto conditions: antecedent [α]φ is suﬃcient for proving succedent [α]ψ when postcondition φ entails ψ in all states, as shown in the premise of []gen. Clearly, for rule []gen, if all states reachable by α satisfy φ (antecedent [α]φ) and φ implies ψ in all states (premise φ→ψ), then ψ also holds in all states reachable by α (succedent [α]ψ). Similarly, for rule gen, if some state reachable by α satisﬁes φ (antecedent α φ) and φ implies ψ in all states (premise φ→ψ), then ψ also holds in some state reachable by α (succedent α ψ). Rule ind is an induction schema for loops with inductive invariant φ [HKT00, Pla08a]. Rule ind says that φ holds after any number of repetitions of α if it holds initially (antecedent) and, for all states, invariant φ remains true after one iteration of α (premise). If φ is true after executing α whenever φ has been true before (premise), then, if φ holds in the beginning, φ will continue to hold, no matter how often we repeat α in [α∗ ]φ. Similarly, con generalizes Harel’s convergence rule [HKT00] to the hybrid case with decreasing variant ϕ [Pla08a]. Rule con expresses that the variant ϕ(v) holds for some real number v ≤ 0 after repeating α suﬃciently often (succedent) if ϕ(v) holds for some real number at all in the beginning (antecedent) and, by premise, ϕ(v) can decrease after every execution of α by 1 (or another positive real constant). This rule can be used to show positive progress (by 1) with respect to ϕ(v) by executing α.

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

25

Example. As a simple example illustrating how the QdL proof calculus works, we consider the QdL derivation in Fig. 4 for a simple QdL formula. The QdL formula that we consider here follows the pattern of the running example formula in (3.1). But we simplify the formula to consider just one case and postpone the discussion of the full system to Section 9. Here we consider the QdL formula: ∀i=j x(i)=x(j) → [∀i (x(i) = v(i), v(i) = −b)] ∀j=k x(j)=x(k) (6.1) The diﬀerence of the simpler QdL formula (6.1) compared to the full QdL formula (3.1) is that the simpler formula considers only the case of the QHP dynamics where all cars are braking. Certainly, if the system would not be safe when all cars are braking (which is one possible behavior of DCCS ), then it would not be safe always. The other diﬀerence is that (6.1) has a weaker assumption in the precondition. It only assumes that cars start from diﬀerent positions (∀i=j x(i)=x(j)), not that they respect the compatibility constraint ∀i, j : C M(i, j). In fact, we are using the derivation in Fig. 4 to ﬁnd out how we need to choose M(i, j) to ensure collision freedom, because M(i, j) needs to imply at least that all cars would remain safe when braking. The derivation in Fig. 4 can be used to ﬁnd out under which circumstances the QdL formula (6.1), from which we start the derivation at the bottom of Fig. 4, is true. Formula (6.1) claims that cars would never crash if they start at diﬀerent positions (∀i=j x(i)=x(j)) and all cars brake by following the dynamics ∀i x(i) = −b. Since braking is the safest operation for cars, we might think that car control would always be safe in this most conservative scenario. But that is not the case. If the cars start with incompatible velocities and distances, then not even braking can prevent a crash. The premise discovered by the QdL derivation in Fig. 4 reveals that collisions will only be prevented by braking if the initial velocities and positions satisfy the monotonicity condition M(j, k) that we have already shown in (3.2). QE(∀X, Y, V, W (j = k ∧ X = Y → X≤Y ∧V ≤W ∨ X≥Y ∧V ≥W ))
i∀ QE i∀ ∀r [:=] [:] →r ∀r []

∀i=j x(i)=x(j) →(j=k → (x(j)≤x(k)∧v(j)≤v(k) ∨ x(j)≥x(k)∧v(j)≥v(k)))
b b ∀i=j x(i)=x(j) → QE(∀s≥0 (j=k → − 2 s2 + v(j)s + x(j) = − 2 s2 + v(k)s + x(k))) b b ∀i=j x(i)=x(j), s≥0 →(j=k → − 2 s2 + v(j)s + x(j) = − 2 s2 + v(k)s + x(k)) b b ∀i=j x(i)=x(j), s≥0 →∀j=k (− 2 s2 + v(j)s + x(j) = − 2 s2 + v(k)s + x(k)) b ∀i=j x(i)=x(j), s≥0 →∀j=k [∀i x(i) := − 2 s2 + v(i)s + x(i)] x(j)=x(k) b ∀i=j x(i)=x(j), s≥0 →[∀i x(i) := − 2 s2 + v(i)s + x(i)] ∀j=k x(j)=x(k) b ∀i=j x(i)=x(j) →(s≥0 → [∀i x(i) := − 2 s2 + v(i)s + x(i)] ∀j=k x(j)=x(k)) b ∀i=j x(i)=x(j) →∀t≥0 [∀i x(i) := − 2 t2 + v(i)t + x(i)] ∀j=k x(j)=x(k)

∀i=j x(i)=x(j) →[∀i (x(i) = v(i), v(i) = −b)] ∀j=k x(j)=x(k)

Figure 4: Example of a QdL derivation to prove collision-freedom of simple car control. The proof in Fig. 4 starts with the conjecture at the bottom (goal). The proof uses rule [ ] to turn the quantiﬁed diﬀerential equation system into a quantiﬁed assignment with an extra quantiﬁer for the duration t of the evolution. The quantiﬁed diﬀerential b equation system is easy to solve. The quantiﬁed assignment ∀i x(i) := − 2 t2 + v(i)t + x(i) b solving it can be obtained easily from the solution x := − 2 t2 + vt + x of the deparametrized

26

´ ANDRE PLATZER

diﬀerential equation system x = v, v = −b, just by adding the parameter i back in and checking that the resulting terms solve the quantiﬁed diﬀerential equation. Now the topmost logical operator in the succedent is the quantiﬁer ∀t. Even though it is a quantiﬁer over a real variable, we cannot use the decision procedure of quantiﬁer elimination for real-closed ﬁelds [Tar51] to handle it, because we do not have a formula of ﬁrst-order real arithmetic, but still a QdL formula with a modality expressing a property of all reachable states. Instead, we use rule ∀r to postpone quantiﬁer elimination and turn variable t into a Skolem function s. This Skolem function has no arguments, because no free (existential) logical variables occur in the formula [Pla08a]. After that, we use the standard propositional sequent rule →r to normalize implications in the succedent into sequent form by moving their left-hand side to the antecedent. The resulting quantiﬁed assignment to x(i) (for all i) takes eﬀect on the postcondition ∀j=k x(j) = x(k) by skipping over the quantiﬁer ∀j=k with rule [:] and then aﬀecting x(j) and x(k) subsequently by rule [:=] (and another application of [:] to skip over =, which is not shown in Fig. 4). At this point (the top-most use of rule ∀r in Fig. 4), we already have a ﬁrst-order formula and it may seem as if we could apply i∀ directly instead of ∀r. This would not work, however, because quantiﬁer elimination works from inside out and will have to eliminate the inner quantiﬁer ∀j=k before the outer quantiﬁer ∀s. Yet, the resulting formula is not an instance of ﬁrst-order real arithmetic (not even when using Lemma 6.2), because there are dependencies on the quantiﬁed variables j, k in function arguments of the resulting formula: b b ∀s≥0 ∀j=k − s2 + v(j)s + x(j) = − s2 + v(k)s + x(k) 2 2 Instead, the proof in Fig. 4 uses rule ∀r to turn the quantiﬁed variables j, k into Skolem functions, which, for simplicity, we again denote by j and k. Subsequently, we can use rule i∀ to reintroduce a quantiﬁer for the Skolem function s. Rule i∀ does not produce an if-then-else, because s has no arguments. This time, the formula is still not in ﬁrst-order real arithmetic, because function symbols like v(j) occur. However, it is an instance (v(j) for V and x(j) for X and v(k) for W and x(k) for Y ) of the following formula of ﬁrst-order real arithmetic: b b (6.2) ∀s≥0 j=k → − s2 + V s + X = − s2 + W s + Y 2 2 and thus quantiﬁer elimination can be lifted by Lemma 6.2. The result of quantiﬁer elimination is an instance (with the same instantiation as above) of the result of applying QE to (6.2). To improve traceability, we show the application of QE as a separate proof step (indicated by QE). Finally (the top-most rule), we use rule i∀ to ﬁnish the deduction. We still cannot yet use rule i∀ for j, k, but we can use rule i∀ for the (non-Skolem) function symbols x and v. This time, the use of rule i∀ is more involved than before, because the functions x and v have arguments. When using rule i∀ on ∀i=j x(i)=x(j)→(j=k → (x(j)≤x(k)∧v(j)≤v(k) ∨ x(j)≥x(k)∧v(j)≥v(k)))

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

27

we formally obtain QE ∀X, Y, V, W if j = k then j = k ∧ X = X → X≤X∧V ≤V ∨ X≥X∧V ≥V
else

j = k ∧ X = Y → X≤Y ∧V ≤W ∨ X≥Y ∧V ≥W Since the condition if j = k contradicts the assumption j = k, this formula simpliﬁes to: QE(∀X, Y, V, W (j = k ∧ X = Y → X≤Y ∧V ≤W ∨ X≥Y ∧V ≥W )) Simpliﬁcations like those arise often and can be exploited for automated theorem proving. Applying QE in the above formula yields false, so the derivation in Fig. 4 does not result in a closed proof. This is good news, however, because the conjecture at the bottom of Fig. 4 is not true under all interpretations. The constraints at the top of Fig. 4 can be used to construct the constraints required for safety, which coincide with M(j, k) from (3.2). Derived Rules. Several useful rules can be derived from the QdL rules in Fig. 2 to shortcut common reasoning cases. For instance, the following derived rules characterize the eﬀect of creating objects of type C on actualist quantiﬁers over type C! (where n is of type C): [ (n) := 1]φ(n) ∨ ∃i : C! [ (n) := 1]φ(i) [ (n) := 1]φ(n) ∧ ∀i : C! [ (n) := 1]φ(i) (ν∃) (ν∀) [ (n) := 1]∀i : C! φ(i) [ (n) := 1]∃i : C! φ(i) They commute the eﬀect [ (n) := 1] of object creation with quantiﬁcation, retaining the eﬀect on the new object explicitly. Rule ν∀ states that the new object denoted by n— which may not have been created before—needs to satisfy φ(n) too in order for ∀i : C! φ(i) to hold after (n) := 1 ensures that n is created. Dually, rule ν∃ states that created object n is an alternative choice for i, in addition to the previous domain of C!. A similar derived rule νA states that, after creating an object of type C, this created object will be aﬀected by actualist quantiﬁed assignments ranging over C!, so that commuting has to take care of the eﬀect on the new object explicitly. [∀i : C!∪{n} f (s) := θ][ (n) := 1]φ (νA) [ (n) := 1][∀i : C! f (s) := θ]φ For this situation where n is adjoined to the range of quantiﬁcation (n might even have been in the range before, so the union is not necessarily disjoint), we use the following mnemonic abbreviation in the premise of νA: ∀i : C!∪{n} f (s) := θ ≡ ∀i : C (f (s) := if i = n ∨ (i) then θ else f (s) ﬁ) Note that we cannot simply apply the assignment to n separately before ∀i : C! f (s) := θ as in i := n; f (s) := θ; ∀i : C! f (s) := θ, because that would change f twice if n already existed initially. 7. Soundness We have presented a proof calculus for QdL in Section 6. One of the most important questions about it is whether we can rely on the proofs and know that every QdL formula proven in the QdL calculus is really a valid formula. That is, the question is whether the QdL calculus is sound. An unsound calculus would be disastrous, because we could use it ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃

28

´ ANDRE PLATZER

to “prove” counterfactual properties. We need to make sure that the proof calculus ﬁts to the semantics of QdL. Indeed it does. Theorem 7.1. ( Soundness). The QdL calculus is sound: every QdL formula that can be proven in the QdL calculus is valid, i.e., true in all states. Proof. The calculus is sound if each rule instance is sound. Some of the rules of the QdL calculus are even locally sound, i.e., their conclusion is true at state σ if all its premises are true at σ, which implies soundness. The proofs for the propositional rules, and regular rules [;], ; ,[∪], ∪ ,[?], ? are as usual [Pla10b]. We refer to previous work [Pla08a, Pla10b] for the soundness proofs for ∃r,∀l,∀r,∃l,i∃, which are more involved. i∀ Rule i∀ is locally sound. For this, we assume that the premise holds, i.e., we assume σ |= QE(∀X, Y (if s = t then Φ(X)→Ψ(X) else Φ(X)→Ψ(Y ) ﬁ)). Since QE yields an equivalence, we conclude σ |= ∀X, Y (if s = t then Φ(X)→Ψ(X) else Φ(X)→Ψ(Y ) ﬁ). This is equivalent to σ |= if s = t then ∀X (Φ(X)→Ψ(X)) else ∀X, Y (Φ(X)→Ψ(Y )) ﬁ, because the fresh variables X, Y do not occur in s or t. Then we assume the antecedent of the conclusion is true, i.e., σ |= Φ(f (s)). We conclude that the succedent of the conclusion is true, σ |= Ψ(f (t)), by choosing σ[[f (s)]] for X and σ[[f (t)]] for Y in the premise. If σ |= ¬(s = t) then σ |= Ψ(f (t)) follows directly from the premise. If, otherwise, σ |= s = t, then σ |= Ψ(f (t)) also follows, because the choice σ[[f (s)]] for X is identical to the choice σ[[f (t)]] for Y in the premise. By admissibility of substitutions, any variables occurring in terms s and t are free at all occurrences of f (s) and f (t), hence their value is the same in all occurrences. := Rule := is locally sound for injective ∀i : C f (s) := θ, which we abbreviate as A. Injective A give a deterministic transition. We assume that the premise holds σ |= if ∃i : C s = A u then ∃i : C (s = A u ∧ φ(θ)) else φ(f ( A u)) ﬁ. We show that σ |= φ( ∀i : C f (s) := θ f (u)). First assume that, with a fresh variable z, φ(z) is a ﬁrst-order formula without modalities or quantiﬁers. Let τ be the (unique) state with (σ, τ ) ∈ ρ(∀i : C f (s) := θ) = ρ(A). By renaming, we can assume the quantiﬁed variable i not to occur anywhere else than in A. We write this occurrence constraint as i ∈ u and i ∈ φ(z). – Suppose σ |= ∃i : C s = A u, then σ |= ∃i : C (s = A u ∧ φ(θ)) by premise. e That is equivalent to: there is an e ∈ σ(C) with σi |= s = A u ∧ φ(θ). That e e means σi d |= φ(z) for d := σi [[θ]] by the substitution lemma. This is equivalent z d |= φ(z), because i ∈ φ(z), i.e., i does not occur in φ(z), so that its value to σz d is irrelevant. We want to show that σz |= φ(z) also holds for d = σ[[ A f (u)]], because this implies σ |= φ( A f (u)) by the substitution lemma. Now
e σ[[ A f (u)]] = τ [[f (u)]] = τ (f ) τ [[u]] = τ (f ) σ[[ A u]] = τ (f ) σi [[s]] ∗ ρ(A) e = σi [[θ]] = d

Thus σ |= φ( A f (u)). The equality marked ∗ holds, because the premise ime plies σi |= s = A u, which yields
e e σi [[s]] = σi [[ A u]] = σ[[ A u]] i∈u

– Suppose σ |= ¬∃i : C s = A u, then σ |= φ(f ( A u)) by premise. Consequently d σz |= φ(z) for d := σ[[f ( A u)]] by the substitution lemma. We show that d σz |= φ(z) also holds for d = σ[[ A f (u)]], because this implies σ |= φ( A f (u))

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

29

by the substitution lemma. This time we have σ[[ A f (u)]] = τ [[f (u)]] = τ (f ) τ [[u]] = σ(f ) τ [[u]] = σ(f ) σ[[ A u]] = σ[[f ( A u)]] = d The equality marked ∗ holds, because—by assumption σ |= ¬∃i : C s = A u— we know that for position τ [[u]] = σ[[ A u]] there is no e ∈ σ(C) such that
e e σi [[s]] = τ [[u]] = σ[[ A u]] = σi [[ A u]] i∈u ∗

Thus A has no eﬀect on the interpretation of f at position τ [[u]] and σ and τ agree at that position. In both cases, equivalence of premise and conclusion can be established by following the equations and equivalences backwards, which also gives a proof for the dual rule [:=]. For the case where φ(z) contains modalities or quantiﬁers, the proof is accordingly using the substitution lemma and the fact that the interpretation of the symbols occurring in A f (u) is not aﬀected by the modalities and quantiﬁers in φ(z) (since all substitutions need to be admissible for QdL rules to be applicable). [:] Local soundness of rule [:] for injective quantiﬁed assignments ∀i : C f (s) := θ is a simple consequence of the fact that a quantiﬁed assignment to f cannot aﬀect the evaluation of another operator Υ = f , but only its arguments (assuming admissible substitutions). The soundness of axiom (i.e., validity of the conclusion) is a simple consequence of the fact that we have assumed ﬁnite support for the createdness ﬂag (·) and that domains are inﬁnite. That is, there are only ﬁnitely many e ∈ σ(C) with e σi |= (i) = 1, yet domain σ(C) is inﬁnite. Consequently, in every state σ, there e always is a choice e for i that has not been created yet (σi |= (i) = 1). Rule is locally sound. Let ys (t) be simultaneous solutions for the respective diﬀerential equations with symbolic initial values f (s). Let ∀i : C f (s) := ys (t) denote the quantiﬁed assignment ∀i : C f (s) := ys (t) . Assume σ satisﬁes the premise: ˜ ˜ σ |= ∃t≥0 (χ ∧ ∀i : C f (s) := ys (t) φ , with ∀0≤t≤t ∀i : C f (s) := ys (t) χ abbrevi¯ r |= χ ∧ ∀i : C f (s) := y (t) φ. ¯ ated as χ. By premise, there is a real r ≥ 0 such that σt ¯ s Abbreviate ∀i : C f (s) = θ & χ by D. We have to show that σ |= D φ. Equivar lently, we show σt |= D φ, because t is a fresh variable that does not occur in D or φ. Let function ϕ : [0, r] → S be deﬁned such that (σ, ϕ(ζ)) ∈ ρ(f (s) := ys (t)) for all ζ ∈ [0, r]. By premise, ϕ(0) is identical to σ and φ holds at ϕ(r). Thus it only remains to be shown that ϕ respects the constraints for the ﬂow function ϕ in the deﬁnition of the semantics of ρ(D) in Section 4. In fact, ϕ obeys the continuity and diﬀerentiability properties required for well-deﬁnedness of time-derivatives by the corresponding properties of the solution ys (t). Moreover, for any e ∈ σ(C), ζe ϕ(ζ)e [[f (s)]] = σt i [[ys (t)]] has a derivative of value ϕ(ζ)e [[θ]], because ys is a solution i i of the quantiﬁed diﬀerential equation ∀i : C f (s) = θ with corresponding initial values σ(f (s)). Further, it can be shown that the evolution invariant region χ is r r respected along ϕ as follows: By premise, σt |= χ holds for the initial state σt , thus ¯ ϕ(ζ) |= χ for all ζ ∈ [0, r]. Combining these results, we can conclude that ϕ is a witness for σ |= D φ. The converse direction can be shown accordingly to prove equivalence and the dual rule [ ] for quantiﬁed diﬀerential equations with unique solutions (see end of Section 4). Without unique solutions, the rule is more complicated, but still works: all ∃ ∃ ∃ ∃ ∃

30

´ ANDRE PLATZER

[:∗]

gen

ind

con

parameters of all parametric solutions will need to be quantiﬁed over in addition to time t≥0. Rules [:∗], :∗ are locally sound by a simple consequence of the fact that arbitrary nondeterministic assignment of θ for any j of type C to n is the same as corresponding quantiﬁcation over C. The semantics of [∀j : C n := θ] then is equivalent to universal quantiﬁcation, that of ∀j : C n := θ is equivalent to existential quantiﬁcation. Rules []gen, gen,ind,con are sound (but not locally sound) by a variation of the usual proofs [HKT00, Pla10b]. For gen, let premise φ→ψ be valid. Let the antecedent be true in a state: σ |= α φ, i.e., let (σ, τ ) ∈ ρ(α) with τ |= φ. Hence, the premise implies τ |= φ → ψ, thus τ |= ψ, which implies σ |= α ψ. The proof for []gen is similar. Let premise φ→[α]φ be valid and let the antecedent of the conclusion be true in σ, that is σ |= φ. By premise, τ |= φ for all states τ with (σ, τ ) ∈ ρ(α). We thus conclude σ |= φ → [α∗ ]φ by induction along the series of states reached from σ by repeating α. Assume that the antecedent is valid and that the premise holds in σ. By premise, we have that τ |= v > 0 ∧ ϕ(v) → α ϕ(v − 1) for all states τ . By antecedent, there d is a d ∈ R such that σv |= ϕ(v). Now, the proof is a well-founded induction on d. If d ≤ 0, we have σ |= α∗ ∃v≤0 ϕ(v) directly for zero repetitions. Otherwise, if d > 0, we have, by premise, that
d σv |= v > 0 ∧ ϕ(v) → α ϕ(v − 1) d d As v > 0 ∧ ϕ(v) holds true at σv , we have for some τ with (σv , τ ) ∈ ρ(α) that d−1 τ |= ϕ(v − 1). Thus, τv |= ϕ(v) satisﬁes the induction hypothesis for a smaller d and a reachable τ , because (σ, τ ) ∈ ρ(α) as v does not occur in α. The induction is well-founded, because d decreases by 1 up to the base case d ≤ 0.

8. Completeness The veriﬁcation problem for distributed hybrid systems is extremely challenging. It has three independent sources of undecidability. Thus, no veriﬁcation technique can be eﬀective. Hence, QdL cannot be eﬀectively axiomatizable. The discrete fragment of QdL is not eﬀectively axiomatizable and the discrete fragment of QHPs is a computationally complete sublanguage. The continuous fragment of QdL is also not eﬀectively axiomatizable. The fragment with only structural and dimension-changing dynamics is not eﬀective either, because it can encode two-counter machines in link data structures. As a stronger result, we give a simple proof showing that each of those fragments of QdL can deﬁne ﬁrst-order integer arithmetic and are, thus, aﬀected by G¨del’s incompleteness theorem [G¨d31]. o o Theorem 8.1. ( Incompleteness of QdL). The discrete fragment of QdL, the continuous fragment of QdL, and the fragment of QdL with structural and dimension-changing dynamics are not eﬀectively axiomatizable, i.e., they have no sound and complete eﬀective calculus, because natural numbers are deﬁnable in each of those fragments.

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

31

Proof. We prove that natural numbers are deﬁnable among the real numbers of QdL interpretations in all three fragments. Then these fragments extend ﬁrst-order integer arithmetic such that the incompleteness theorem of G¨del [G¨d31] applies. G¨del’s incompleteness o o o theorem shows that no logic extending ﬁrst-order integer arithmetic can have a sound and complete eﬀective calculus. Natural numbers are deﬁnable in the discrete fragment using repetitive additions without continuous evolutions, quantiﬁed state change, or ﬁrst-order function symbols: nat(n) ↔ x := 0; (x := x + 1)∗ x = n. In the continuous fragment, an isomorphic copy of the natural numbers is deﬁnable using linear ordinary (non-quantiﬁed) diﬀerential equations without ﬁrst-order function symbols: nat(n) ↔ ∃s ∃c ∃τ (s = 0 ∧ c = 1 ∧ τ = 0 ∧ s = c, c = −s, τ = 1 (s = 0 ∧ τ = n)). These diﬀerential equations characterise sin and cos as unique solutions for s and c, respectively. Their zeros, as detected by τ , correspond to an isomorphic copy of natural numbers, scaled by π, i.e., nat(n) holds iﬀ n is of the form kπ for a k ∈ N; see Fig. 5. The initial values for s and c prevent the trivial solution identical to 0. s

π

2π

3π

4π

5π

τ

Figure 5: Characterisation of N as zeros of solutions of diﬀerential equations. Integer arithmetic for natural numbers is also deﬁnable in the fragment with only structural and dimensional dynamics. The proof is somewhat more involved, because we do not consider data arithmetic to be part of that fragment. Instead, we characterize natural numbers by chains of links along the values of a function p, where we encode zero by a constant symbol z: nat(n) ↔ (?n = z; n := p(n))∗ n = z. We characterize addition by a QHP plus(s, n, m) to express that the result of adding the natural numbers represented by n and m yields the number represented by s: plus(s, n, m) ≡ s := z; ?n = z; n := p(n); ν := new; p(ν) := s; s := ν ; ?m = z; m := p(m); ν := new; p(ν) := s; s := ν ; ?(n = z ∧ m = z) The idea behind this characterization is to create a new chain of links along the values of p by ﬁrst creating exactly as many links as we can follow along p when starting from n, and then continue creating exactly as many links as we can follow along p when starting from m, instead; see Fig. 6. The number of links of the result s then is the sum of the respective numbers of links of n and m. We characterize multiplication by a QHP times(s, n, m) to express that the result of multiplying the natural numbers represented by n and m yields the number represented by s: times(s, n, m) ≡ s := z; ?n = z; n := p(n); plus(t, m, s); s := t ; ?n = z
∗ ∗ ∗

32

´ ANDRE PLATZER

n z p p m s=n+m new copy of n append new copy of m

Figure 6: Characterization of N addition with p links in dimensional dynamics. The idea behind this characterization is to compute multiplication by a corresponding number of additions characterized by plus(t, m, s). That is, the product of n and m can be computed by adding m to an accumulator s, n times. The standard way to show adequacy of proof calculi for problems that are not eﬀective is to prove completeness relative to an oracle for handling a fragment of the logic. Unlike in Cook/Harel relative completeness for discrete programs [Coo78, HKT00], however, QdL cannot be complete relative to the fragment of the data logic (many-sorted ﬁrst-order logic with reals), because ﬁrst-order real arithmetic is decidable and many-sorted ﬁrst-order logic is semidecidable. If the QdL calculus would be complete relative to its data of manysorted ﬁrst-order logic with real arithmetic, then, since this is a semidecidable logic, the QdL calculus would be complete altogether, which would contradict Theorem 8.1. Thus, we need a diﬀerent basis for a relative completeness argument. Unlike in conventional discrete programs, the complexity of distributed hybrid systems truly originates from the actual dynamics, not the data. Theorem 8.1 shows that the discrete fragment, the continuous fragment, and also the structural/dimensional fragment of QdL each cause non-axiomatizability of QdL. The combination of these fragments and their repeated interaction in the QHP dynamics of QdL cannot be any easier. We prove that, nevertheless, our QdL calculus is a complete axiomatization relative to the fragment of QdL that has only quantiﬁed diﬀerential equations in modalities. We call this sublogic FOQD, the ﬁrst-order logic of quantiﬁed diﬀerential equations, i.e., (many-sorted) ﬁrst-order logic with real arithmetic augmented with formulas expressing properties of quantiﬁed diﬀerential equations, that is, QdL formulas of the form [∀i : C f (s) = θ & χ]F . The dual formula ∀i : C f (s) = θ & χ F is expressible as ¬[∀i : C f (s) = θ & χ]¬F . Note that the inclusion of χ in FOQD is not essential [Pla12]. Theorem 8.2. ( Axiomatization). The calculus in Fig. 2 is a sound and complete axiomatization of QdL relative to quantiﬁed diﬀerential equations, i.e., every valid QdL formula can be derived from valid FOQD tautologies. Proof Outline. The (constructive) proof, which, in full, is contained in the remainder of this section, generalizes our earlier proof for static, unquantiﬁed hybrid systems [Pla08a] to QdL and distributed hybrid systems. We prove that every valid QdL formula can be proven in the QdL calculus from elementary properties of quantiﬁed diﬀerential equations (valid oracle instances). The crucial step is to show that every valid property of a repetition α∗ of a QHP α for a distributed hybrid system can be proven by ind or con with a suﬃciently strong invariant or variant that is expressible in QdL. For this, we show that QHP transitions can be characterized in QdL. One decisive diﬀerence to our previous proof [Pla08a] is the need

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

33

to show that states can be characterized by a ﬁxed-size vector of real numbers, and can thus be quantiﬁed over. This is easy in static ﬁnite-dimensional systems, but a fairly tricky challenge in unbounded varying-dimensional systems with ﬁrst-order functions. This central result shows that properties of distributed hybrid systems can be proven to exactly the same extent to which properties of quantiﬁed diﬀerential equations can be proven. Proof-theoretically, the QdL calculus completely lifts veriﬁcation techniques for quantiﬁed continuous dynamics to distributed hybrid dynamics. Even though distributed hybrid systems have numerous independent sources of undecidability, we have shown that all true QdL formulas can be proven in our QdL calculus, if only we manage to tame the complexity of the continuous dynamics. Despite these new independent sources of undecidability, we have shown that QdL can still be axiomatized completely relative to diﬀerential equations, only now they are quantiﬁed diﬀerential equations. Another important consequence of this result is that decomposition is successful in taming the complexity of distributed hybrid systems. The QdL proof calculus is strictly compositional. All proof rules prove logical formulas or properties of QHPs by reducing them to structurally simpler QdL formulas. As soon as we understand that the distributed hybrid systems complexity comes from a combination of several simpler aspects, we can, hence, tame the system complexity by reducing it to analyzing the dynamical eﬀects of simpler parts. This decomposition principle is exactly how QdL proofs can scale to interesting systems in practice. The relative completeness theorem 8.2 gives the theoretical evidence why this principle works in general. In the remainder of this section, we present a fully constructive proof of Theorem 8.2. We have already shown that the QdL calculus is a sound axiomatization of QdL in Theorem 7.1. We need to prove that the QdL calculus is a complete axiomatization relative to quantiﬁed diﬀerential equations: every valid QdL formula can be derived in the QdL calculus from elementary properties of quantiﬁed diﬀerential equations. We need to prove that every valid QdL formula can be derived in the QdL calculus from a ﬁnite set of valid FOQD tautologies. A road map of the proof of Theorem 8.2 that we present here is above. The basic structure follows that of our relative completeness proof for unquantiﬁed differential dynamic logic for ﬁxed-dimensional static hybrid systems in previous work [Pla08a]. Here we generalize the proof to QdL. A fundamental diﬀerence to previous work is that states can be characterized trivially in ﬁxed-dimensional static hybrid systems, but it is not obvious why a ﬁnite formula would be suﬃcient in varying dimensions. In (dynamic) distributed hybrid systems, we have to prove that there is a ﬁnite formula that can characterize and identify all states (see Section 8.2). In ﬁxed-dimensional static hybrid systems, states can be characterized and identiﬁed trivially by a ﬁxed vector of real numbers for each system variable. In QdL, instead, states are full ﬁrst-order structures with interpretations of functions for all function symbols and the ability to characterize semantic states in logic is no longer obvious. States are no longer assignments of real numbers to a ﬁnite number of variables. In QdL, states are full ﬁrst-order interpretations of function symbols. Natural numbers are deﬁnable in FOQD by Theorem 8.1. Thus, we allow quantiﬁers over natural numbers like ∀x : N φ and ∃x : N φ and over integers ∀x : Z φ as abbreviations. 8.1. Characterizing Real G¨del Encodings. As the central device for constructing a o FOQD formula that captures the eﬀect of unboundedly many repetitive hybrid transitions and just uses ﬁnitely many real variables, we show that a real version of G¨del encoding is o

34

´ ANDRE PLATZER

deﬁnable in FOQD. That is, we show that there is a FOQD formula that reversibly packs ﬁnite sequences of real values into a single real number. Observe that a single diﬀerential equation system is not suﬃcient for deﬁning these pairing functions as their solutions are diﬀerentiable, yet, as a consequence of Morayne’s theorem [Mor87], there is no diﬀerentiable surjection R → R2 , nor to any part of R2 of positive measure. We show that real sequences can be encoded nevertheless by chaining the eﬀects of solutions of multiple diﬀerential equations and quantiﬁers. ¨ Lemma 8.3. ( R-Godel encoding). The formula at(Z, n, j, z), which holds iﬀ Z is a real number that represents a G¨del encoding of a sequence of n real numbers with real value z o at position j (for a position j with 1 ≤ j ≤ n), is deﬁnable in FOQD. For a formula φ(z) (n) we abbreviate ∃z (at(Z, n, j, z) ∧ φ(z)) by φ(Zj ). Proof. The proof is an immediate corollary to a result from previous work [Pla08a, Lemma 4].

8.2. First-order State Identiﬁcation. The crucial step in the proof of Theorem 8.2 is the construction of QdL (in)variants that are strong enough to characterize properties of repetition. In order to be able to characterize QHP state transitions in QdL (in)variants for the completeness proof, we ﬁrst need to ﬁnd formulas that characterize/identify states. For ﬁnite-dimensional systems of a ﬁxed dimension n, states can simply be characterized completely by the values of all n real state variables. A particular state could be characterized uniquely by the formula x = 2 ∧ y = 0.5 ∧ z = −0.382, for example. As a trivial corollary to Lemma 8.3, states can then even be characterized uniquely by one real number when using the R-G¨del encoding. For inﬁnite-dimensional systems, systems with changing o dimension, or systems with a dynamics that depends on evolving interpretations of function symbols f (s), the situation is more diﬃcult. After all, a state of QdL is a full ﬁrst-order structure with functions as interpretations of function symbols, and these interpretations can change from state to state. Furthermore, in order to navigate among states during the completeness proof, we need to be able to characterize the current ﬁrst-order state, but also to recall a previously identiﬁed ﬁrst-order state and express what holds true at this state. We show that the ﬁrst-order states reachable with QHP α from an initial state can, nevertheless, be characterized uniquely by real numbers, which can thus be quantiﬁed over. Furthermore, we show that this correspondence can be axiomatized in FOQD. One key observation is that the ﬁrst-order interpretations can change from state to state, but only according to the dynamics of the QHP. Intuitively, the diﬀerence of any reachable ﬁrstorder state to the initial state can be characterized by a ﬁnite list of diﬀerences to the initial state. Clearly this diﬀerence concerns only ﬁnitely many symbols occurring in α. It also concerns only ﬁnitely many positions of their interpreted functions, because actualist quantiﬁed assignments and actualist quantiﬁed diﬀerential equations only change the interpretation of ﬁnitely many function symbols at ﬁnitely many positions (actual quantiﬁed domains C! occurring in actualist quantiﬁers of QHPs are ﬁnite). Note that it is crucial for this argument that we have assumed the actual existence predicate (i) to have ﬁnite support. Lemma 8.4. ( State identification). Let Σb be a ﬁnite set of function symbols containing (·). The operators ↓ and @ , which identify and recall states reachable by QHPs, are deﬁnable in FOQD such that: ∃ ∃

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

35

(1) For every QHP α with BV(α) ⊆ Σb , every variable I ∈ Σb of sort R, and every state σ, the formula ↓ I is true in at most one of the states reachable by α from σ. That is, there is at most one state ι such that (σ, ι) ∈ ρ(α) and ι |= ↓ I. (2) For every QHP α with BV(α) ⊆ Σb , every variable I ∈ Σb of sort R, every formula φ, and every state σ, the formula @ I φ is true in any state reachable by α from σ if and only if φ is true in the (unique) state that is reachable by α from σ in which ↓ I holds (provided such a state is reachable at all, otherwise the truth-value of @ I φ is arbitrary). That is, suppose there is a state ι such that (σ, ι) ∈ ρ(α) and ι |= ↓ I (thus, by case 1, ι is unique with that property). Then for any state τ with (σ, τ ) ∈ ρ(α), it is the case that τ |= @ I φ if and only if ι |= φ. If, on the contrary, there is no state ι with (σ, ι) ∈ ρ(α) and ι |= ↓ I, then this lemma makes no statement concerning the truth of formula @ I φ at any state τ . Proof. The formulas ↓ I and @ I φ are like the here and at operators of hybrid-nominal logic. We show that they can be characterized by FOQD formulas. For deﬁning ↓ I and @ I φ, we use an auxiliary function isf (I, o) to improve readability. The formula θ = isf (I, o) is true if the value of θ coincides with the value of f at position o according to the state characterized by I (i.e., where ↓ I is true). We characterize θ = isf (I, o) by the following FOQD formula:
(m) (m) if ∃s : N (s < m ∧ Xs = o) then ∃s : N (s < m ∧ Xs = o ∧ θ = Ys(m) ) else θ = f (o) ﬁ (d) (3) (d) (3) 2 ,Y (d) (3) 3

where I is split into the following abbreviations m := Ii 1 , X := Ii further d is the number of symbols in Σb and i is the index of f in Σb

:= Ii

The function symbol isf (I, o) gives the value (θ) of function f at position o at the state characterized by the real number denoted by I. It can be deﬁned easily using the real pairing function from Lemma 8.3. The basic idea is to understand I via the real pairing function (m) (m) as a list of length m of position/value pairs (Xs /Ys ), which characterize changes to the value f (o) for each of the ﬁnitely many function symbols f ∈ Σb . Using an arbitrary but ﬁxed ordering, these function symbols f are identiﬁed with their index d in Σb . The most important insight for the proof is that, for every state reachable by α from σ, the list of changes of f compared to f (o) at σ is always ﬁnite after ﬁnitely many transitions of quantiﬁed state change with ﬁnite support (see end of Section 5). Consequently, the list of changes can always be encoded by one (ﬁnite) real number according to Lemma 8.3. Using the auxiliary deﬁnition θ = isf (I, o), we characterize cases 1 and 2, that is ↓ I and @ I φ by the following FOQD formulas: ↓I ≡
f ∈Σb

∀o : Sf f (o) = isf (I, o)

where Sf is the sort of the arguments of f

@ I φ ≡ ∀i : C ∀u : R f (i) = u (φ ∧ ↓ I) The deﬁnitions do not need recursion, so that we can consider occurrences of the deﬁned notations as syntactic abbreviations for quantiﬁed variables satisfying the respective deﬁnitions (like for Lemma 8.3). Case 1: The characterization for ↓ I is deﬁned as a conjunction over all relevant function symbols f ∈ Σb asserting that the value f (o) of f at each position o of the sort Sf of f is identical to the corresponding value isf (I, o) characterized by I. Case 2: The characterization for @ I φ uses a quantiﬁed diﬀerential equation with a variable u that only occurs on the right hand side and thus changes f at all positions i

36

´ ANDRE PLATZER

with an arbitrary slope u. The @ I φ characterization then checks if the appropriate state characterized by I has been reached using ↓ I and further expresses that φ holds at this state. By case 1, we know that ↓ I holds in at most one of the states reachable by α from σ. In the quantiﬁed diﬀerential equation system for @ I φ, the second quantiﬁed variable u amounts to nondeterministically specifying a slope u for each f (i). Unlike i, quantiﬁed variable u only occurs on the right hand side of the quantiﬁed diﬀerential equation. Consequently, the semantics (case 2 of the transition relation ρ(α) deﬁned in Section 4) deﬁnes the states corresponding to all choices for u to be reachable. These respective choices for u include the choice that leads to the state characterized by ↓ I, e.g., by choosing slope u := isf (I, i) − f (i) for each i and evolving for 1 time unit. To simplify notation, we deﬁne @ I φ only for Σb = {f }. The construction is repeated accordingly (by nesting modalities) for each f ∈ Σb , which are ﬁnitely many. The createdness ﬂag (·) needs to be part of Σb so that object creation is taken care of on the ﬂy. 8.3. Expressibility and Rendition of Quantiﬁed Hybrid Program Semantics. In order to show that QdL is suﬃciently expressive to state the invariants and variants that are needed for proving valid statements about QHP loops with ind and con, we prove an expressibility result. We give a constructive proof that the state transition relation of QHPs is deﬁnable in FOQD, i.e., there is a FOQD-formula Rα (I) characterizing the state transitions of quantiﬁed hybrid program α from the current state to the state characterized by I (a real variable that characterizes a state by way of Lemma 8.4). For this, we need to characterize the dynamics of QHPs, which are dynamic distributed hybrid processes with repetitively evolving discrete, continuous, structural, and dimension-changing dynamics, equivalently by quantiﬁed diﬀerential equations in FOQD. Lemma 8.5. ( Program rendition). For every QHP α with symbols among a ﬁnite set Σb ⊇ { (·)} there is a FOQD-formula Rα (I) with one additional free variable I of sort R such that Rα (I) ↔ α ↓ I R∀i : C ∃
f (s):=θ (I)

≡ ∀o : Sf
if ∃i : C o = s then ∃i : C (o = s ∧ θ = isf (I, o)) else f (o) = isf (I, o) ﬁ

∧
g∈Σb \{f }

∀o : Sg g(o) = isg (I, o)

R∀i : C R∀i : C

f (s) =θ (I)

≡ ∀i : C f (s) = θ ↓ I ≡ ∀i : C f (s) = θ & χ ↓ I

f (s) =θ & χ (I)

R?χ (I) ≡ χ ∧ ↓ I Rβ∪γ (I) ≡ Rβ (I) ∨ Rγ (I) Rβ; γ (I) ≡ ∃B (Rβ (B) ∧ @ B Rγ (I)) Rβ ∗ (I) ≡ ∃B ∃n : N ↓ B1 ∧ B(n) = I ∧ ∀i : N (1 ≤ i < n → @ Bi n
(n) (n)

Figure 7: Explicit rendition of QHP transition semantics in FOQD

∃

Rβ (Bi+1 ))

(n)

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

37

Proof. The program rendition is deﬁned inductively in Fig. 7. The characterization of quantiﬁed assignments is a variation of the characterization of ↓ I from the proof of Lemma 8.4. The only diﬀerence is that the value θ is used instead of f (o) for positions o that are aﬀected by the quantiﬁed state change, i.e., o is of the form s for some i (where the quantiﬁed assignment matches as expressed by ∃i : C o = s). Quantiﬁed diﬀerential equations give FOQD-formulas already, because ↓ I is a FOQD-formula, hence no further reduction is necessary. With a ﬁnite formula, the characterization of repetition Rβ ∗ (v) in FOQD needs to capture arbitrarily long sequences of intermediate ﬁrst-order states and the correct transition between successive states of such a sequence. To achieve this with ﬁrst-order quantiﬁers, we use the real G¨del encoding from Lemma 8.3 in Fig. 7 along with the ﬁrst-order state ideno tiﬁcation from Lemma 8.4 to map unbounded sequences of real ﬁrst-order states reversibly to a single real variable B, which can be quantiﬁed over in ﬁrst-order logic and identify a ﬁrst-order state with it by Lemma 8.4. Using the QHP rendition from Lemma 8.5 to characterize modalities, we prove that every QdL formula can be expressed equivalently in FOQD by structural induction. Lemma 8.6. ( Expressibility). QdL is expressible in FOQD: for all QdL formulas φ ∈ Fml there is a FOQD-formula φ ∈ FmlFOQD that is equivalent, i.e., φ ↔ φ . The converse holds trivially. Proof. The proof follows an induction on the structure of formula φ for which it is imperative to ﬁnd an equivalent φ in FOQD. Observe that the construction of φ from φ is eﬀective. 0. If φ is a ﬁrst-order formula, then φ := φ already is a FOQD-formula such that nothing has to be shown. (1) If φ is of the form ϕ ∨ ψ, then by induction hypothesis there are FOQD-formulas ϕ , ψ such that ϕ ↔ ϕ and ψ ↔ ψ , from which we can conclude by congruence that (ϕ ∨ ψ) ↔ (ϕ ∨ ψ ) giving φ ↔ φ by choosing ϕ ∨ ψ for φ . Likewise reasoning concludes the other propositional connectives or quantiﬁers. (2) The case where φ is of the form α ψ is a consequence of the characterization of the semantics of QHPs in FOQD. The expressibility conjecture holds by induction hypothesis using the equivalence of explicit QHP renditions from Lemma 8.5: α ψ ↔ ∃I (Rα (I) ∧ @ I ψ ) . (3) The case where φ is [α]ψ is again a consequence of Lemma 8.5: [α]ψ ↔ ∀I (Rα (I) → @ I ψ ) .

8.4. Relative Completeness of First-order Assertions. As special cases of Theorem 8.2, we ﬁrst prove relative completeness for ﬁrst-order assertions about QHPs. These ﬁrst-order cases constitute the basis for the general completeness proof for arbitrary QdL formulas. In the sequel, we use the notation D φ to indicate that a QdL formula φ is derivable from a set of FOQD-tautologies, which is equivalent to saying that φ is derivable in the QdL calculus augmented with a single oracle axiom D, that gives all valid FOQD-instances. The QdL calculus contains a complete calculus for propositional logic and for many-sorted

38

´ ANDRE PLATZER

ﬁrst-order logic. We implicitly use simple propositional reasoning (using the cut-rule) to glue together subproofs propositionally. Proposition 8.7. ( Relative completeness of first-order safety). For every QHP α and all FOQD formulas F, G F → [α]G implies
D

F → [α]G .

Proof. We generalize the relative completeness proof by Cook [Coo78] to QdL and follow an induction on the structure of program α. In the following, IH is short for the induction hypothesis. (1) The cases where α is of the form f (s) := θ, ?χ, β ∪ γ, or β; γ are consequences of the soundness of the rules [;], [∪], [?], and [:=], which are equivalence rules. Consequently, whenever their conclusion is valid, their premise is valid and of smaller complexity (the programs get simpler), hence the premise is derivable by IH. Thus, we can derive F → [α]G by applying the respective rule. For [:=] and [:], respectively, the premise is simpler because the quantiﬁed assignment is only applied to structurally simpler expressions (u) in the premise than in the conclusion (f (u)) while the program stays the same. For nondeterministic assignments, the reasoning is similar using equivalence rule [:∗] instead of [:=]. Again, the premise is valid, and already a FOQD formula, hence derivable as an D axiom directly. A formal rewrite proof along these lines is a simple modiﬁcation of prior work [BP06]. We explicitly show the proof for β; γ as it contains an extra twist. (2) F → [β; γ]G, which implies F → [β][γ]G. By Lemma 8.6, there is a FOQDformula G such that G ↔ [γ]G. From the validity of F → [β]G , we can conclude by IH that D F →[β]G is derivable. Similarly, because of G → [γ]G, we conclude D G → [γ]G by IH. With an application of []gen, the latter derivation can be extended to a derivation of D [β]G →[β][γ]G. Combining the above derivations propositionally by a cut with [β]G , we can derive D F →[β][γ]G, from which [;] yields D F →[β; γ]G as desired. (3) F → [∀i : C f (s) = θ & χ]G is a FOQD-formula and hence derivable as a D axiom directly. (4) F → [β ∗ ]G can be derived by induction. For this, we deﬁne the invariant as a FOQD encoding of the statement that all potential poststates of β ∗ satisfy G according to Lemma 8.6: φ ≡ ([β ∗ ]G) ≡ ∀I (Rβ ∗ (I) → @ I G) . Since F → φ and φ → G are valid FOQD-formulas according to the semantics, they are derivable by D. By []gen, D [β ∗ ]φ→[β ∗ ]G is derivable from the latter. Likewise, φ → [β]φ is valid according to the semantics of repetition, thus derivable by IH, since β is less complex. Now ind yields D φ→[β ∗ ]φ. Combining the above derivations propositionally by a cut with [β ∗ ]φ and φ yields D F →[β ∗ ]G. Proposition 8.8. ( Relative completeness of first-order liveness). For each QHP α and all FOQD-formulas F, G F → α G implies
D

F → αG .

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

39

Proof. We generalize the integer arithmetic completeness proof by Harel [Har79] to the hybrid case. Most cases of the proof are simple adaptations of the corresponding cases in Proposition 8.7. What remains to be shown is the case of repetitions. Assume that F → β ∗ G. To derive this formula by con, we use a FOQD-formula ϕ(n) as a variant expressing that, after n iterations, β can lead to a state satisfying G. This formula is obtained from Lemma 8.5-8.6 as ( β ∗ G) ≡ ∃I (Rβ ∗ (I) ∧ @ I G), except that the quantiﬁer on the repetition count n is removed such that n becomes a free variable (plus index shifting to count repetitions): ϕ(n − 1) ≡ ∃B ↓ B1 ∧ B(n) = I ∧ ∀i : N (1 ≤ i < n → @ Bi n
(n) (n)

Rβ (Bi+1 )) ∧ @ I G .

(n)

By Lemma 8.3, ϕ(n) can only hold true if n is a natural number. According to the loop semantics, n > 0 ∧ ϕ(n) → β ϕ(n − 1) is valid by construction: If n > 0 is a natural number then so is n − 1, and if β reaches G after n repetitions, then, after executing β once, n − 1 repetitions of β reach G. By IH, this formula is derivable, since β contains less loops. We have derived D n > 0 ∧ ϕ(n) → β ϕ(n − 1). Thus ∗ D ∃v ϕ(v)→ β ∃v≤0 ϕ(v) by con. It only remains to show that the antecedent is derivable from F and that β ∗ G is derivable from the succedent. From our assumption, we conclude that the following are valid FOQD-formulas, hence D-axioms: • F → ∃v ϕ(v), because F → β ∗ G, and • (∃v≤0 ϕ(v)) → G, because v≤0 and the fact, that, by Lemma 8.3, ϕ(v) only holds true for natural numbers, imply ϕ(0). Further, ϕ(0) entails G, because zero repetitions of β have no eﬀect. We extend the latter derivation to D β ∗ ∃v≤0 ϕ(v)→ β ∗ G by gen. Now, the above derivations can be combined propositionally by a cut with β ∗ ∃v≤0 ϕ(v) and with ∃v ϕ(v) to yield D F → β ∗ G. 8.5. Relative Completeness of the QdL Calculus. Having succeeded with the proofs of the above statements about parts of the completeness proof, we can ﬁnish the proof of Theorem 8.2. Proof of Theorem 8.2. The proof follows a basic structure similar to that of Harel’s proof for the discrete case [Har79, Theorem 3.1]. We have to show that every valid QdL formula φ can be proven from FOQD axioms within the QdL calculus: from φ we have to prove D φ. The proof proceeds as follows: By propositional recombination, we inductively identify fragments of φ that correspond to φ1 → [α]φ2 or φ1 → α φ2 logically. Next, we express subformulas φi equivalently in FOQD by Lemma 8.6, and use Proposition 8.7 and 8.8 to resolve these ﬁrst-order safety or liveness assertions. Finally, we prove that the original QdL formula can be re-derived from the subproofs. We can assume φ to be given in conjunctive normal form by appropriate propositional reasoning. In particular, we assume that negations are pushed inside over modalities using the dualities ¬[α]φ ≡ α ¬φ and ¬ α φ ≡ [α]¬φ. The remainder of the proof follows an induction on a measure |φ| deﬁned as the number of modalities in φ. For a uniform proof, we assume real quantiﬁers to be abbreviations for modal formulas by ∃x : R φ ≡ x = 1 φ ∨ x = −1 φ and ∀x : R φ ≡ [x = 1]φ ∧ [x = −1]φ. Following either x = 1 or x = −1, we can reach any real number as a value for x. Similarly, we assume quantiﬁers for sort C = R to be abbreviations for modal formulas by ∃x : C φ ≡ ∀j : C x := j φ

40

´ ANDRE PLATZER

and ∀x : C φ ≡ [∀j : C x := j]φ. We can obtain any object of sort C by an appropriate choice of j. Now the proof is by induction on the measure |φ| of φ. 0. |φ| = 0 then φ is a ﬁrst-order formula, hence derivable by D. (1) φ is of the form ¬φ1 , then φ1 is ﬁrst-order, as we assumed negations to be pushed inside. Hence, case 0 applies: |φ| = 0. (2) φ is of the form φ1 ∧ φ2 , then individually deduce the simpler proofs for D φ1 and D φ2 by IH, which can be combined by ∧r. (3) φ is a disjunction and—without loss of generality—has one of the following forms (otherwise use associativity and commutativity to select a diﬀerent order for the disjunction): φ1 ∨ [α]φ2 φ1 ∨ α φ2 As a uniﬁed notation for those cases we use φ1 ∨ [α] φ2 . Then, |φ2 | < |φ|, since φ2 has less modalities. Likewise, |φ1 | < |φ| because [α] φ2 contributes one modality to |φ| that is not part of φ1 . According to Lemma 8.6 there are FOQD-formulas φ1 , φ2 that satisfy φi ↔ φi for i = 1, 2. By congruence, the validity φ yields that φ1 ∨ [α] φ2 , which directly implies ¬φ1 → [α] φ2 . Then by Proposition 8.7 or 8.8, respectively, we can derive
D

¬φ1 → [α] φ2 .

(8.1)

Further φ1 ↔ φ1 implies ¬φ1 → ¬φ1 , which is derivable by IH, because |φ1 | < |φ|. We combine the resulting derivation D ¬φ1 →¬φ1 , with (8.1) by a cut with ¬φ1 to obtain (8.2) D ¬φ1 → [α] φ2 . Likewise φ2 ↔ φ2 implies φ2 → φ2 , which is derivable by IH, as |φ2 | < |φ|. We can extend the derivation of D φ2 → φ2 D [α] φ2 → [α] φ2 by []gen– gen. Finally we combine the latter propositionally with (8.2) by a cut with [α] φ2 to derive D ¬φ1 → [α] φ2 , from which D φ1 ∨ [α] φ2 can be obtained, again using cut, to complete the proof.

9. Distributed Car Control Verification With the QdL calculus and the compatibility condition M(i, j) from eqn. (3.2), we can easily prove collision freedom, i.e., formula (5.2), in the distributed car control system (5.4): (∀i, j : C! M(i, j)) → [(n := new C; ?∀i : C! M(i, n); ∀i : C! (x(i) = a(i))) ] ∀i=j : C! x(i)=x(j) (9.1) The biggest challenge in the proof of this QdL formula is that it involves continuous dynamics, discrete dynamics, and dimensional dynamics, and that all parts of the system need to interact safely for the system to stay collision-free. In particular, formula (9.1) states a safety property of unboundedly many cars driving on a road, where an unbounded number of new cars may additionally appear dynamically during the evolution of the system. See Fig. 8 for a formal QdL proof of this QdL formula, which proves collision freedom despite dynamic appearance of new cars.
∗

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

41

∗ ∗ i∀ , M(i, n), t≥0→St M(i, n) M(i, j), , t≥0→St M(i, j) ∀l ∀l . . . , ∀i : C! M(i, n), t≥0→St M(i, n) ∀i, j : C! M(i, j), . . . , t≥0→St M(i, j) ∧r ∀i, j : C! M(i, j), ∀i : C! M(i, n), t≥0→St M(i, n) ∧ St M(i, j) [:=] ∀i, j : C! M(i, j), ∀i : C! M(i, n), t≥0→[∀i : C!∪{n} St (i)](M(i, n) ∧ M(i, j)) ∀r ∀i, j : C! M(i, j), ∀i : C! M(i, n), t≥0→[∀i : C!∪{n} St (i)]∀i, j : C! (M(i, n) ∧ M(i, j)) ν∀ ∀i, j : C! M(i, j), ∀i : C! M(i, n), t≥0→[∀i : C!∪{n} St (i)][ (n)]∀i, j : C! M(i, j) νA ∀i, j : C! M(i, j), ∀i : C! M(i, n), t≥0→[ (n)][∀i : C! St (i)]∀i, j : C! M(i, j) ∀r,→r ∀i, j : C! M(i, j), ∀i : C! M(i, n)→[ (n)]∀t≥0 [∀i : C! St (i)]∀i, j : C! M(i, j) [ ] ∀i, j : C! M(i, j), , ∀i : C! M(i, n)→[ (n)][∀i : C! (x(i) = a(i))]∀i, j : C! M(i, j) ν∀,∧l ∀i, j : C! M(i, j), [ (n)]∀i : C! M(i, n)→[ (n)][∀i : C! (x(i) = a(i))]∀i, j : C! M(i, j) →r ∀i, j : C! M(i, j)→[ (n)](∀i : C! M(i, n) → [∀i : C! (x(i) = a(i))]∀i, j : C! M(i, j)) [?] (n) = 0, ∀i, j : C! M(i, j)→[ (n)][?∀i : C! M(i, n); ∀i : C! (x(i) = a(i))]∀i, j : C! M(i, j) new ∀i, j : C! M(i, j)→[n := new C][?∀i : C! M(i, n); ∀i : C! (x(i) = a(i))]∀i, j : C! M(i, j) [;] ∀i, j : C! M(i, j)→[DCCS]∀i, j : C! M(i, j) ind ∀i, j : C! M(i, j)→[(DCCS)∗ ]∀i=j : C! x(i)=x(j)
i∀

Figure 8: QdL proof for collision freedom in distributed car control with dynamic appearance. The proof in Fig. 8 uses induction (rule ind) with invariant ∀i, j : C! M(i, j). Figure 8 does not show the branch proving that the invariant ∀i, j : C! M(i, j) implies the postcondition ∀i=j : C! x(i)=x(j), which is easy to prove. The proof step marked by new uses the deﬁnition of new C from eqn. (5.1). To save space, we abbreviate [ (n) := 1] by [ (n)] in Fig. 8. The proof uses the derived rules ν∀ and νA from Section 6 to propagate the eﬀect of object creation on actualist quantiﬁers and actualist quantiﬁed assignments respectively. In rule νA, the shorthand notation ∀i : C!∪{n} St (i) in the resulting formula indicates that the new object n is also updated according to the solution St (n), not just the previously existing objects (∀i : C! St (i)). Here, we abbreviate by St (i) the solution x(i) := x(i) + v(i)t + a(i) t2 , v(i) := v(i) + a(i)t of the 2 quantiﬁed diﬀerential equation ∀i : C x(i) = a(i), which rule [ ] introduces. For the topmost application of rule [:=], we denote by St M(i, j) the result of substituting ∀i : C! St (i) into M(i, j) according to rule [:=]. In Fig. 8, we leave out some irrelevant formulas, indicated by ellipsis (. . . ) or gray print. The proof closes (indicated by ∗) by QE with rule i∀. Hence, QdL formula (9.1) is valid by Theorem 7.1. In a similar way, the QdL proof rules can prove collision freedom in an advanced distributed car control system that has both dynamic appearance of cars on the road as in (5.4) and more ﬂexibility in acceleration and braking choices of the individual cars as in (5.3). For this, we choose a weaker constraint for M(i, j) that allows cars that move with quite diﬀerent accelerations, if only the respective safety distances are compatible with the diﬀerent velocities: i = j → (x(i) < x(j) ∧ v(i)2 < v(j)2 + 2b(x(j) − x(i)) ∧ v(i) ≥ 0 ∧ v(j) ≥ 0) ∨ (x(i) > x(j) ∧ v(j)2 < v(i)2 + 2b(x(i) − x(j)) ∧ v(i) ≥ 0 ∧ v(j) ≥ 0) ∃ ∃

∃

∃ ∃ ∃ ∃ ∃ ∃

∃

∃

42

´ ANDRE PLATZER

With this choice for M(i, j), the QdL proof calculus can be used to prove the following QdL formula with a proof very similar to that in Fig. 8: ∀i, j : C! M(i, j) → n := new C; ?∀i : C! M(i, n); ∀i : C! a(i) := if ∀j : C! far(i, j) then a else −b ﬁ; τ := 0; ∀i : C! (x(i) = v(i), v(i) = a(i), τ = 1 & v(i) ≥ 0 ∧ τ ≤ ε))∗ ∀i=j : C! x(i)=x(j) (9.2) The QHP in QdL formula (9.2) allows all cars to change their respective acceleration freely when all other cars are suﬃciently far away like in (5.3). For this, we choose a condition characterizing that the distributed car control system stays controllable for at least ε time units (which is the maximum reaction time of the controller): v(i)2 − v(j)2 a a 2 + +1 ε + εv(i) 2b b 2 The continuous dynamics in (9.2) is bounded by the evolution domain constraint τ ≤ ε to evolve for at most ε time units, at which point, at the latest, the discrete controllers will have a chance to react to situation changes again (i.e., the control loop repeats). The QdL proof of (9.2) has the same structure as that in Fig. 8 except that the arithmetic is more involved to handle the resulting nonlinear and nonmonotonic arithmetic constraints, see [Pla10d]. For a QdL proof extending the above ideas to a proof of collision-freedom for a more realistic distributed car control system having arbitrarily many cars switching between arbitrarily many lanes with dynamic appearance and disappearance of arbitrarily many cars, we refer to follow-up work [LPN11]. Unlike our simpliﬁed system model, this followup work does not assume that all cars use the same braking power. far(i, j) ≡ x(j) > x(i) → x(j) > x(i) + 10. Conclusions We have introduced a formal system model and semantics for dynamic distributed hybrid systems together with a compositional veriﬁcation logic and proof calculus. We believe this is the ﬁrst formal veriﬁcation approach for distributed hybrid dynamics, where structure and dimension of the system can evolve jointly with the discrete and continuous dynamics. Our approach handles distributed hybrid systems with interacting discrete dynamics, continuous dynamics, structural dynamics, and dimensional dynamics. We have proven our calculus to be a sound and complete axiomatization relative to quantiﬁed diﬀerential equations. Our calculus proves collision avoidance in distributed car control with dynamic appearance of new cars on the road, which is out of scope for other approaches. Future work includes full modular concurrency in distributed hybrid systems, which is already challenging in discrete programs. Acknowledgement I thank Frank Pfenning for his helpful comments and the reviewers for their feedback.

A COMPLETE AXIOMATIZATION OF QdL FOR DISTRIBUTED HYBRID SYSTEMS

43

References
[ACHH92] Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho. Hybrid automata: An algorithmic approach to the speciﬁcation and veriﬁcation of hybrid systems. In Grossman et al. [GNRR93], pages 209–229. Krzysztof R. Apt, Frank S. de Boer, and Ernst-R¨diger Olderog. Veriﬁcation of Sequential and u Concurrent Programs. Springer, 3rd edition, 2010. Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag, editors. Hybrid Systems III: Veriﬁcation and Control, Proceedings, volume 1066 of LNCS. Springer, 1996. Paul C. Attie and Nancy A. Lynch. Dynamic input/output automata: A formal model for dynamic systems. In Kim Guldstrand Larsen and Mogens Nielsen, editors, CONCUR, volume 2154 of LNCS, pages 137–151. Springer, 2001. Michael S. Branicky, Vivek S. Borkar, and Sanjoy K. Mitter. A uniﬁed framework for hybrid control: Model and optimal control theory. IEEE T. Automat. Contr., 43(1):31–45, 1998. Vladimir I. Bogachev. Deterministic and stochastic diﬀerential equations in inﬁnite-dimensional spaces. Acta Appl. Math., 40(1):25–93, Jul 1995. Bernhard Beckert and Andr´ Platzer. Dynamic logic with non-rigid functions: A basis for e object-oriented program veriﬁcation. In Ulrich Furbach and Natarajan Shankar, editors, IJCAR, volume 4130 of LNCS, pages 266–280. Springer, 2006. Michael S. Branicky. General hybrid dynamical systems: Modeling, analysis, and control. In Alur et al. [AHS96], pages 186–200. George E. Collins and Hoon Hong. Partial cylindrical algebraic decomposition for quantiﬁer elimination. J. Symb. Comput., 12(3):299–328, 1991. Zhou Chaochen, Wang Ji, and Anders P. Ravn. A formal description of hybrid systems. In Alur et al. [AHS96], pages 511–530. Stephen A. Cook. Soundness and completeness of an axiom system for program veriﬁcation. SIAM J. Comput., 7(1):70–90, 1978. Akash Deshpande, Aleks G¨ll¨, and Pravin Varaiya. SHIFT: A formalism and a programming o u language for dynamic networks of hybrid automata. In Panos J. Antsaklis, Wolf Kohn, Anil Nerode, and Shankar Sastry, editors, Hybrid Systems, volume 1273 of LNCS, pages 113–133. Springer, 1996. Gilles Dowek, C´sar Mu˜oz, and V´ e n ıctor A. Carre˜o. Provably safe coordinated strategy for n distributed conﬂict resolution. In Proceedings of the AIAA Guidance Navigation, and Control Conference and Exhibit 2005, AIAA-2005-6047, 2005. Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer, New York, 2nd edition, 1996. Melvin Fitting and Richard L. Mendelsohn. First-Order Modal Logic. Kluwer, Norwell, MA, USA, 1999. Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel, editors. Hybrid Systems, volume 736 of LNCS. Springer, 1993. ¨ Kurt G¨del. Uber formal unentscheidbare S¨tze der Principia Mathematica und verwandter o a Systeme I. Mon. hefte Math. Phys., 38:173–198, 1931. David Harel. First-Order Dynamic Logic. Springer, New York, 1979. Thomas A. Henzinger. The theory of hybrid automata. In LICS, pages 278–292, Los Alamitos, 1996. IEEE Computer Society. Ann Hsu, Farokh Eskaﬁ, Sonia Sachs, and Pravin Varaiya. Design of platoon maneuver protocols for IVHS. PATH Research Report UCB-ITS-PRR-91-6, Institute of Transportation Studies, University of California, Berkeley, 1991. David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic logic. MIT Press, Cambridge, 2000. Charles Antony Richard Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576–580, 1969. Reiner H¨hnle and Peter H. Schmitt. The liberalized δ-rule in free variable semantic tableaux. a J. Autom. Reasoning, 13(2):211–221, 1994. Jo˜o P. Hespanha and Ashish Tiwari, editors. Hybrid Systems: Computation and Control, 9th a International Workshop, HSCC 2006, Santa Barbara, CA, USA, March 29-31, 2006, Proceedings, volume 3927 of LNCS. Springer, 2006.

[AdBO10] [AHS96] [AL01]

[BBM98] [Bog95] [BP06]

[Bra95] [CH91] [CJR95] [Coo78] [DGV96]

[DMC05]

[Fit96] [FM99] [GNRR93] [G¨d31] o [Har79] [Hen96] [HESV91]

[HKT00] [Hoa69] [HS94] [HT06]

44

´ ANDRE PLATZER

Dexter Kozen. Kleene algebra with tests. ACM Trans. Program. Lang. Syst., 19(3):427–443, 1997. [KSPL06] Fabian Kratz, Oleg Sokolsky, George J. Pappas, and Insup Lee. R-Charon, a modeling language for reconﬁgurable hybrid systems. In Hespanha and Tiwari [HT06], pages 392–406. [LPN11] Sarah M. Loos, Andr´ Platzer, and Ligia Nistor. Adaptive cruise control: Hybrid, distributed, e and now formally veriﬁed. In Michael Butler and Wolfram Schulte, editors, FM, volume 6664 of LNCS, pages 42–56. Springer, 2011. [Lyn96] Nancy Lynch. Distributed Algorithms. Morgan Kaufmann, 1996. [Mor87] Michal Morayne. On diﬀerentiability of Peano type functions. Colloquium Mathematicum, LIII:129–132, 1987. [MS06] Jos´ Meseguer and Raman Sharykin. Speciﬁcation and analysis of distributed object-based e stochastic hybrid systems. In Hespanha and Tiwari [HT06], pages 460–475. [Pla08a] Andr´ Platzer. Diﬀerential dynamic logic for hybrid systems. J. Autom. Reas., 41(2):143–189, e 2008. [Pla08b] Andr´ Platzer. Diﬀerential Dynamic Logics: Automated Theorem Proving for Hybrid Systems. e PhD thesis, Department of Computing Science, University of Oldenburg, Dec 2008. Appeared with Springer. [Pla10a] Andr´ Platzer. Diﬀerential-algebraic dynamic logic for diﬀerential-algebraic programs. J. Log. e Comput., 20(1):309–352, 2010. [Pla10b] Andr´ Platzer. Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. e Springer, Heidelberg, 2010. [Pla10c] Andr´ Platzer. Quantiﬁed diﬀerential dynamic logic for distributed hybrid systems. In Anuj e Dawar and Helmut Veith, editors, CSL, volume 6247 of LNCS, pages 469–483. Springer, 2010. [Pla10d] Andr´ Platzer. Quantiﬁed diﬀerential dynamic logic for distributed hybrid systems. Technical e Report CMU-CS-10-126, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 2010. [Pla11] Andr´ Platzer. Quantiﬁed diﬀerential invariants. In Emilio Frazzoli and Radu Grosu, editors, e HSCC, pages 63–72. ACM, 2011. [Pla12] Andr´ Platzer. The complete proof theory of hybrid systems. In LICS. IEEE Computer Society, e 2012. [Pra76] Vaughan R. Pratt. Semantical considerations on Floyd-Hoare logic. In FOCS, pages 109–121. IEEE, 1976. [PSFB07] L. Pallottino, V. G. Scordio, E. Frazzoli, and A. Bicchi. Decentralized cooperative policy for conﬂict resolution in multi-vehicle systems. IEEE Trans. on Robotics, 23(6):1170–1183, 2007. [Rou04] William C. Rounds. A spatial logic for the hybrid π-calculus. In Rajeev Alur and George J. Pappas, editors, HSCC, volume 2993 of LNCS, pages 508–522. Springer, 2004. [R¨m06] u Philipp R¨mmer. Sequential, parallel, and quantiﬁed updates of ﬁrst-order structures. In Miki u Hermann and Andrei Voronkov, editors, LPAR, volume 4246 of LNCS, pages 422–436. Springer, 2006. [SRS+ 06] Raja Sengupta, Shahram Rezaei, Steven E. Shladover, Delphine Cody, Susan Dickey, and Hariharan Krishnan. Cooperative collision warning systems: Concept deﬁnition and experimental implementation. PATH Research Report UCB-ITS-PRR-2006-6, Institute of Transportation Studies, University of California, Berkeley, 2006. [Tar51] Alfred Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley, 2nd edition, 1951. [vBMR+ 06] D. A. van Beek, Ka L. Man, Michel A. Reniers, J. E. Rooda, and Ramon R. H. Schiﬀelers. Syntax and consistent equation semantics of hybrid Chi. J. Log. Algebr. Program., 68(1-2):129– 210, 2006. [Wal98] Wolfgang Walter. Ordinary Diﬀerential Equations. Springer, 1998. [ZPC10] Paolo Zuliani, Andr´ Platzer, and Edmund M. Clarke. Bayesian statistical model checking with e application to Simulink/Stateﬂow veriﬁcation. In Karl Henrik Johansson and Wang Yi, editors, HSCC, pages 243–252. ACM, 2010. [ZRH92] Chaochen Zhou, Anders P. Ravn, and Michael R. Hansen. An extended duration calculus for hybrid real-time systems. In Grossman et al. [GNRR93], pages 36–59.

[Koz97]