TXT

# A Temporal Dynamic Logic for Verifying Hybrid System Invariants...

By Laura Olson,2014-05-27 15:05
9 views 0
A Temporal Dynamic Logic for Verifying Hybrid System Invariants...

??ÎÄÓÉcoowind152??Ï×

pdfÎÄµµ?ÉÄÜÔÚWAP?Ëä?ÀÀÌåÑé???Ñ????ÒéÄúÓÅÏÈÑ?ÔñTXT???òÏÂÔØÔ?ÎÄ?þµ????ú?é????

A Temporal Dynamic Logic for Verifying Hybrid System Invariants

Andr?ä Platzer e

University of Oldenburg, Department of Computing Science, Germany Carnegie Mellon University, Computer Science Department, Pittsburgh, PA platzer@informatik.uni-oldenburg.de

Abstract. We combine ?rst-order dynamic logic for reasoning about possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports veri?cation of hybrid programs with ?rst-order de?nable ?ows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of ?nal states. Further, we prove that this gives a conservative extension of dynamic logic. On this basis, we provide a modular veri?cation calculus that reduces correctness of temporal behaviour of hybrid systems to non-temporal reasoning. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints. Keywords: dynamic logic, temporal logic, sequent calculus, logic for hybrid systems, deductive veri?cation of embedded systems

1

Introduction

Correctness of real-time and hybrid systems depends on a safe operation throughout all states of all possible trajectories, and the behaviour at intermediate states is highly relevant [1, 7, 9, 12, 14, 23]. Temporal logics (TL) use temporal operators to talk about intermediate states [1, 10, 11, 24]. They have been used successfully in model checking [1, 6, 14, 15, 18] of ?nite-state system abstractions. Continuous state spaces of hybrid systems, however, often do not admit equivalent ?nite-state abstractions [14,18]. Instead of model checking, TL can also be used deductively to prove validity of formulas in calculi [8, 9]. Valid TL formulas, however, only express very generic facts that are true for all systems, regardless of their actual behaviour. Hence, the behaviour of a speci?c system ?rst needs to be axiomatised declaratively to obtain meaningful results. Then, however, the correspondence between actual system operations and a declarative temporal representation may be questioned.

This research was supported by a fellowship of the German Academic Exchange Service (DAAD). It was also sponsored by the German Research Council (DFG) as part of the Transregional Collaborative Research Center ??Automatic Veri?cation and Analysis of Complex Systems??

(SFB/TR 14 AVACS, see www.avacs.org).

S. Artemov and A. Nerode (Eds.): LFCS 2007, LNCS 4514, pp. 457?C471, 2007. c Springer-Verlag Berlin Heidelberg 2007

458

Andr?ä Platzer e

Dynamic logic (DL) [13] is a successful approach for deductively verifying (in?nite-state) systems [2, 3, 13, 16]. Like model checking, DL can analyse the behaviour of actual system models, which are speci?ed operationally. Yet, operational models are internalised within DL-formulas, and DL is closed under logical operators. Thus, DL can refer to multiple systems and analyse their relationship. This can be important for verifying larger systems compositionally or for investigating re?nement relations, see [22]. Further, Davoren and Nerode [9] argue that, unlike model checking, deductive methods support formulas with free parameters. However, DL only considers the behaviour at ?nal states, which is insu?cient for verifying safety invariants that have to hold all the time. We close this gap of expressivity by combining ?rst-order dynamic logic [13] with temporal logic [10,11,24]. Moreover, we generalise both operational system models and semantics to hybrid systems [14]. In this paper, we introduce a temporal dynamic logic dTL, which provides modalities for quantifying over traces of hybrid systems. We equip it with temporal operators to state what is true all along a trace or at some point during a trace. As in our non-temporal dynamic logic dL [19, 20, 22], we use hybrid programs as an operational model for hybrid systems. They admit a uniform treatment of interacting discrete and continuous evolution in logic. As a semantical foundation for combined temporal dynamic formulas, we introduce a hybrid trace semantics for dTL. We prove that dTL is a conservative extension of dL: for non-temporal speci?cations, trace semantics is equivalent to the non-temporal ?nal state semantics of [19, 22]. As a means for veri?cation, we introduce a sequent calculus for dTL that successively reduces temporal statements about traces of hybrid programs to non-temporal formulas. In this way, we make the intuition formally precise that safety invariants can be checked by augmenting proofs with appropriate assertions about intermediate states. Like in [22], our calculus supports compositional reasoning. It structurally decomposes correctness statements about hybrid programs into corresponding statements about its parts by symbolic transformation. Our approach combines the advantages of DL in reasoning about the behaviour of (multiple and parametric) operational system models with those of TL to verify temporal statements about traces. On the downside, we show that our logic is incomplete. Yet, reachability in hybrid systems is already undecidable [14]. We argue that, despite this theoretical obstacle, dTL can verify practical systems and

demonstrate this by studying safety invariants in train control [7, 12]. The ?rst contribution of this paper is the logic dTL, which provides a coherent foundation for reasoning about the temporal behaviour of operational models of hybrid systems with symbolic parameters. The main contribution is our calculus for deductively verifying temporal statements about hybrid systems. Hybrid Systems. The behaviour of safety-critical systems typically depends on both the state of a discrete controller and continuous physical quantities. Hybrid systems are mathematical models for dynamic systems with interacting discrete

A Temporal Dynamic Logic for Verifying Hybrid System Invariants

459

and continuous behaviour [9,14]. Their behaviour combines continuous evolution (called ?ow ) characterised by di?erential equations and discrete jumps. Dynamic Logic. The principle of dynamic logic is to combine system operations and correctness statements about system states within a single speci?cation language (see [13] for a general introduction in the discrete case). By permitting system operations ?Á as actions of modalities, dynamic logic provides formulas of the form [?Á]?Õ and ?Á ?Õ, where [?Á]?Õ expresses that all terminating runs of system ?Á lead to ?nal states in which condition ?Õ holds. Likewise, ?Á ?Õ expresses that it is possible for ?Á to execute and result in a ?nal state satisfying ?Õ. In dTL, hybrid programs [19, 20, 22] play the role of ?Á. In this paper, we modify the semantics of [?Á] to refer to all traces of ?Á rather than only all ?nal states reachable with ?Á (similarly for ?Á ). For instance, the formula [?Á] ?Õ expresses that ?Õ is true at each state during all traces of the hybrid system ?Á. With this, dTL can also be used to verify temporal statements about the behaviour of ?Á at intermediate states during system runs. Related Work. Based on [25], Beckert and Schlager [4] added separate trace modalities to dynamic logic and presented a relatively complete calculus. Their approach only handles discrete state spaces. In contrast, dTL works for hybrid programs with continuous state spaces. There, a particular challenge is that invariants may change their truth-value during a single continuous evolution. Mysore et al. [18] analysed model checking of TCTL [1] properties for semialgebraic hybrid systems and proved undecidability. Our logic internalises operational models and supports multiple parametric systems. Zhou et al. [26] presented a duration calculus extended by mathematical expressions with derivatives of state variables. Their calculus is unwieldy as it uses a multitude of rules and requires external mathematical reasoning about derivatives and continuity. Davoren and Nerode [9] extended the propositional modal ?Ì-calculus with a semantics in hybrid systems and examine topological aspects. In [8], Davoren et al. gave a semantics in general ?ow systems for a generalisation of CTL? [11]. In both cases,

the authors of [9] and [8] provided Hilbert-style calculi to prove formulas that are valid for all systems simultaneously using abstract actions. The strength of our logic primarily is that it is a ?rst-order dynamic logic: it handles actual hybrid programs like x := x + 1; x = 2y rather than only abstract ?B actions of unknown e?ect. Our calculus directly supports veri?cation of hybrid programs with ?rst-order de?nable ?ows; ?rst-order approximations of more general ?ows can be used according to [23]. First-order DL is more expressive and calculi are deductively stronger than other approaches [4, 17]. Structure of this Paper. After introducing syntax and semantics of the temporal dynamic logic dTL in Sect. 2, we introduce a sequent calculus for verifying temporal dTL speci?cations of hybrid systems in Sect. 4 and prove soundness. In Sect. 5, we prove safety invariants of the train control system presented in Sect. 3.

460

Andr?ä Platzer e

Alternating path and trace quanti?ers for liveness veri?cation are discussed in Sect. 6. Finally, we draw conclusions and discuss future work in Sect. 7.

2

2.1

Temporal Dynamic Logic for Hybrid Systems

Overview: The Basic Concepts of dTL

The temporal dynamic logic dTL extends dynamic logic [13] with three concepts for verifying temporal speci?cations of hybrid systems: Hybrid programs. The behaviour of hybrid systems can be described by hybrid programs [19, 20, 22], which generalise real-time programs [15] to hybrid change. The distinguishing feature of hybrid programs in this context is that they provide uniform discrete jumps and continuous evolutions along di?erential equations. While hybrid automata [14] can be embedded, program structures are more amenable to compositional symbolic processing by calculus rules [19]. Modal operators. Modalities of dynamic logic express statements about all possible behaviour ([?Á]?Ð) of a system ?Á, or about the existence of a trace ( ?Á ?Ð), satisfying condition ?Ð. As in [19, 20, 22], the system ?Á is described as a hybrid program. Yet, unlike in standard dynamic logic [13], ?Ð is a trace formula in dTL, and ?Ð is allowed to refer to all states that occur during a trace using temporal operators. Temporal operators. For dTL, the temporal trace formula ?Õ expresses that the formula ?Õ holds all along a trace selected by [?Á] or ?Á . For instance, the state formula ?Á ?Õ says that the state formula ?Õ holds at every state along at least one trace of ?Á. Dually, the trace formula ??Õ expresses that ?Õ holds at some point during such a trace. It can occur in a state formula ?Á ??Õ to express that there is such a state in some trace of

?Á, or as [?Á]??Õ to say that, along each trace, there is a state satisfying ?Õ. In this paper, the primary focus of attention is on homogeneous combinations of path and trace quanti?ers like [?Á] ?Õ or ?Á ??Õ. 2.2 Syntax of dTL

State and Trace Formulas. The formulas of dTL are built over a non-empty set V of real-valued variables and a ?xed signature ?? of function and predicate symbols. For simplicity, ?? is assumed to contain exclusively the usual function and predicate symbols for real arithmetic, such as 0, 1, +, ??, =, ?Ü, <, ?Ý, >. The set Trm(V ) of terms is de?ned as in classical ?rst-order logic. The formulas of dTL are de?ned similar to ?rst-order dynamic logic [13]. However, the modalities [?Á] and ?Á accept trace formulas that refer to the temporal behaviour of all states along a trace. Inspired by CTL and CTL? [10, 11], we distinguish between state formulas, that are true or false in states, and trace formulas, that are true or false for system traces. The sets Fml(V ) of state formulas, FmlT (V ) of trace formulas, and HP(V ) of hybrid programs with variables in V are simultaneously inductively de?ned in De?nition 1 and 2, respectively.

A Temporal Dynamic Logic for Verifying Hybrid System Invariants

461

De?nition 1 (Formulas). The set Fml(V ) of (state) formulas is simultaneously inductively de?ned as the smallest set such that: 1. 2. 3. 4. If If If If p ?Ê ?? is a predicate, ?È1 , . . . , ?Èn ?Ê Trm(V ), then p(?È1 , . . . , ?Èn ) ?Ê Fml(V ). ?Õ, ?× ?Ê Fml(V ), then ??Õ, (?Õ ?Ä ?×), (?Õ ?Å ?×), (?Õ ?ú ?×) ?Ê Fml(V ). ?Õ ?Ê Fml(V ) and x ?Ê V , then ?x ?Õ, ?x ?Õ ?Ê Fml(V ). ?Ð ?Ê FmlT (V ) and ?Á ?Ê HP(V ), then [?Á]?Ð, ?Á ?Ð ?Ê Fml(V ).

The set FmlT (V ) of trace formulas is the smallest set with: 1. If ?Õ ?Ê Fml(V ), then ?Õ ?Ê FmlT (V ). 2. If ?Õ ?Ê Fml(V ), then ?Õ, ??Õ ?Ê FmlT (V ). Formulas without and ?, i.e., without case 2 of the trace formulas, are called non-temporal dL formulas [19, 22]. Unlike in CTL, state formulas are true on a trace (case 1) if they hold for the last state of a trace, not for the ?rst. Thus, [?Á]?Õ expresses that ?Õ is true at the end of each trace of ?Á. In contrast, [?Á] ?Õ expresses that ?Õ is true all along all states of every trace of ?Á. This combination gives a smooth embedding of non-temporal dL into dTL and makes it possible to de?ne a compositional calculus. Like CTL, dTL allows nesting with a branching time semantics [10], e.g., [?Á] (x ?Ý 2 ?ú ?Ã ?x ?Ü 0). Hybrid Programs. The hybrid programs [19, 20, 22] occurring in dynamic modalities of dTL are built from elementary discrete jumps and continuous evolutions using a regular control structure [13]. De?nition 2 (Hybrid programs). The set HP(V ) of hybrid programs is inductively de?ned as the smallest set such that: 1. 2. 3. 4. 5. 6. If If If If If If x ?Ê V and ?È ?Ê Trm(V ), then (x := ?È) ?Ê HP(V ).

x ?Ê V and ?È ?Ê Trm(V ), then (x = ?È) ?Ê HP(V ). ?B ?Ö ?Ê Fml(V ) is quanti?er-free and ?rst-order, then (??Ö) ?Ê HP(V ). ?Á, ?Ã ?Ê HP(V ) then (?Á ?È ?Ã) ?Ê HP(V ). ?Á, ?Ã ?Ê HP(V ) then (?Á; ?Ã) ?Ê HP(V ). ?Á ?Ê HP(V ) then (?Á? ) ?Ê HP(V ).

The e?ect of x := ?È is an instantaneous discrete jump in state space or a mode switch. That of x = ?È is an ongoing continuous evolution regulated by the ?B di?erential equation with time-derivative x of x and term ?È (accordingly for ?B systems of di?erential equations). Test actions ??Ö are used to de?ne conditions. Their semantics is that of a no-op if ?Ö is true in the current state, and that of a dead end operator aborting any further evolution, otherwise. The sequential composition ?Á; ?Ã, nondeterministic choice ?Á ?È ?Ã, and non-deterministic repetition ?Á? of system actions are as usual [13]. They can be combined with ??Ö to form other control structures [13]. In dTL, there is no need to distinguish between discrete and continuous variables or between system parameters and state variables, as they share the same

462

Andr?ä Platzer e

uniform semantics. For pragmatic reasons, an informal distinction can nevertheless improve readability. For instance, ?x [x = ?x]x ?Ü 5 expresses that there is a ?B choice of the initial value for x (which could be a parameter) such that after all evolutions along x = ?x, the outcome of the state variable x will be at most 5. ?B 2.3 Trace Semantics of dTL

In standard dynamic logic [13] and dL [19, 22], modalities only refer to the ?nal states of system runs and the semantics is a reachability relation on states: State ?Ø is reachable from state ?Í using ?Á if there is a run of ?Á which terminates in ?Ø when started in ?Í. For dTL, however, formulas can refer to intermediate states of runs as well. Thus, the semantics of a hybrid system ?Á is the set of its possible traces, i.e., successions of states that occur during the evolution of ?Á. States contain values of system variables during a hybrid evolution. A state is a map ?Í : V ?ú R; the set of all states is denoted by Sta(V ). In addition, we distinguish a state ?? to denote the failure of a system run when it is aborted due to a test ??Ö that yields false. In particular, ?? can only occur at the end of an aborted system run and marks that there is no further extension. Hybrid systems evolve along piecewise continuous traces in multi-dimensional space as time passes. Continuous phases are governed by di?erential equations, whereas discontinuities are caused by discrete jumps in state space. Unlike in discrete cases [4,25], traces are not just sequences of states, since hybrid systems pass through uncountably many states even in bounded time. Beyond that, continuous changes are more involved than in pure real-time [1, 15], because all variables can evolve along

di?erent di?erential equations. Generalising the realtime traces of [15], the following de?nition captures hybrid behaviour by splitting the uncountable succession of states into periods ?Òi that are regulated by the same control law. For discrete jumps, some periods are point ?ows of duration 0. De?nition 3 (Hybrid Trace). A trace is a (non-empty) ?nite or in?nite sequence ?Ò = (?Ò0 , ?Ò1 , ?Ò2 , . . . ) of functions ?Òi : [0, ri ] ?ú Sta(V ) with respective durations ri ?Ê R (for i ?Ê N). A position of ?Ò is a pair (i, ?Æ) with i ?Ê N and ?Æ in the interval [0, ri ]; the state of ?Ò at (i, ?Æ) is ?Òi (?Æ). Positions of ?Ò are ordered lexicographically by (i, ?Æ) (j, ?Î) i? either i < j, or i = j and ?Æ < ?Î. Further, for a state ?Í ?Ê Sta(V ), ?Í : 0 ?ú ?Í is the point ?ow at ?Í with duration 0. A trace ? terminates if it is a ?nite sequence (?Ò0 , ?Ò1 , . . . , ?Òn ) and ?Òn (rn ) = ??. In that case, the last state last ?Ò is denoted as ?Òn (rn ). The ?rst state ?rst ?Ò is ?Ò0 (0). Unlike in [1, 15], the de?nition of traces also admits ?nite traces of bounded duration, which is necessary for compositionality of traces in ?Á; ?Ã. The semantics of hybrid programs ?Á as the set ?Ó(?Á) of its possible traces depends on valuations val(?Í, ??) of formulas and terms at intermediate states ?Í. The valuation of terms [13], and interpretations of function and predicate symbols are as usual for real arithmetic. The valuation of formulas will be de?ned in De?nition 5. We use ?Í[x ?ú d] to denote the modi?cation that agrees with state ?Í on all variables except for the symbol x, which is changed to d ?Ê R.

A Temporal Dynamic Logic for Verifying Hybrid System Invariants

463

De?nition 4 (Trace semantics of hybrid programs). The trace semantics, ?Ó(?Á), of a hybrid program ?Á, is the set of all its possible hybrid traces and is de?ned as follows: 1. ?Ó(x := ?È) = {(?, ?Ø ) : ?Ø = ?Í[x ?ú val(?Í, ?È)] for ?Í ?Ê Sta(V )} ?Í ? 2. ?Ó(x = ?È) = {(f ) : 0 ?Ü r ?Ê R and f : [0, r] ?ú Sta(V ) is such that the func?B tion val(f (?Æ), x) is continuous in ?Æ on [0, r] and has a derivative of value val(f (?Æ), ?È) at each ?Æ ?Ê (0, r). Variables without a di?erential equation do not change} 3. ?Ó(??Ö) = {(?) : val(?Í, ?Ö) = true} ?È {(?, ??) : val(?Í, ?Ö) = false} ?Í ?Í ? 4. ?Ó(?Á ?È ?Ã) = ?Ó(?Á) ?È ?Ó(?Ã) 5. ?Ó(?Á; ?Ã) = {?Ò ? ? : ?Ò ?Ê ?Ó(?Á) , ? ?Ê ?Ó(?Ã) when ?Ò ? ? is de?ned}; the composition of ?Ò = (?Ò0 , ?Ò1 , ?Ò2 , . . . ) and ? = (?0 , ?1 , ?2 , . . . ) is ? ?(?Ò0 , . . . , ?Òn , ?0 , ?1 , . . . ) if ?Ò terminates at ?Òn and last ?Ò = ?rst ? ? ?Ò?? = ?Ò if ?Ò does not terminate ? ? not de?ned otherwise 6. ?Ó(?Á? ) =

n?ÊN

?Ó(?Án ), where ?Án+1 = (?Án ; ?Á) for n ?Ý 1, and ?Á0 = (?true).

Time passes di?erently during discrete and continuous change. During continuous evolution, the discrete step index i of positions

(i, ?Æ) remains constant, whereas the continuous duration ?Æ remains 0 during discrete point ?ows. This permits multiple discrete state changes to happen at the same (super-dense) continuous time, unlike in [1]. De?nition 5 (Valuation of formulas). The valuation of state and trace formulas is de?ned respectively. For state formulas, the valuation val(?Í, ??) with respect to state ?Í is de?ned as follows: 1. val(?Í, p(?È1 , . . . , ?Èn )) = p val(?Í, ?È1 ), . . . , val(?Í, ?Èn ) , where p is the relation associated to p. 2. val(?Í, ?Õ ?Ä ?×) is de?ned as usual, the same holds for ?, ?Å, ?ú. 3. val(?Í, ?x ?Õ) = true :?? val(?Í[x ?ú d], ?Õ) = true for all d ?Ê R 4. val(?Í, ?x ?Õ) = true :?? val(?Í[x ?ú d], ?Õ) = true for some d ?Ê R 5. val(?Í, [?Á]?Ð) = true :?? for each trace ?Ò ?Ê ?Ó(?Á) that starts in ?rst ?Ò = ?Í, if val(?Ò, ?Ð) is de?ned, then val(?Ò, ?Ð) = true. 6. val(?Í, ?Á ?Ð) = true :?? there is a trace ?Ò ?Ê ?Ó(?Á) starting in ?rst ?Ò = ?Í, such that val(?Ò, ?Ð) = true. For trace formulas, the valuation val(?Ò, ??) with respect to trace ?Ò is: 1. If ?Õ is a state formula, then val(?Ò, ?Õ) = val(last ?Ò, ?Õ) if ?Ò terminates, whereas val(?Ò, ?Õ) is not de?ned if ?Ò does not terminate. 2. val(?Ò, ?Õ) = true :?? val(?Òi (?Æ), ?Õ) = true for all positions (i, ?Æ) of ?Ò with ?Òi (?Æ) = ??. 3. val(?Ò, ??Õ) = true :?? val(?Òi (?Æ), ?Õ) = true for some position (i, ?Æ) of ?Ò with ?Òi (?Æ) = ??. As usual, a (state) formula is valid if it is true in all states.

464

Andr?ä Platzer e

2.4

Conservative Temporal Extension

The following result shows that the extension of dTL by temporal operators does not change the meaning of non-temporal dL formulas. The trace semantics given in De?nition 5 is equivalent to the ?nal state reachability relation semantics [19, 22] for the sublogic dL of dTL. A proof for this can be found in [21]. Proposition 1. The logic dTL is a conservative extension of non-temporal dL, i.e., the set of valid dL-formulas is the same with respect to transition reachability semantics of dL [19, 22] as with respect to the trace semantics of dTL (De?nition 5).

3

Safety Invariants in Train Control

In the European Train Control System (ETCS) [12], trains are coordinated by decentralised Radio Block Centres (RBC), which grant or deny movement authorities (MA) to the individual trains by wireless communication. In emergencies, trains always have to stop within the MA issued by the RBC, see Fig. 1. Following the reasoning pattern for tra?c agents in [7], each train negotiates with the RBC to extend its MA when approaching the end, say m, of its current MA. Since wireless

communication takes time, this negotiation is initiated in due time before reaching m. During negotiation, trains are assumed to keep their desired speed as in [7]. Before entering negotiation at some point ST, the train still has su?cient distance to MA (it is in far mode) and can regulate its speed freely within the track limits. Depending on weather conditions, slope of track etc., the local train motion control determines a safety envelope s around the train, within which it considers driving safe, and adjusts its acceleration a in accordance with s (called correction [7]). In particular, depending on the maximum RBC response time, this determines the latest point, SB, on the track where a response from the RBC must have arrived to guarantee safe driving.

RBC

far

ST

negot SB

corr

MA

Fig. 1. ETCS train coordination by movement authorities

As a model for train movements, we use the ideal-world model adapted from [7]. It does not model friction, slopes, or mass of train but is perfectly suitable for analysing the cooperation level of train control [7]. The local safety

A Temporal Dynamic Logic for Verifying Hybrid System Invariants

465

properties that where used when verifying the cooperation protocol can then be shown for more detailed models of individual components. For a safe operation of multiple tra?c agents, it is crucial that the MA is respected at every point in time during this protocol, not only at its end. Hence, we need to consider temporal safety invariants. For instance, when the train has entered the negotiation phase at its current position z, dTL can analyse the following safety invariant of a part of the train controller: ?× ?ú [negot; corr; z = v, v = a] ( ?Ü L ?ú z < m) ?B ?B where negot ?Ô z = v, ?B = 1 ?B corr ?Ô (?m ? z < s; a := ?b) ?È (?m ? z ?Ý s; a := . . . ) . (1)

It expresses that?ªunder a sanity condition ?× for parameters?ªa train will always remain within its MA m, as long as the accumulated RBC negotiation latency is at most L. We refer to [12] for details on what contributes to . Like in [7], we model the train to ?rst negotiate while keeping a constant speed (z = v) in negot. ?B Thereafter, in corr , the train corrects its acceleration or brakes with force b (as a failsafe recovery manoeuvre) on the basis of the remaining distance (m ? z). Finally, the train continues moving according to the system (z = v, v = a) or, ?B ?B equivalently, z = a. Instead of manually choosing speci?c

values for the free ?? parameters of (1) as in [7,12], we will use the techniques developed in this paper to automatically synthesise constraints on the relationship of parameters that are required for a safe operation of cooperative train control.

4

A Veri?cation Calculus for Safety Invariants

In this section, we introduce a sequent calculus for verifying temporal speci?cations of hybrid systems in dTL. With the basic idea being to perform a symbolic decomposition, hybrid programs are successively transformed into simpler logical formulas describing their e?ects. There, statements about the temporal behaviour of a hybrid program are successively reduced to corresponding nontemporal statements about the intermediate states. For propositional logic, standard rules P1?CP9 are listed in Fig. 2. The rule P10 is a shortcut to handle quanti?ers of ?rst-order real arithmetic, which is decidable. We use P10 as a modular interface to arithmetic and refer to [19] for a goal-oriented integration of arithmetic, which combines with dTL. Rules D1?CD8 work similar to those in [3,13]. For handling discrete change, D8 inductively uses substitutions. D9?CD10 handle continuous evolutions given a ?rst-order de?nable ?ow yx . In particular, in conjunction with P10, they fully encapsulate handling of di?erential equations within hybrid systems. Rules T1?CT10 successively transform temporal speci?cations of hybrid programs into non-temporal dL formulas. The idea underlying this transformation is to decompose hybrid programs and recursively augment intermediate state transitions with appropriate speci?cations. D1?CD2 are identical for dTL and dL speci?cations, hence they apply for all trace formulas ?Ð and not just for state formulas. Rules for handling [?Á]??Õ and ?Á ?Õ are discussed in Sect. 6.

466

Andr?ä Platzer e

4.1

Rules of the Calculus

A sequent is of the form ?? ?, where ?? and ? are ?nite sets offormulas. Its semantics is that of the formula ?Õ?Ê?? ?Õ ?ú ?×?Ê? ?× and will be treated as an abbreviation. In the following, an update U is a list of discrete assignments of the form x := ?È (see [3] for advanced update techniques, which can be combined with our calculus). De?nition 6 (Provability, derivability). A formula ?× is provable from a set ?µ of formulas, denoted by ?µ dTL ?× i? there is a ?nite set ?µ0 ? ?µ for which the sequent ?µ0 ?× is derivable. In turn, a sequent of the form ??, U ?µ U ??, ? (for some update U, including the empty update, and ?nite sets ??, ? of context formulas) is derivable i? there is an instance ?µ1 ??1 ???? ?µ ?? ?µn ??n

Report this document

For any questions or suggestions please email
cust-service@docsford.com