Martin De Wulf

Laurent Doyen

Nicolas Markey

Jean-François Raskin

Robustness and Implementability of Timed Automata

In a former paper, we defined a new semantics for timed automata, the Almost ASAP semantics, which is parameterized by ∆ to cope with the reaction delay of the controller. We showed that this semantics is implementable provided there exists a strictly positive value for the parameter ∆ for which the strategy is correct. In this paper, we define the implementability problem to be the question of existence of such a ∆. We show that this question is closely related to a notion of robustness for timed automata defined in [Pur98] and prove that the implementability problem is decidable.

Introduction

Timed automata are an important formal model for the specification and analysis of real-time systems. Formalisms like timed automata and hybrid automata are central in the so-called model-based development methodology for embedded controllers. The steps underlying that methodology can be summarized as follows: (i) construct a (timed/hybrid automaton) model Env of the environment in which the controller will be embedded; (ii) make clear what is the control objective: for example, prevent the environment to enter a set of Bad states; (iii) design a (timed automata) model Cont of the control strategy; (iv) verify that Reach( Env Cont ) ∩ Bad = ∅ (where Reach( Env Cont ) denotes the set of states reachable in the transition system associated to the synchronized product of the automaton for the environment and the automaton for the controller). When Cont has been proven correct, it would be valuable to ensure that an implementation Impl of that model can be obtained in a systematic way in order to ensure the conservation of correctness, that is to ensure that Reach( Env Impl ) ∩ Bad = ∅ is obtained by construction.

Unfortunately, this is often not possible for several fundamental and/or technical reasons. First, the notion of time used in the traditional semantics of timed automata is continuous and defines perfect clocks with infinite precision while implementations can only access time through digital and finitely precise clocks. Second, timed automata react instantaneously to events and time-outs while implementations can only react within a given, usually small but not zero, reaction delay. Third, timed automata may describe control strategies that are unrealistic, like zeno-strategies or strategies that ask the controller to act faster and faster [START_REF] Cassez | A comparison of control problems for timed and hybrid systems[END_REF]. For one of those three reasons, a model for a digital controller that has been proven correct may not be implementable (at all) or it may not be possible to turn it systematically into an implementation that is proven correct w.r.t. this model.

To overcome those problems, we recently proposed in [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF] an alternative semantics to timed automata. This semantics is called the Almost ASAP semantics, AASAP for short. The AASAP-semantics of a timed automaton A, noted A AASAP ∆ , is a parametric semantics that leaves as a parameter ∆ ∈ Q ≥0 the reaction delay of the controller. This semantics relaxes the classical semantics of timed automata in that it does not impose on the controller to react instantaneously but imposes on the controller to react within ∆ time units. We have proven that a timed controller is implementable with a sufficiently fast hardware if and only if there exists ∆ ∈ Q >0 such that Reach( Env Cont ∆ ) ∩ Bad = ∅. Details on the notion of implementability can be found in [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF]. The implementability problem is to determine the existence of such a ∆. The decidability of that important problem is open. We will close this open question here.

The use of the AASAP-semantics in the verification phase can be understood intuitively as follows. When we verify a control strategy using the AASAPsemantics, we test if the proposed strategy is robust in the following sense1 : "Is the strategy still correct if it is perturbed a little bit when executed on a device that has a finite speed and uses finitely precise clocks ?"

In this paper, we show that this intuition relating robustness and implementability allows us to draw an interesting and important link with a paper by Puri [START_REF] Puri | Dynamical properties of timed automata[END_REF] and allows us to answer positively the open question about the decidability of the implementability problem.

Related works. In this paper, we focus on timed controllers and environments that can be modeled using timed automata. There exist related works where the interested reader will find other ideas about implementability.

In [START_REF] Alur | Generating embedded software from hierarchical hybrid models[END_REF], Rajeev Alur et al consider the more general problem of generating code from hybrid automata, but they only sketch a solution and state interesting research questions. The work in this paper should be useful in that context.

In [AFM + 02,AFP + 03], Wang Yi et al present a tool called Times that generates executable code from timed automata models. However, they make the synchrony hypothesis and so they assume that the hardware on which the code is executed is infinitely fast and precise.

In [START_REF] Henzinger | From control models to real-time code using Giotto[END_REF], Tom Henzinger et al introduce a programming model for realtime embedded controllers called Giotto. Giotto is an embedded software model that can be used to specify a solution to a given control problem independently of an execution platform but which is closer to executable code than a mathematical model. So, Giotto can be seen an intermediary step between mathematical models like hybrid automata and real execution platforms.

Our paper is structured as follows. In Section 2, we recall some classical definitions related to timed automata and we introduce a general notion of enlarged semantics for those automata. In Section 3, we recall the essential notions and problems related to the AASAP-semantics, and we recall the notion of robustness as introduced by Puri in [START_REF] Puri | Dynamical properties of timed automata[END_REF]. In Section 4, we present a small example that illustrates the enlarged semantics and the problems that we want to solve on this semantics. In Section 5, we make formal the link between our notion of implementability and the notion of robustness introduced by Puri. In Section 6, we give a direct proof that the implementability problem is decidable. Finally, we close the paper by a conclusion.

Complete proofs can be found in a longer version of this paper at the following web page: http://www.ulb.ac.be/di/ssd/cfv/publications.html.

Preliminaries

Definition 1 [TTS] A timed transition system T is a tuple S, ι, Σ, → where S is a (possibly infinite) set of states, ι ∈ S is the initial state, Σ is a finite set of labels, and → ⊆ S × Σ ∪ R ≥0 × S is the transition relation where R ≥0 is the set of positive real numbers. If (q, σ, q ) ∈ → we write q σ -→ q .

A trajectory of a TTS T = S, ι, Σ, → is a sequence π = (s 0 , t 0 ) . . . (s k , t k ) such that for 0 ≤ i ≤ k, (s i , t i ) ∈ S × R and for 0 ≤ i < k, s i σ -→ s i+1 and either σ ∈ Σ and t i+1 = t i , or σ ∈ R >0 and t i+1 = t i + σ. We sometimes refer to this trajectory as π[t 0 , t k ] and write π(t i ) instead of q i . A trajectory is stutter-free iff it is not the case for any i that q i τ i -→ q i+1 and q i+1 τ i+1 ---→ q i+2 with τ i , τ i+1 ∈ R >0 . A state s of T is reachable if there exists a trajectory π = (s 0 , t 0 ) . . . (s k , t k ) such that s 0 = ι and s n = s. The set of reachable states of T is noted Reach(T ).

Given a set Var = {x 1 , . . . , x n } of clocks, a clock valuation is a function v : Var → R ≥0 . In the sequel, we often say that a clock valuation is a point

in R n . If R ⊆ Var, then v[R := 0] denotes the valuation v such that v (x) = 0 if x ∈ R v(x) if x ∈ R
A closed rectangular guard g over {x 1 , . . . , x n } is a set of inequalities of the form a i ≤ x i ≤ b i , one for each x i where a i , b i ∈ Q ≥0 ∪ {+∞} and a i ≤ b i . We write Rect c (Var) for the set of closed rectangular guards over Var. For ∆ ≥ 0, we define

g ∆ = {(x 1 , . . . , x n ) | a i -∆ ≤ x i ≤ b i + ∆} ⊆ R n . When ∆ = 0, we write g instead of g 0 .
We slightly modify the classical definitions related to timed automata [START_REF] Alur | A theory of timed automata[END_REF]. In particular, guards on edges are rectangular and closed 2 . Also the value of their clock is bounded by M , the largest constant appearing in guards. The last restriction does not reduce the expressive power of timed automata.

Definition 2 [Timed automaton] A timed automaton is a tuple A = Loc, Var, q 0 , Lab, Edg where -Loc is a finite set of locations representing the discrete states of the automaton. -Var = {x 1 , . . . , x n } is a finite set of real-valued variables.

q 0 = (l 0 , v 0 ) where l 0 ∈ Loc is the initial location and v 0 is the initial clock valuation such that ∀x ∈ Var :

v 0 (x) ∈ N ∧ v 0 (x) ≤ M . -Lab is a finite alphabet of labels. -Edg ⊆ Loc×Loc×Rect c (Var)×Lab×2
Var is a set of edges. An edge (l, l , g, σ, R) represents a jump from location l to location l with guard g, event σ and a subset R ⊆ Var of variables to be reset.

We now define a family of semantics for timed automata that is parameterized by ∈ Q ≥0 (drift on clocks) and ∆ ∈ Q ≥0 (imprecision on guards).

Definition 3 [Enlarged semantics of timed automata] The semantics of a timed automaton A = Loc, Var, q 0 , Lab, Edg , when the two parameters and ∆ are fixed is given by the TTS A ∆ = S, ι, Σ, → where

1. S = {(l, v) | l ∈ Loc ∧ v : Var → [0, M ]}. 2. ι = q 0 . 3. Σ = Lab.
(l, v), t, (l , v )) ∈ → iff l = l and v (x i )- v(x i ) ∈ [(1 -)t, (1 + )t] for i = 1 . . . n.
In the sequel, we write A for A 0 0 , which is the classical semantics of timed automata.

Remark Our definition of timed automata does not use strict inequalities; this simplifies the presentation and is not restrictive. Indeed, consider a timed automaton A with (possibly open) rectangular guards and the closure automaton A resulting from A by replacing strict inequalities by non-strict ones. It appears obviously that

Reach( A ∆ 2 ) ⊆ Reach( A ∆ ) and Reach( A ∆ ) ⊆ Reach( A ∆ ),
and hence the implementability problem on A "Does there exist ∆ ∈ Q >0 such that Reach( A ∆ ) ∩ Bad = ∅ ?" is equivalent to the the implementability problem on A.

We now recall some additional classical notions related to timed automata.

Let x denote the integer part of x (the greatest integer k ≤ x), and x denote its fractional part.

Definition 4 [Clock regions] A clock region is an equivalence class of the relation ∼ defined over the clock valuations in Var → [0, M ]. We have v ∼ w iff all the following conditions hold:

-∀x ∈ Var : v(x) = w(x) . -∀x, y ∈ Var : v(x) ≤ v(y) iff w(x) ≤ w(y) . -∀x ∈ Var : v(x) = 0 iff w(x) = 0.
We write ]v[ for the clock region containing v. It is easy to see that ]v[ contains the valuations that agree with v on the integer part of the variables, and on the ordering of their fractional part and 0. The closure of the region containing v is noted [v]. Such a set is called a closed region.

Definition 5 [Region graph] Given the TTS A = S, s 0 , Σ, → A of a timed automaton A, we define the corresponding region graph G = C, → G of A :

-C = {(l, [v]) | (l, v) ∈ S} is the set of closed regions. -→ G ⊆ C × C. ((l, [v]), (l , [v ])) ∈→ G if (l, v)→ A (l , v ) and (l, [v]) = (l , [v ]).
This definition is meaningful since C is finite and whenever

(l, [v]) → G (l , [v ]), for any s ∈ [v] there exists s ∈ [v ] such that (l, s)→ A (l , s ), and for any s ∈ [v ] there exists s ∈ [v] such that (l, s)→ A (l , s ) [AD94].
Let W = |C| be the total number of regions.

Definition 6 [Zones] A zone Z ⊆ R n is a closed set defined by inequalities of the form x i -x j ≤ m ij , α i ≤ x i ≤ β i where 1 ≤ i, j ≤ n and m ij , α i , β i ∈ Z.
A set of states is called a zone-set if it is a finite union of sets of the form {l} × Z where l is a location and Z is a zone.

Definition 7 [Progress cycle]

A progress cycle in the region graph of a timed automaton is a cycle in which each clock is reset at least once.

Assumption 8 We make the assumption that every cycle in the region graph of the timed automata we consider is a progress cycle.

This assumption, made by Puri in his paper [START_REF] Puri | Dynamical properties of timed automata[END_REF], is not a very restrictive assumption, since it is weaker than classical non-Zeno assumptions in the literature (for example in [START_REF] Asarin | Controller synthesis for timed automata[END_REF], they impose that "in every cycle in the transition graph of the automaton, there is at least one transition which resets a clock variable x i to zero, and at least one transition which can be taken only if x i ≥ 1").

In [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF], we introduced the Almost ASAP semantics. This semantics relaxes the usual semantics of timed automata, its main characteristics are summarized as follows:

-any transition that can be taken becomes urgent only after a small delay ∆ (which may be left as a parameter); -a distinction is made between the occurrence of an event in the environment (sent) and in the controller (received), however the time difference between the two events is bounded by ∆; -guards are enlarged by some small amount depending on ∆.

In the same paper, in Theorem 6, we show that this semantics can be encoded using a syntactical transformation of the automaton controller and by enlarging the guards by the parameter ∆ which takes its value in the positive rationals. So we can study the AASAP-semantics of Env Cont by considering the semantics Env Cont 0 ∆ where Cont is obtained syntactically from Cont. So in the rest of this paper, we will consider the ∆-enlarged semantics instead of the AASAPsemantics.

In this previous work, we have shown that the AASAP-semantics and so the ∆-enlarged semantics allow us to reason about the implementability of a control strategy defined by a timed automaton. The problems that we want to solve algorithmically on the ∆-enlarged semantics are the following ones:

-[Fixed] given a zone-set of Bad states, the timed automata Env and Cont, and a fixed value of ∆ ∈ Q >0 decide whether Reach( Env Cont 0 ∆ ) ∩ Bad = ∅; -[Existence] given a zone-set of Bad states, Env and Cont, decide whether there exists ∆ ∈ Q >0 such that Reach( Env Cont 0 ∆ ) ∩ Bad = ∅. This is also called the implementability problem.

-[Maximization] given a zone-set of Bad states, Env and Cont, compute the least upper bound of the set of ∆ ∈ Q >0 such that Reach( Env Cont 0 ∆ ) ∩ Bad = ∅. Intuitively, this gives us the information about the slowest hardware that can implement correctly the strategy.

To solve the fixed version, we use the usual reachability algorithm for timed automaton defined in [START_REF] Alur | A theory of timed automata[END_REF]. To solve the maximization version (in an approximative way), we observe that for any timed automaton A, any two positive rational numbers

∆ 1 , ∆ 2 , if ∆ 1 ≤ ∆ 2 then Reach( A 0 ∆ 1 ) ⊆ Reach( A 0 ∆ 2 ).
So, given a tolerance η ∈ Q >0 , the maximal value of ∆ can be approached by η as follows: assuming Bad is reachable in A 0 ∆=1 , it suffices to solve the [Fixed] problems with values ∆ i = iη (0 ≤ i ≤ 1 η ), and take as approximation of the maximal ∆ the value ∆ i such that the answer of the [Fixed] problem is Yes for ∆ i and No for ∆ i+1 , which can be found more efficiently with a dichotomy search.

The decidability of the implementability problem is established in the next sections. To achieve this, we draw a strong link with a robust semantics defined by Puri in [START_REF] Puri | Dynamical properties of timed automata[END_REF]. In that paper, Puri shows that the traditional reachability analysis defined in [START_REF] Alur | A theory of timed automata[END_REF] is not correct when the clocks drift even by a very small amount. He then reformulates the reachability problem as follows: given a timed automaton A, instead of computing Reach( A 0 0 ), he proposes an algorithm that computes ∩ ∈Q >0 Reach( A 0 ). When A is clear from the context, this set is denoted by R * . This is the set of states that can be reached when the clocks drift by an infinitesimally small amount. He shows that this set has nice robustness properties with respect to modeling errors. In particular, he establishes that if the clocks are drifting, then guards can be checked with some small imprecisions (see [START_REF] Puri | Dynamical properties of timed automata[END_REF] for details).

In our paper, in order to make the link with the implementability problem, we study a variant of this robust semantics where only small imprecisions on guards checking are allowed: the set of reachable states in this semantics is the set ∩ ∆∈Q >0 Reach( A 0 ∆ ). When A is clear from the context, this set is abbreviated by R * ∆ . We first show that for any timed automaton A, any zone-set Bad, we have that:

∩ ∆∈Q >0 Reach( A 0 ∆ ) ∩ Bad = ∅ iff there exists ∆ ∈ Q >0 such that Reach( A 0 ∆ ) ∩ Bad = ∅.
After, we establish that the algorithm proposed by Puri to compute the set ∩ ∈Q >0 Reach( A 0 ) is also valid to compute the set of states ∩ ∆∈Q >0 Reach( A 0 ∆ ). As corollaries, we obtain that

∩ ∈Q >0 Reach( A 0 ) = ∩ ∆∈Q >0 Reach( A 0
∆ ) and so we obtain an algorithm to decide the implementability problem.

The proofs of our results follow the general ideas of the proofs of Puri and are based on the structure of limit cycles of timed automata (a fundamental notion introduced by Puri) but we needed new techniques to treat the imprecisions on guards instead of the drifts of clocks as in the original paper. Also the proofs in the paper of Puri are not always convincing, so we reproved a large number of his lemmas that are needed to establish our proof and had to correct one of them.

Example

Consider automaton A of Fig. 1. We examine two cases : α = 2 and α = 3. For both cases, the reachable states of the classical semantics A are the same and are depicted in Fig. 2 (the points v 0 . . . v 7 will be used later in the paper). The safety property we want to verify is that the location err is not reachable. Note that in the classical semantics this is true in both cases.

Consider now the enlarged semantics A 0 ∆ with ∆ > 0. In this semantics, guards are enlarged by the amount ∆. The edge from l 1 to l 2 has the guard a ≤ 2 + ∆ and the edge from l 2 to l 1 has the guard b ≥ 2 -∆. Starting from the initial state (l 1 , a = 1, b = 0), the jump to l 2 can occur ∆ time units later, so that the states (l 2 , a = 0, b ≤ 1 + ∆) are reached. Similarly, the transition from l 2 back to l 1 is enabled ∆ time units earlier and the states (l 1 , a ≥ 1 -2∆, b = 0) can be reached. By iterating the cycle, the states (l 1 , a ≥ 1 -2k∆, b = 0) and (l 2 , a = 0, b ≤ 1 + (2k -1)∆) are reachable. So, for any ∆ > 0 some new states

l 1 l 2 err a := 1 b := 0 a ≤ 2 a := 0 b := 0 b ≥ 2 a = 0 b ≥ α Fig. 1. A timed automaton A. 0 1 2 1 2 0 1 2 1 2 b b a a l 1 l 2 .v 7 .v 3 .v 4 .v 2 .v 1 .v 0 .v 5 .v 6
Fig. 2. Reach( A ) for the timed automaton A of Fig. 1. are reachable in A 0 ∆ that were not reachable in the classical semantics. Those states are represented in Fig. 3.

0 1 2 1 2 0 1 2 1 2 b b a a l 1 l 2 .v 7 .v 3 .v 4 .v 2 .v 1 .v 0 .v 5 .v 6
From those new states that become reachable in location l 2 , if α = 3, the location err remains unreachable but if α = 2 it becomes reachable. Clearly, from this example, one sees that a correct timed system (in the sense of the classical semantics) could have a completely different (and potentially bad) behavior due to an infinitesimally small inaccuracy in testing of the clocks (which is unavoidable since the clocks are discrete in embedded systems). This is the case for the automaton of figure 1. When α = 2, the classical semantics is not robust since even the slightest error in guard checking allows new discrete transition to be taken. In other words, there is no strictly positive value for the parameter ∆ that still ensures the safety property for A 0 ∆ . Systems with such features cannot have a correct implementation because their correctness relies on the idealization of the mathematical model.

But this is not always the case: for the same automaton when α = 3, no more discrete transitions are possible in the enlarged semantics than in the classical one. In this case, we can answer positively to the question "Is there a strictly positive value for parameter ∆ that allows the enlarged semantics to still satisfy the safety property?". And indeed, we can prove that any value ∆ < 1 3 is satisfying.

Linking robustness and implementability

The classical semantics of timed automaton A is A =0 ∆=0 , which is a mathematical idealization of how we expect an implementation would behave: it makes the hypothesis that the hardware is perfectly precise and infinitely fast. Unfortunately, the execution of a timed automaton on a real hardware cannot be considered as ideal in the mathematical sense. It is thus an interesting question to know whether a small drift or imprecision of the clocks could invalidate some properties satisfied by the classical semantics. Drifts in clocks have been studied in [START_REF] Puri | Dynamical properties of timed automata[END_REF]. We are interested in studying imprecisions in the evaluation of the guards since it is directly connected to the question of implementability, as explained above. The main result of this paper is the following.

Theorem 9 There exists an algorithm that decide for any timed automaton A, any zone-set Bad if there exists ∆ ∈ Q >0 such that Reach( A 0 ∆ ) ∩ Bad = ∅.

To prove Theorem 9, we show that the set Bad intersects R * ∆ iff it intersects Reach( A 0 ∆ ) for some ∆ > 0. As shown in the next section, Algorithm 1 computes R * ∆ . Consequently, the implementability problem is decidable.

Theorem 10 For any timed automaton A, any zone-set Bad,

R * ∆ ∩ Bad = ∅ iff ∃∆ > 0 : Reach( A 0 ∆ ) ∩ Bad = ∅.
The proof of Theorem 10 relies on two intermediate lemmas, one of which corrects a wrong claim in [START_REF] Puri | Dynamical properties of timed automata[END_REF]: it gives a bound on the distance between two zones with empty intersection. This bound is claimed to be 1 2 . We show that 1 n where n is the dimension of the space is the tightest bound. However the final results of [START_REF] Puri | Dynamical properties of timed automata[END_REF] are not deeply affected by this mistake. The distance considered is defined by

d ∞ (x, y) = x -y ∞ = max 1≤i≤n (|x i -y i |). Let us reformulate that lemma. Lemma 11 (Corrected from [Pur98, Lemma 6.4]) Let Z 1 ⊆ R n and Z 2 ⊆ R n be two zones such that Z 1 ∩ Z 2 = ∅. Then, for any x ∈ Z 1 and y ∈ Z 2 , d ∞ (x, y) ≥ 1
n . This bound is tight.

In the sequel, when a distance d or a norm is used, we always refer to d ∞ and ∞ . The following lemma relies on the theory of real numbers and the basics of topology.

Lemma 12 Let A ∆ (∆ ∈ R >0 ) be a collection of sets such that A ∆ 1 ⊆ A ∆ 2 if ∆ 1 ≤ ∆ 2 . Let A = ∆>0 A ∆ be nonempty. If d(A, B) > 0, then there exists ∆ > 0 such that A ∆ ∩ B = ∅. Proof of theorem 10. If R * ∆ ∩ Bad = ∅, since R * ∆
and Bad are unions of sets of the form {l} × Z l where Z l is a zone, Lemma 11 applies and we have d(R * ∆ , Bad) > 0. From Lemma 12, we obtain that there exists ∆ > 0 such that

Reach( A 0 ∆ ) ∩ Bad = ∅. If there exists ∆ > 0 such that Reach( A 0 ∆ ) ∩ Bad = ∅, then trivially R * ∆ ∩ Bad = ∅.
6 Algorithm for computing R * ∆ Algorithm 1: Algorithm from [START_REF] Puri | Dynamical properties of timed automata[END_REF] for computing R * (A) for a timed automaton A. Data : A timed automaton A = Loc, Var, q 0 , Lab, Edg Result : The set

J * = R * begin 1. Construct the region graph G = (R A , -→ A ) of A ; 2. Compute SCC(G) = strongly connected components of G; 3. J * ← [(q 0 )] ; 4. J * ← Reach(G, J * ) ; 5. if for some S ∈ SCC(G), S ⊆ J * and J * ∩ S = ∅ then J * := J * ∪ S ; Goto 4 ; end
In this section, we prove that the algorithm proposed in [START_REF] Puri | Dynamical properties of timed automata[END_REF] computes R * ∆ . This implies that R * = R * ∆ . The algorithm is shown as Algorithm 1.

Let us first examine how Algorithm 1 performs on the example of section 4. In the region graph of the timed automaton of Fig. 1, there is a cycle that runs from valuation v 0 to itself through v 1 to v 7 (see Fig. 2). Thus there is a cycle through the regions containing valuations v 0 to v 7 . Furthermore, these regions have an intersection with the set of reachable states in the classical semantics (in gray). Indeed since we consider closed regions, the intersection of two adjacent regions is not empty. Since those regions form a strongly connected component of the region graph and their intersection with the reachable states in the classical semantics is not empty, the algorithm adds all those regions to the set J * .

One can check that all regions of R * ∆ for the automaton A of figure 1 will be correctly added by Algorithm 1 (see figure 3).

In the rest of this section, we prove that this algorithm computes R * ∆ , by proving J * ⊆ R * ∆ on the one hand, and R * ∆ ⊆ J * on the other hand.

Limit cycles

This section studies the behavior of limit cycles. A limit cycle of a timed automaton A is a trajectory π = (q 0 , t 0 )(q 1 , t 1 ) . . . (q k , t k ) of A such that t k > t 0 and q k = q 0 . As suggested in [START_REF] Puri | Dynamical properties of timed automata[END_REF], given a progress cycle in the region graph and a region on this cycle, we focus on the subset of points of this region having a limit cycle. We first define this subset:

Definition 13 [See [Pur98, Section 7.1]] Consider a cyclic path p = p 0 p 1 . . . p N with p N = p 0 in the region graph of a timed automaton A. We define the return map R p : 2 p 0 → 2 p 0 by R p (S) = ∪ q∈S R p ({q}) for S ⊆ p 0 , and, for singletons, R p ({q 0 }) = q N there exists a trajectory π in A s.t. π = (q 0 , t 0 )(q 1 , t 1 ) . . . (q N , t N ) and ∀i. q i ∈ p i .

The set L i,p of points which can return back to themselves after i cycles through p, is defined as follows: L i,p = {q | q ∈ R i p (q)}. The set of points with limit cycles through p is L p = ∪ i∈N L i,p .

In the sequel, we write R or L instead of R p or L p when the path p is clear from the context. The interesting property of L p is that it is always reachable from any valuation in p: Theorem 14 ([Pur98, Lemma 7.10]) Let p = p 0 p 1 . . . p N be a cycle in G. Then for any z ∈ p 0 , there exists z , z ∈ L s.t. there exist trajectories in A from z to z and from z to z.

Soundness of Algorithm 1:

J * ⊆ R * ∆ Let r ∈ R ≥0 and x ∈ R n . The closed ball of radius r centered in x is the set B(x, r) = {x | d(x, x ) ≤ r}.
The following Lemma shows how a trajectory may be modified when enlarging guards in timed automata:

Lemma 15 Let A be a timed automaton with n clocks, ∆ ∈ Q >0 , and δ = ∆ n . Let p = p 0 p 1 p 2 . . . p N be a cycle in the region graph of A. Let u be a valuation in p 0 having a limit cycle, i.e. for which there exists a trajectory π[0, T ] in A 0 0 following p and with π(0) = π(T ) = u. Let v ∈ p 0 ∩ B(u, δ) be a neighbor valuation. Then there exists a trajectory from u to v in A 0 ∆ .

Intuitively, the result is proved by slightly anticipating or delaying the transition dates when a clock is reset.

Consider for instance the following path:

(x = a, y = b) τ 1 --→---→ x:=0 (x = 0, y = b + τ 1 ) τ 2 -→ (x = a , y = b ).
with a = τ 2 and b = b + τ 1 + τ 2 . By slightly modifying the continuous transition labels τ i , we get

(x = a, y = b) τ 1 -δ ---→---→ x:=0 (x = 0, y = b + τ 1 -δ) τ 2 +δ ---→ (x = a + δ, y = b ).
Thus the final value of clock y is identical in both cases, while the final value of x has been slightly modified. By carefully repeating this procedure, we can independently modify the final valuations of each clock. This corresponds to the idea behind Lemma 15.

Theorem 16 Let A be a timed automaton. Let p = p 0 p 1 . . . p N be a cyclic path in the region graph of A, and let x and y be two valuations in p 0 . For any ∆ ∈ Q >0 , there exists a trajectory from x to y in A 0 ∆ .

Proof. From Lemma 14, there exists u, v ∈ L s.t. x → u and v → y in A . Then u satisfies the conditions of Lemma 15, and thus any w ∈ L "close to" u is reachable from u in A 0 ∆ . Since L is convex, by recursively applying the previous argument, any w ∈ L is reachable from u in A 0 ∆ . In particular, v is reachable from u in A 0 ∆ , and y is reachable from x in A 0 ∆ .

As a consequence:

Theorem 17 The set J * computed by Algorithm 1 is a subset of R * ∆ , i.e. J * ⊆ R * ∆ .

Proof. Let ∆ > 0. If a set of regions J is a subset of Reach( A 0 ∆ ), then so is the set of reachable regions from J in the region graph G. Moreover, whenever a state of J appears in a cyclic region path p, then Theorem 16 ensures that any state in that region path is reachable in A 0 ∆ . Thus J ∪ p ⊆ Reach( A 0 ∆ ). Since J * is built by successively applying the above two operations, this ensures that J * ⊆ Reach( A 0 ∆ ). This holds for any ∆ > 0, thus J * ⊆ R * ∆ .

Completeness of Algorithm

1: R * ∆ ⊆ J *
To prove the completeness of Algorithm 1, we need to better understand the relationship between trajectories of A 0 ∆ and those of A . In particular, Theorem 18 states that any trajectory π of A 0 ∆ can be approached by a trajectory π of A , making the same discrete transitions and passing by the same regions.

Theorem 18 For any distance δ ∈ R >0 , for any number of steps k ∈ N, there exists ∆ ∈ Q >0 such that for any k-step trajectory π = (q 0 , t 0 ) . . . (q k , t k ) of A 0 ∆ , there exists a k-step trajectory π = (q 0 , t 0 ) . . . (q k , t k ) of A such that for any position i (0 ≤ i ≤ k) q i ∈ [q i ], that is the two trajectories cross the same regions, -and the distance between corresponding states q i and q i is bounded by δ, that is

q i = (l i , v i ), q i = (l i , v i ) where l i = l i and v i -v i ≤ δ.
Below, we give the general ideas underlying the proof. It uses the following lemma, stating that if v is reachable from u by letting time elapse, then any point The outline of the proof is as follows. We define a "simulation" relation R between valuations, which is a subset of R n × N × R n and we write R a (x , x) if (x , a, x) ∈ R. We show that

If      a ≤ k R a (x , x) x t -→ y σ -→ z in A 0 ∆ then ∃y, z :    x t - → y σ -→ z in A R a+1 (z , z) z -z ≤ y -y ≤ δ
The relation R a takes into account the current position in the trajectory: if x is the a th state in the trajectory, then x is in a neighborhood of size parameterized by a. This size increases with a, because the longer is the trajectory, the greater is the possible deviation (Fig. 4). This is not a classical simulation relation because it only works for a fixed trajectory length k (which is sufficient for proving Theorem 18).

Intuitively, R links a valuation x with a valuation x if whenever two clock have close fractional parts in x (for a special distance D), those clocks have identical fractional parts in x.

Fig. 5 illustrates the necessity of this choice: consider the trajectory (x , 0) (y , t )(z , t ) of A 0 ∆ . We must construct a trajectory (x, 0 taking the same discrete transition (labeled with σ). In the enlarged semantics, the guard on this transition is satisfied by y (i.e. y ∈ g ∆ ).

)(y, t)(z, t) of A R 0 R 1 R k • • • • • • t, σ t , σ R a (x , x) R a+1 (z , z) x z
The only possible choice for y is to both lie in the region [y ] and in g 0 as shown in the figure. This imposes the choice of x on the diagonal (i.e. with identical fractional parts for x i and x j ). -→ z enforces to take x with x i = x j . This is because x i and x j are too close.

R is formally defined in the complete proof, and it is shown that the ∆ can be chosen such that ∆ < δ 2 k (2+4n) .

The following theorem is a direct consequence of Theorem 18. It says that points in J * cannot reach points that are more than distance α away from J * in A 0 ∆ for sufficiently small ∆. Theorem 20 Suppose x ∈ J * and there exists a trajectory from x to y in A 0 ∆ with ∆ < α 2 W +1 (2+4n) where α < 1 2n , and W is the total number of regions. Then d(y, J * ) < α.

Finally, we can establish the completeness of Algorithm 1.

Theorem 21 The set J * computed by Algorithm 1 contains R * ∆ , i.e. R * ∆ ⊆ J * .

Proof. Since J * is a closed set containing the initial state, from Theorem 20, for any y ∈ Reach( A 0 ∆ ), d(y, J * ) ≤ α where α can be made arbitrarily small. It follows that R * ∆ ⊆ J * .

This concludes the proof that Algorithm 1 computes R * ∆ . According to [START_REF] Puri | Dynamical properties of timed automata[END_REF], we have the corollary that R * ∆ = R * = R * where R * = ∩ ∆∈Q >0 ∩ ∈Q >0 Reach( A ∆ ) so that the enlarged semantics R * ∆ is also robust against drifts in clocks.

Complexity

Complexity issues have been studied in [START_REF] Puri | Dynamical properties of timed automata[END_REF], so we recall the main result.

Theorem 22 ([Pur98]) Given a timed automaton A = Loc, Var, q 0 , Lab, Edg and a location l f ∈ Loc, determining whether a state (l f , v) ∈ R * ∆ for some valuation v is PSPACE-Complete.

Conclusion

In this paper, we have shown that a notion of robustness defined by Puri [START_REF] Puri | Dynamical properties of timed automata[END_REF] is closely related to a notion of implementability that we recently introduced in [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF]. Making this link formal allowed us to show that our notion of implementability is decidable for the class of timed automata. To establish this link, we have proved that the algorithm proposed by Puri computes the set of reachable states of timed automata where guards are enlarged by an infinitesimally small rational value. The existence of such a value implies the implementability as shown in our previous paper. The proofs of the decidability result rely on non trivial adaptations of the main ideas underlying the study of drift in the rate of clocks made by Puri. The algorithm that is used to check implementability manipulates strongly connected components of the region graph. It can be seen as defining exact accelerations of cycles of the timed automaton.

We will work in the future on making those accelerations practical and as a consequence, we will work on to turn the theoretical algorithm proposed in this paper into a practical one. If we succeed in this task, the results of this paper and of our previous paper [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF] will allow us to propose a practical procedure to produce provably correct code from proved correct controller modeled as timed automata.

  4. The transition relation → is defined by (a) For the discrete transitions: ((l, v), σ, (l , v )) ∈ → iff there exists an edge (l, l , g, σ, R) ∈ Edg such that v ∈ g ∆ and v = v[R := 0]. (b) For the continuous transitions: (

Fig. 3 .

 3 Fig. 3. The set R * ∆ for the timed automaton A of Fig. 1.

  x ∈ [u] in the neighborhood of u can reach some point y ∈ [v] in the neighborhood of v. More precisely: Lemma 19 Suppose r → G r in the region graph G of a timed automaton, and u τ -→ v with u ∈ r, v ∈ r and τ ∈ R ≥0 . Then for any x ∈ B(u, R) ∩ r, there exists y ∈ B(v, 2R) ∩ r such that x τ -→ y for some τ with |ττ | ≤ R. Proof (Sketch) of theorem 18.

Fig. 4 .

 4 Fig. 4. Simulation of the trajectory π of A 0 ∆ .

  Fig. 5. Simulating x t -→ y σ

Our notion of robustness is different from another interseting one introduced in [GHJ97].

In the sequel, the guards are enlarged by strictly positive parameter ∆, and so it is natural to consider them closed.

Supported by the FRFC project "Centre Fédéré en Vérification" funded by the Belgian National Science Foundation (FNRS) under grant nr 2.4530.02 Research fellow supported by the Belgian National Science Foundation (FNRS)


J M Davoren
email: davoren@unimelb.edu.au

V Coulthard

N Markey
email: markey@lsv.ens-cachan.fr

T Moor

B Humberstone

L Humberstone

G Restall

Non-deterministic temporal logics for general flow systems ⋆

In this paper, we use the constructs of branching temporal logic to formalize reasoning about a class of general flow systems, including discretetime transition systems, continuous-time differential inclusions, and hybrid-time systems such as hybrid automata. We introduce Full General Flow Logic, GFL ⋆ , which has essentially the same syntax as the well-known Full Computation Tree Logic, CTL ⋆ , but generalizes the semantics to general flow systems over arbitrary time-lines. We propose an axiomatic proof system for GFL ⋆ and establish its soundness w.r.t. the general flow semantics.

Introduction

Recent work in set-valued dynamical systems [START_REF] Aubin | Viability kernels and capture basins: Lecture notes[END_REF][START_REF] Aubin | Dynamical qualitative analysis of evolutionary systems[END_REF], investigates a general class known as evolutionary systems. These are described by a set-valued map S which maps each state x ∈ X to the set S(x) of all possible future evolutions γ from initial state x, where γ : [0, ∞) → X, γ(0) = x. These systems are non-deterministic: from an initial state, there may be none, exactly one, or many possible futures. The defining condition of these systems is that the family of sets S(x) must be closed under the operations of taking a suffix of an evolution, and of taking the fusion of the two evolutions at a common state. It includes as examples the solution maps over real time of differential equations with inputs, and of differential inclusions and their impulse/hybrid extensions [START_REF] Aubin | Viability kernels and capture basins: Lecture notes[END_REF][START_REF] Aubin | Impulse differential inclusions: A viability approach to hybrid systems[END_REF]. In the discrete time case, these same closure properties come up in the study of sets computation sequences, in automata theory and the semantics of branching temporal logics such as CTL ⋆ [START_REF] Alur | Automatic symbolic verification of embedded systems[END_REF][START_REF] Stirling | Modal and temporal logics[END_REF][START_REF] Reynolds | An Axiomatization of Full Computation Tree Logic[END_REF]. The same closure properties appear again in Willems' Behavioural Systems theory [START_REF] Willems | Paradigms and puzzles in the theory of dynamical systems[END_REF], under the names time invariance and axiom of state, with the time domain the reals or the integers. In the analysis of evolutionary systems, there is particular interest in the area of Viability Theory [START_REF] Aubin | Impulse differential inclusions: A viability approach to hybrid systems[END_REF][START_REF] Aubin | Viability kernels and capture basins: Lecture notes[END_REF], where a central concept is that of an evolution being "viable in K until capturing target C", which means that the path starts at a state in K, and either remains in K for all time, or it reaches C in finite time, and remains within K until it does so. From a computer science perspective, this concept corresponds to the Until construct on paths in temporal logic.

The purpose of this paper is to generalize the class of evolutionary systems to give an adequate semantics for non-deterministic temporal logic that is uniform for discretetime transition systems, continuous-time differential inclusions, and hybrid systems, where the time domains of evolutions lie in the lexicographically ordered L = N × R +

• . There are three novelties in our work. First, we take a minimalist approach to the notion of a time-line: for the suffix and fusion-closure properties, the minimal structure needed on a linear order are translation or shift maps, which is weaker than a semi-group. Second, we don't take as primitive objects evolutions or paths defined on the entire time line; that perspective gives something of a "god's eye" view of the system, looking forward from now to eternity. Instead, our basic object of a path describes a boundedtime segment of a possible evolution of or signal within a system; it starts somewhere, at relative time 0 with some value x ∈ X, and then progresses with an ordering given by the underlying time-line L to end somewhere, at some time-point τ 0, with a value x ′ ∈ X. We then build up a theory of infinitary extensions with unbounded time domains. Third, we don't restrict to paths γ : T → X with bounded interval time domains T = [0, τ ] ⊆ L, but rather allow "gaps" in T . Over L = N × R +

• , finite hybrid trajectories are functions taking values in some X, with time domains

T ⊆ L of the form T = i<N [ (i, 0), (i, ∆ i ) ], with ∆ i ∈ R +
• the duration of the i-th interval. Within T , time (i + 1, 0) is the immediate discrete successor of time (i, ∆ i ), but in the underlying line L, there is a continuum-length open interval "gap" in between.

The body of the paper is as follows. Section 2 covers preliminaries on set-valued maps and linear orders, and develops some basic theory of paths with "gappy" time domains. We introduce general flow systems in Section 3, and give examples in discrete, continuous and hybrid time. In Section 4, we give an infinitary completion construction, and relate our model class to evolutionary systems and behavioural systems. Section 5 introduces Full General Flow Logic, GFL ⋆ , with basically the same syntax as the wellknown Full Computation Tree Logic, CTL ⋆ , developed for discrete-time models, but semantics w.r.t. general flow systems over arbitrary time. In Section 6, we propose an axiomatic proof system for GFL ⋆ and sketch soundness w.r.t. general flow semantics.

Preliminaries: set-valued maps, time-lines and paths

When we write Y ⊂ X for sets X, Y , we will mean Y is a proper subset of X, and so

Y ⊆ X iff Y ⊂ X or Y = X. We write r : X ; Y to mean r : X → 2 Y is a set-valued map, with set-values r(x) ⊆ Y for every x ∈ X (possibly r(x) = ∅); equivalently, r ⊆ X × Y is a relation. Let [ X ; Y ] := 2 X×Y
denote the set of all maps, partially ordered by ⊆, so r ⊆ r ′ iff r(x) ⊆ r ′ (x) for all x ∈ X, with least element the empty map ∅. Every map r : X ; Y has a converse r -1 : Y ; X given by x ∈ r -1 (y) iff y ∈ r(x). The domain of a set-valued map is dom(r) := {x ∈ X | r(x) = ∅}, and the range is ran(r) := dom(r -1 ) ⊆ Y . A map r : X ; Y is total on X if dom(r) = X. We distinguish several sub-classes of maps. We write r : X → Y to mean r is a (total) function, with values written r(x) = y. We also distinguish partial functions, and write r : X Y to mean that r is single-valued on its domain dom(r) ⊆ X, and write r(x) = y when x ∈ dom(r), and r(x) = UNDEF when x / ∈ dom(r). Let (L, <, 0) be a linear order with least element 0 and no largest element, and the reflexive closure of <.

exists an l ∈ L such that a < l < b. A linear order L is called discrete if succ L is a total function (dom(succ L ) = L), and is dense if succ L if dom(succ L ) = ∅.
Given two linear orders (L, <) and (L ′ , < ′ ), a function g : L → L ′ is called: strictly orderpreserving if (∀l, k ∈ L), l < k implies g(l) < ′ g(k); and an order isomorphism if it bijective and both g and g -1 are strictly order-preserving. Definition 1. Let (L, <, 0) be a linear order with least element 0 and no largest element. We call L a (future) time line if L is shift invariant, in the sense that if for each a ∈ L, there exists an order isomorphism σ -a : [a, ∞) → L, with inverse σ +a := (σ -a ) -1 : L → [a, ∞), and σ -0 = id L . We call the functions σ -a left ashift maps, and the inverses σ +a right a-shift maps.

The discrete time line N, and the dense continuum time line R +

• := [0, ∞), are considered with their usual orderings. The hybrid time space N × R +

• is linearly ordered lexicographically: i.e. (i, t) < lex (j, s) iff i < j or i = j and t < s. The least element is 0 := (0, 0). This ordering does not admit any natural addition operation to make it a linearly ordered semi-group, but its shift invariance is witnessed by the following order isomorphisms: for each a = (k, r) ∈ L, define σ -a : [a, ∞) → L by σ -a (i, t)

:= (0, t -r) if i = k and σ -a (i, t) := (i -k, t) if i > k, for l = (i, t) ∈ [a, ∞). Then σ +a : L → [a, ∞) satisfies σ +a (i, t) = (k, t + r) if i = 0 and σ +a (i, t) = (i + k, t) if i > 0. The full hybrid time line N × R +
• is everywhere dense. In the "gappy" time domains T ⊂ L considered below, the partial function succ T may be defined at some time points in T and not at others, so T is a "hybrid" of discrete and dense. X | dom(γ) ∈ BT(L) }, and define IPath(L, X) to be the subset interval paths with dom(γ) ∈ BI(L). For γ ∈ Path(L, X), define b γ := b dom(γ) to be the largest element in dom(γ), so that γ(0) ∈ X is the start-value of γ and γ(b γ ) ∈ X is the end-value of γ. Proposition 1. For L any time line, the set BT(L) is closed under the following operations: for T, T ′ ∈ BT(L) and t ∈ L,

• intersection: T ∩ T ′ ∈ BT(L); in particular, [0, t] ∩ T ∈ BT(L) if t ∈ T ; • left t-shift: σ -t ([t, b T ] ∩ T ) ∈ BT(L) if t ∈ T ; • union with right t-shift: T ∪ σ +t (T ) ∈ BT(L) if t b T .
The subset BI(L) of bounded initial closed intervals is closed under the first two operations, and is also closed under union with right shift restricted to t = b T .

For X any value space, the following operations are well-defined in Path(L, X):

for γ, γ ′ ∈ Path(L, X) and t ∈ dom(γ), • t-end prefix: γ| t ∈ Path(L, X), where γ| t := γ ↾ [0,t]∩ dom(γ) • t-start suffix: t |γ ∈ Path(L, X), where ( t |γ)(l) := γ(σ +t (l)) for all l ∈ dom( t |γ) := σ -t ([t, b γ ] ∩ dom(γ)) • fusion: γ * γ ′ ∈ Path(L, X), provided that γ ′ (0) = γ(b γ ) , where (γ * γ ′ )(l) := γ(l) for l ∈ dom(γ) and (γ * γ ′ )(l) := γ ′ (σ -b γ (l)) for l ∈ σ +b γ (dom(γ ′ )).
For each value x ∈ X, define the trivial path θ x : [0, 0] → X by θ x (0) = x. In Path(L, X), the trivial path θ x functions as a point-wise identity with respect to fusion:

θ x * γ = γ iff γ starts at value x = γ(0), and γ * θ x = γ iff γ ends at value x = γ(b γ ).
Definition 3. Let (L, <, 0) be a time line and X a value space. Define a partial order on Path(L, X) from the underlying linear order on L (re-using notation) by: γ

< γ ′ iff γ ⊂ γ ′ and t < t ′ for all t ∈ dom(γ) and t ′ ∈ dom(γ ′ ) -dom(γ). If γ < γ ′ , we say the path γ ′ is a (proper) extension of γ, or γ is a proper prefix of γ ′ .
In general, the path extension ordering < is a proper subordering of the subset relation, but when restricted to the set IPath(L, X), it collapses to the subset relation. The following proposition characterizes the path extension partial order in terms of the fusion operation. Proposition 2. For L a time line, X a value space, and for all γ, γ ′ ∈ Path(L, X), γ < γ ′ iff γ ′ = γ * γ ′′ for some γ ′′ ∈ Path(L, X) with γ ′′ = θ x and γ ′′ (0) = γ(b γ ).

We now return to the hybrid time line L = N × R +

• for a more detailed discussion of some of its paths. Define DS := IPath(N, R +

• ) to be the set of all (finite) duration sequences; i.e. ∆ ∈ DS is a finite sequence of values ∆ i := ∆(i) ∈ R +

• for i < N for N = length(∆) ∈ N. For duration sequences ∆ ∈ DS, define HT (∆) to be the hybrid time domain determined by ∆:

HT (∆) := i<length(∆) [ (i, 0), (i, ∆ i ) ] HT := { HT (∆) ∈ BT(L) | ∆ ∈ DS } HPath(X) := { γ ∈ Path(N × R + • , X) | dom(γ) ∈ HT } (1)
For hybrid paths γ ∈ HPath(X), define the duration sequence of γ by ds(γ) = ∆ iff dom(γ) = HT (∆) for ∆ ∈ DS, and define the discrete length of γ by dl(γ) := length(ds(γ)) ∈ N. Also define the total duration of γ by td(γ) := i<dl(γ) ∆ i .

Proposition 3. For all γ, γ ′ ∈ HPath(X),

γ lex γ ′ iff dl(γ) dl(γ ′ ) and (∀i < N := dl(γ) -1 ) γ i = γ ′ i and γ N γ ′ N
With hybrid paths, we have to deal with the product structure on the time line. We also encounter product structure on the value space. Let π X : (X × Y ) → X and π Y : (X × Y ) → Y be the standard coordinate projection functions on a product of sets X ×Y . These can be lifted to give projection functions on paths π X : Path(L, X ×Y ) → Path(L, X) and to projections on functions π

X : [ L → (X × Y ) ] → [ L → X ], by defining (π X ζ)(t) := π X (ζ(t)) for t ∈ dom(ζ) and ζ ∈ Path(L, X × Y ) or ζ : L → (X × Y );
and symmetrically for π Y in the other coordinate.

General flow systems

The general dynamical system model we develop here is essentially Aubin's model of an evolutionary system, generalized to arbitrary time lines L, and "deconstructed", so that the basic objects are bounded length paths, having dom(γ) ⊆ [0, b γ ]. Definition 4. Let (L, <, 0) be a time line, and let X = ∅ be an arbitrary value space. A general flow system over X with time line L is a map Φ : X ; Path(L, X) satisfying, for all x ∈ dom(Φ), for all γ ∈ Φ(x), and for all t ∈ dom(γ):

(GF0) initialization: γ(0) = x (GF1) suffix-closure: t |γ ∈ Φ(γ(t)) (GF2) fusion-closure: γ| t * γ ′ ∈ Φ(x) for all γ ′ ∈ Φ(γ(t)) • Φ has interval paths if ran(Φ) ⊆ IPath(L, X); • Φ has hybrid paths if ran(Φ) ⊆ HPath(X) and L = N × R + • ; • Φ is reflexive if θ x ∈ Φ(x) for all x ∈ dom(Φ); • Φ is blocked at x if Φ(x) = {θ x } ,
and non-blocking if not blocked at any x ∈ X; • Φ is prefix-closed if γ| t ∈ Φ(x) for all x ∈ dom(Φ), γ ∈ Φ(x) and t ∈ dom(γ); • Φ is deterministic if for all x ∈ dom(Φ), the set Φ(x) is linearly ordered by <.

In terms of Behavioural Systems theory [START_REF] Willems | Paradigms and puzzles in the theory of dynamical systems[END_REF], the suffix-closure condition (GF1) corresponds to the time invariance property, while the fusion-closure condition (GF2) corresponds to the so-called "axiom of state" principle, that "the state should contain sufficient information about the past so as to determine the future behaviour", because the various possible extensions of a trajectory at time t are exactly those which would have been possible if we had observed only the state at time t, and not the past of the trajectory prior to that point. Proposition 4. Let (L, <, 0) be a time line, let X = ∅ be a value space, and let Φ : X ; Path(L, X) be a general flow system over X with respect to L. Then:

(1.) The set dom(Φ) ⊆ X is closed under reachability by Φ-paths: if x ∈ dom(Φ) and γ ∈ Φ(x), and t ∈ dom(γ), then γ(t) ∈ dom(Φ). (2.) Φ is reflexive iff Φ is prefix-closed. (3.) Φ is non-blocking iff for all x ∈ dom(Φ), γ ∈ Φ(x), there is a γ ′ ∈ Φ(x) : γ < γ ′ . Example 1. If g : L 1 → L 2 is
an order embedding, and Φ : X ; Path(L 1 , X) is a general flow system, then the map Φ g : X ; Path(L 2 , X) is also a general flow, where for x ∈ dom(Φ g ) := dom(Φ), define

Φ g (x) := {η ∈ Path(L 2 , X) | ∃γ ∈ Φ(x) : dom(η) = g(dom(γ)) ∧ (∀t ∈ dom(η) ) η(t) = γ(g -1 (t)) .
Example 2. A (basic) state transition system is a structure (X, R) where X = ∅ is the state space, and R : X ; X is any set-valued map (the one-step transition relation). The map R determines a general flow system with interval paths over time-line

L = N: Φ R (x) := {γ ∈ IPath(N, X) | γ(0) = x ∧ (∀i < b γ -1 ) γ(i + 1) ∈ R(γ(i)) }. It is easily verified that Φ R (x) = {θ x } iff x / ∈ dom(R).
Hence Φ R is non-blocking iff the map R is total on X, and Φ R is deterministic iff the map R is a partial function.

Example 3. A differential inclusion is a structure (X, F ) where X ⊆ R n is a finite dimensional vector space with the Euclidean norm, and

F : X ; R n is a set-valued map. Define AC(X) := {γ ∈ IPath(R + • , X) | γ absolutely continuous on [0, b γ ] }.
Solutions to the inclusion ẋ(t) ∈ F (x(t)) starting at a state x are defined by:

Sol F (x) := γ ∈ AC(X) | γ(0) = x ∧ d dt γ (l) ∈ F (γ(l)) a.e. for l ∈ [0, b γ ] .
It is immediate that Sol F is reflexive and is suffix-closed and fusion, hence is a general flow system with interval paths over L = R +

• . For the non-blocking property, to ensure the existence of non-trivial solutions from each x ∈ cl(dom(F )), one needs to impose some regularity assumptions (e.g. Lipschitz or Marchaud conditions) on the map F [START_REF] Aubin | Impulse differential inclusions: A viability approach to hybrid systems[END_REF][START_REF] Aubin | Viability kernels and capture basins of sets under differential inclusions[END_REF][START_REF] Aubin | Set-Valued Analysis[END_REF]. If F : X → R n is actually a function and the differential equation

ẋ(t) = F (x(t)) has a unique maximal solution η : [0, c x ) → X starting from each x ∈ X, with c x ∈ R + • ∪ {∞}, then Sol F (x) = { η| t | t ∈ [0, c x ) } is linearly ordered, hence deter- ministic at every x ∈ X. Example 4. A hybrid automaton [15, 2, 14, 1] is a structure H = ( Q, E, X, F, D, R ): • Q is a finite set of control modes; • E : Q ; Q is the discrete transition relation; • X ⊆ R n is the continuous state space; • F : Q → [ X ; R n ]
maps each q ∈ Q to a set-valued vector field F (q) : X ; R n with differential inclusion solution map Sol q := Sol F (q) : X ; IPath(R + • , X); • D : Q ; X maps each q ∈ Q to a set D q := D(q) ⊆ X, the domain of mode q; • R : E → [ X ; X ] maps (q, q ′ ) ∈ E to a reset map R q,q ′ := R(q, q ′ ) : X ; X. Define a map Traj H : (Q × X) ; HPath(Q × X) by:

Traj H (q, x) := { γ ∈ HPath(Q × X) | (0) γ(0, 0) = (q, x) ∧ (∀i < dl(γ) ) for ∆ i := ds(γ)(i) ∧ q i := π Q γ i (0) (1) π X γ i ∈ Sol q i (π X γ i (0)) ∧ ran(γ i ) ⊆ {q i } × D q i ∧ (2) (q i , q i+1 ) ∈ E ∧ π X γ i+1 (0) ∈ R q i , q i+1 π X γ i (∆ i ) if i < dl(γ) -1
Paths in Traj H are called (finite) trajectories of H. Direct from the definition, we can see that dom(Traj

H ) = D = {(q, x) ∈ Q × X | x ∈ D q }.
We will say a hybrid automaton H is well-constituted if all of the following hold:

(A) Q = ∅, and E : Q ; Q is total; (B) X ⊆ R n
is a non-empty finite dimensional vector space with the Euclidean norm;

(C) D : Q ; X is total, so D q = ∅ for each q ∈ Q; (D) for each q ∈ Q, domain D q ⊂ dom(Sol q ) and Sol q is not blocked at any x ∈ D q ; (E) for each transition pair (q, q ′ ) ∈ E, the reset relation R q,q ′ : X ; X satisfies the constraints dom(R q,q ′ ) = ∅ and dom(R q,q ′ ) ⊆ D q and ran(R q,q ′ ) ⊆ D q ′ . Any assumptions will do on the set-valued vector fields F (q) : X ; R n , provided they give non-trivial solution paths in Sol q on the mode domains D q . Proposition 5. Let H = ( Q, E, X, F, D, R ) be a hybrid automaton. Then the trajectory map

Traj H : (Q × X) ; HPath(Q × X) is a general flow system over Q × X with time line N × R + • . If H is well-constituted then Traj H is also prefix-closed.
The conditions on H being well-constituted rule out all "trivial" ways that Traj H may become blocked: Sol q is not blocked at any x ∈ D q ⊆ dom(Sol q ); since E is total, every q ∈ Q has a discrete successor; and for each discrete transition (q, q ′ ) ∈ E, the transition guard set dom(R q,q ′ ) is non-empty and contained in D q , and under the reset relation, the image set ran(R q,q ′ ) lies in D q ′ . So in attending to the possibility of blocking, we need to focus only on states x ∈ D q that are not in any transition guard set, so no discrete transition is possible from (q, x), and states x ∈ D q from which every non-trivial q-solution leaves D q "immediately after now", so there are no hybrid trajectories from (q, x) with non-trivial continuous evolution in mode q.

Proposition 6. If a hybrid automaton H is well-constituted, and

Out q := x ∈ D q | (∀γ ∈ Sol q (x))(∀t ∈ dom(γ), t > 0 )(∃s < t) γ(s) / ∈ D q Grd q := q ′ ∈E(q) dom(R q,q ′ )
then Traj H is non-blocking on its domain D iff Out q ⊆ Grd q for each q ∈ Q.

The sets Out q and the condition Out q ⊆ Grd q are identified in [START_REF] Lygeros | Dynamical properties of hybrid automata[END_REF], for systems with deterministic continuous dynamics. In virtue of the continuity of paths in Sol q (x), the set Out q is contained in the topological boundary: Out q ⊆ bd(D q ) := cl(D q )int(D q ). An immediate corollary is that for well-constituted systems H, Traj H will be non-blocking on D if for all q ∈ Q, either (bd(D q ) ∩ D q ) ⊆ Grd q , or D q is open.

We can also show the impulse differential inclusion model of hybrid systems from [START_REF] Aubin | Impulse differential inclusions: A viability approach to hybrid systems[END_REF] to be an example of a general flow system over the hybrid time line; this example and others will be discussed in a separate paper.

Infinitary extensions of general flow systems

From Proposition 4, we know that if a general flow Φ is non-blocking, then for each x ∈ dom(Φ) and γ ∈ Φ(x), there exists an infinite sequence of paths {γ n } with γ 0 = γ and γ n ∈ Φ(x) and γ n < γ n+1 for all n. Motivated by this fact, we view "maximal extensions" or "completions" of paths as infinitary objects, arising as limits of infinite ordered sequences of finitary bounded paths. In this paper, we take limits over ordered sequences of order type (ordinal) ω, the order type of N, but we want to leave open the possibility, for later work, of dealing with sequences of transfinite length, with ordinals greater than ω (for formalizing the notion of a continuation of a Zeno hybrid trajectory that has discrete stages ω, ω + 1, ω + 2, . . . up to some limit ordinal ν > ω). We need access to maximal length paths in order to formalize the Until construct in temporal logic, but we also want to "go to infinity" in order to be able to directly compare our class of dynamical systems with those developed in terms of functions over the whole time line L = N or L = R +

• ; in particular, Aubin's model of an evolutionary system [START_REF] Aubin | Dynamical qualitative analysis of evolutionary systems[END_REF][START_REF] Aubin | Viability kernels and capture basins: Lecture notes[END_REF], and also Willem's behavioural systems model [START_REF] Willems | Paradigms and puzzles in the theory of dynamical systems[END_REF]. Definition 5. For any path set P ⊆ Path(L, X), define the ω-extension of P by:

Ext ω (P) := { η : L X | (∃ γ : ω → Path(L, X) ) (∀k < ω) [ γ k := γ(k) ∧ γ k ∈ P ∧ γ k < γ k+1 ∧ η = k<ω γ k Define EPath ω (L, X) := Ext ω ( Path(L, X) ); EIPath ω (L, X) := Ext ω ( IPath(L, X) ).
Paths η ∈ Ext ω (P) will be called ω-paths of P.

Thus the ω-extension Ext ω (P) contains all the partial functions η : L X that can arise as the union or limit of an ω-length strictly extending sequence of paths in the set P. The path extension ordering < on bounded paths induced by the linear order on L can be lifted to ω-paths. For paths η, η ′ ∈ Path(L, X) ∪ EPath ω (L, X), we extend Definition 3 to define η < η ′ if η ⊂ η ′ and t < t ′ for all t ∈ dom(η) and t ′ ∈ dom(η ′ )dom(η). If η < η ′ then dom(η) must be a bounded subset of L.

For a general flow system, we want to pick out the ω-paths η ∈ Ext ω (Φ(x)) that are maximal in the sense that there are no real paths of the system in Φ(x) extending η. Definition 6. Given a general flow system Φ : X ; Path(L, X), define the maximized ω-extension of Φ to be the set-valued map E ω Φ : X ; EPath ω (L, X) given by:

(E ω Φ)(x) := { η ∈ Ext ω (Φ(x)) | (∀γ ∈ Φ(x) ) η ≮ γ }
A system Φ will be called ω-extendible if for every x ∈ dom(Φ) and every γ ∈ Φ(x), there exists η ∈ (E ω Φ)(x) such that γ < η.

In general, dom(E ω Φ) ⊆ dom(Φ); Φ is ω-extendible iff dom(E ω Φ) = dom(Φ). In reasoning about the behaviour of an ω-extendible system Φ, we can safely replace quantification over all possible paths in Φ(x), with quantification over (E ω Φ)(x), the maximal ω-paths; this is crucial for the semantics of the temporal Until construct.

Proposition 7. For any general flow

Φ : X ; Path(L, X), (1.) Φ is ω-extendible iff Φ is non-blocking. (2.) If Φ non-blocking, then Φ is deterministic iff E ω Φ is a partial function.
The non-trivial direction is: Φ is non-blocking implies Φ is ω-extendible; the proof uses Zorn's Lemma to obtain a maximum of any strictly extending sequence of ω-paths.

We are now in a position to formalize the relationship between Aubin's model of an evolutionary system [START_REF] Aubin | Dynamical qualitative analysis of evolutionary systems[END_REF][START_REF] Aubin | Viability kernels and capture basins: Lecture notes[END_REF], and the general flow systems defined here. An evolutionary system, over time lines L = R +

• or L = N, is a map Ψ : X ; [ L → X ] such that, for whole line paths η : L → X, η(0) = x for all η ∈ Ψ (x) and Ψ is closed under the suffix and fusion operations (the natural extensions to unbounded paths of the operations in Proposition 1), in the same sense as which general flow systems with bounded paths are closed under these operations, as required by clauses (GF1) and (GF2) of Definition 4.

Proposition 8. Let the time line be either

L = N or L = R +
• , and X = ∅. Ψ : X ; [ L → X ] is an evolutionary system in the sense of Aubin iff there exists an interval path general flow system Φ : X ; IPath(L, X) that is non-blocking and satisfies Ψ = E ω Φ.

Thus evolutionary systems are a subclass of non-blocking general flow systems. In Willem's Behavioural Systems model [START_REF] Willems | Paradigms and puzzles in the theory of dynamical systems[END_REF], with time lines

L = N or L = R + • , a behaviour is a set of functions B ⊆ [ L → X ].
It can also be established that B is a time-invariant and complete state behaviour iff there exists an interval path, nonblocking general flow system Φ : X ; IPath(L, X) such that B = ran(E ω Φ).

When L = N, then all ω-paths η ∈ EPath ω (N, X) have infinite time domain, so we will always have (E ω Φ)(x) = Ext ω (Φ(x)) for any non-blocking general flow Φ.

When L = R + • , we know that every ω-path η ∈ EIPath ω (R + • , X) must have dom(η) = [0, c) for some c ∈ R + • ∪ {∞}. For a non-blocking flow Φ, suppose η ∈ Ext ω (Φ(x)) is any ω-path. Then c = ∞ automatically gives η ∈ (E ω Φ)(x). If c < ∞,
then we will have a maximally extended ω-path η ∈ (E ω Φ)(x) exactly when η| t ∈ Φ(x) for all t ∈ [0, c) but the limit as t → c of η(t) does not exist, or does exist but is not in dom(Φ); i.e. η has finite escape time. The analysis for the ω-extensions of general bounded paths η ∈ EPath ω (R +

• , X) is similar. For the differential inclusion systems in Example 3, the Marchaud conditions on F in [START_REF] Aubin | Viability kernels and capture basins of sets under differential inclusions[END_REF][START_REF] Aubin | Impulse differential inclusions: A viability approach to hybrid systems[END_REF] constitute a property stronger than non-blocking: they imply that dom(η) = [0, ∞) for all η ∈ (E ω Sol F )(x), so there are no ω-paths with finite escape time.

When L = N×R + • is the hybrid time line, we can characterize the maximal ω-paths of a non-blocking system as follows.

Proposition 9. For any X = ∅ and non-blocking general flow Φ : X ; HPath(X), every ω-path η ∈ (E ω Φ)(x) is of one of two forms: (i) η = γ * υ where γ ∈ Φ(x) and υ : {0} × [0, c) → X with c ∈ R +

• ∪ {∞} and υ = n<ω γ n and each γ n ∈ Φ(υ(0, 0)) has dl(γ n ) = 1, hence η has finite discrete length dl(η) = dl(γ) ∈ N, and total duration td(η) = td(γ) + c, which may be finite or infinite, depending on c; or (ii) η = n<ω γ n where dl(γ n ) < dl(γ n+1 ), hence η has infinite discrete length, and total duration td(η) = n<ω td(γ n ), which may be finite or infinite;

The non-blocking/ω-extendibility property here allows for two cases among extensions of hybrid paths that are typically considered "pathological": Zeno extended hybrid paths η ∈ (E ω Φ)(x) that have infinite discrete length but finite total duration td(η) < ∞; and livelocked extended hybrid paths η ∈ (E ω Φ)(x) that have finite discrete length dl(η) = k + 1 and finite total duration. Livelocked η are maximal with the last path segment having dom(η k ) = [0, c); this Φ path would "die" at klocal time t = c (hybrid time (k, c)) if it ever got there, but it never can, as for every extension of η k to domain [0, c], the resulting hybrid path is not in Φ(x). For a nonblocking hybrid automaton H, the general flow Traj H will exhibit livelock on an extended trajectory η ∈ (E ω Traj H )(x) with dl(η) = k + 1 iff the last path segment η k : [0, c) → (Q × X) is such that, for q k := π Q η k (0) and x k := π X η k (0), there exists a solution path γ ∈ Sol q k (x k ) such that dom(γ) = [0, b γ ], with b γ > c and γ ↾ [0,c) = π X η k , that eventually leaves the mode domain D q , but never passes through Grd q on the way: γ(c) / ∈ D q and γ(t) ∈ D q -Grd q for all t ∈ [0, c).

5 Full General Flow Logic GFL ⋆ : syntax and semantics

We now turn to the syntax and semantics of a logic we call Full General Flow Logic, GFL ⋆ , which generalizes to general flow models the semantics of Full Computation Tree Logic, CTL ⋆ , introduced by Emerson and Halpern in 1983 [START_REF] Emerson | Sometimes" and "Not Never" revisited: on branching versus linear time[END_REF] for formalizing reasoning about executions of concurrent programs in discrete time. The syntax here is a labelled variant of that of CTL ⋆ , allowing for semantic models consisting of a finite family of non-blocking general flow systems.

Definition 7.

A signature is a pair Σ = (Sys, Prp), where Sys is a finite set of system labels, and Prp is a countable set of atomic propositions. The temporal logic language L(Σ) consists of the set of all formulae ϕ generated by the grammar:

ϕ ::= p | ¬ ϕ | ϕ 1 ∨ ϕ 2 | ϕ 1 U a ϕ 2 | ∀ a ϕ
for atomic propositions p ∈ Prp, and system labels a ∈ Sys.

The other propositional (Boolean) connectives and logical constants true, ⊤, and false, ⊥, are defined in a standard way, and the path quantifiers ∀ a have classical negation duals ∃ a , as follows:

ϕ 1 ∧ ϕ 2 def = ¬ (¬ ϕ 1 ∨ ¬ϕ 2 ) ϕ 1 → ϕ 2 def = ¬ ϕ 1 ∨ ϕ 2 ϕ 1 ↔ ϕ 2 def = (ϕ 1 → ϕ 2 ) ∧ (ϕ 2 → ϕ 1 ) ∃ a ϕ def = ¬ ∀ a ¬ ϕ ⊤ def = p ∨ ¬ p for any p ∈ Prp ⊥ def = ¬⊤ (2)
The temporal operators, U a , for a ∈ Sys, refer to the ω-path space of a non-blocking general flow system Φ a . The formula ϕ U a ψ, read "ϕ until ψ, for a-type paths", will hold along any ω-path η of type a if at some time in the future (along η) the formula ψ holds, and at all intermediate times (along η) between now and then, ϕ holds. The universal quantifier ∀ a applied to a path formula produces a state formula, and ∀ a (ϕ U a ψ) holds at a state x if every ω-path η ∈ (E ω Φ a )(x) satisfies the path formula ϕ U a ψ. Dually, ∃ a (ϕ U a ψ) holds at a state x if there exists an ω-path η ∈ (E ω Φ a )(x) which satisfies the path formula ϕ U a ψ. The until construct on paths can be formulated in several distinct ways; we shall take as primitive the strictest version of until, and then define weaker variants in terms of it. In particular, an important difference between the logic here, and the usual presentation of CTL ⋆ developed for discrete time paths, is that instead of taking the next-time discrete successor operator as a syntactic and semantic primitive, we use a known method to define next-time in terms of the strictest until [START_REF] Burgess | Axioms for tense logic I: "Since" and "Until[END_REF][START_REF] Gabbay | Temporal Logic: Mathematical Foundations and Computational Aspects[END_REF]. Our semantics covers arbitrary time lines, so in general the immediate successor map is only a partial function on the domain of a path, and in the case of interval paths in a dense time line, may be everywhere undefined.

Definition 8.

A general flow logic model (logic model, for short) of signature Σ = (Sys, Prp) is a structure M = (X, L, S, P), where:

• X = ∅ is the state space, of arbitrary cardinality;

• L is a function mapping each symbol a ∈ Sys to a time line L a := L(a);

• S is a function mapping each symbol a ∈ Sys to an non-blocking general flow system Φ a := S(a) : X ; Path(L a , X) over the space X, with time line L a ; • P : Prp ; X maps each p ∈ Prp to a set P(p) ⊆ X of states. The ω-path space of a model M is defined by EPath(M) := a∈Sys EPath ω (L a , X).

Let GF(Σ) denote the class of all general flow logic models of signature Σ, and for the case of a single time line L, let GF(L, Σ) denote the subclass of all logic models M such that L(a) = L for all a ∈ Sys. For the further special case where |Sys| = 1 and Prp is countably infinite, let TR(N) denote the subclass of all discrete time logic models M with one general flow Φ R : X ; IPath(N, X) from a total transition relation R : X ; X (also called R-generable models [START_REF] Emerson | Deciding Full Branching Time Logic[END_REF][START_REF] Emerson | Sometimes" and "Not Never" revisited: on branching versus linear time[END_REF][START_REF] Reynolds | An Axiomatization of Full Computation Tree Logic[END_REF]). For the case of deterministic systems, let DF(L) denote the subclass of all logic models where the time line L is the non-negative half of a linearly ordered abelian group, and the one general flow Φ : X ; IPath(L, X) is deterministic, total, interval path, and non-blocking [START_REF] Coulthard | Temporal Logics of Dynamical Systems in Discrete and Dense Time[END_REF]. Definition 9. For ϕ ∈ L(Σ) and ω-path η ∈ EPath(M), the relation "ψ is satisfied along path η in model M", written M, η |= ψ, is defined by induction on the structure of formulae, with p ∈ Prp and a ∈ Sys:

M, η |= p iff η(0) ∈ P(p) M, η |= ¬ ψ iff M, η ψ M, η |= ψ 1 ∨ ψ 2 iff M, η |= ψ 1 or M, η |= ψ 2 M, η |= ψ 1 U a ψ 2 iff η ∈ EPath ω (L a , X) and ∃ t ∈ dom(η) with t > 0 : M, t |η |= ψ 2 and ∀s ∈ (0, t) ∩ dom(η) : M, s |η |= ψ 1 M, η |= ∀ a ψ iff ∀ξ ∈ (E ω Φ a )(η(0)) : M, ξ |= ψ
For formulas ϕ ∈ L(Σ), the ω-path denotation set ϕ M ⊆ EPath(M), and the state denotation set ϕ M st ⊆ X, are defined by: ϕ

M := { η ∈ EPath(M) | M, η |= ϕ } ϕ M st := { x ∈ X | ∃η ∈ EPath(M) : M, η |= ϕ and x = η(0) }
For a logic model M ∈ GF(Σ), class of logic models C ⊆ GF(Σ), and for formulas ϕ ∈ L(Σ), we say: The while...always operator is a negation dual of until: ϕ A a ψ def = ¬(ϕ U a (¬ ψ)) , which can be read as "if a type-a path, then while ϕ, always ψ". The semantics are:

• ϕ is satisfiable in M, if ϕ M st = ∅; • ϕ is true in M, written M |= ϕ , if M, η |= ϕ for every η ∈ EPath(M); • ϕ is C-valid, written |= C ϕ , if M |= ϕ for every M ∈ C. Define Valid(C) := {ψ ∈ L(Σ) | |= C ψ } to
M, η |= ϕ A a ψ iff if η ∈ EPath ω (L a , X) then ∀ t ∈ dom(η) with t > 0 , if (∀s ∈ (0, t) ∩ dom(η)) M, s |η |= ϕ then M, t |η |= ψ
Other one-place operators are defined as 3 a ϕ def = ⊤U a ϕ, a ϕ def = ⊤A a ϕ, ⊙ a ϕ def = ⊥U a ϕ, and a ϕ def = ¬ϕA a ⊥, where 3 a ϕ type-a paths along which ϕ will eventually be true in the future;

a ϕ type-a paths along which ϕ will always be true in the future, plus non-type-a paths; ⊙ a ϕ type-a paths along which time 0 has a discrete successor, and ϕ is true then;

a ϕ type a-paths along which ϕ is true immediately after now, plus non-type-a paths.

In particular, the next-time operators, ⊙ a , come out as: M, η |= ⊙ a ϕ iff

ϕ U •• a ψ def = ϕ ∧ ϕ U a (ϕ ∧ ψ) ϕ U •• a ψ def = ϕ ∧ ϕ U a ψ (3)
We briefly illustrate the expressivity of the logic in two areas.

Viability Theory: In the recent work of Aubin and co-workers in Viability Theory [START_REF] Aubin | Viability kernels and capture basins of sets under differential inclusions[END_REF][START_REF] Aubin | Impulse differential inclusions: A viability approach to hybrid systems[END_REF][START_REF] Aubin | Viability kernels and capture basins: Lecture notes[END_REF], the key concept is of paths being "viable in K until capturing target C". Define:

ϕ V a ψ def = ( ⊤ U a ⊤ ∧ ϕ ∧ a ϕ ∧ a 3 a ⊤ ) ∨ ϕ U •• a ψ (4)
The formula ϕ V a ψ is satisfied by an ω-path η ∈ EPath ω (L a , X) iff either ϕ is true now and at all times in the future along η, and the time domain of η is unbounded, or there is a finite time along η at which ψ becomes true, and ϕ is true at all times between now and then (inclusive). Thus η is either viable forever in the set ϕ M or viable in ϕ M until it captures the target set ψ M in finite time. Applying the path quantifiers ∃ a and ∀ a restricts to ω-paths of the system E ω Φ a , and this can be used to formalize in the logic the two-place state set operators known as the viability kernel with target and the invariance kernel with target.

Dynamical properties of hybrid automata:

Given a hybrid automaton H, assume that H is well-constituted, and define a logic model M H X with state space X ⊆ R n the continuous state space of H. Let the system label set Sys H X := Q, and for each q ∈ Q, the time line is L(q) := R +

• and the general flow systems are S(q) = Φ q := Sol q . Assume the atomic proposition set Prp H includes constants D q and G q for each q ∈ Q, and the valuation P : Prp H ; X satisfies P(D q ) = D q , and P(G q ) = Grd q .

• Traj H is non-blocking iff M H X |= q∈Q ( ( q ¬ D q ) → G q ) • If Traj H is non-blocking, then Traj H has no livelock iff M H X |= q∈Q ∀ q ( ( D q ∧ 3 q ¬ D q ) → ( D q U q ( G q ∧ 3 q ¬ D q ) ) ) We can, of course, also form a logic model M H with state space Q × X, and have a single system label Sys H := {0} with the general flow system Φ 0 := Traj H , and formalize with the operators U 0 and ∀ 0 quite sophisticated temporal and dynamic properties of H as a single system. We can also reason about multiple systems over a common state space, and express comparative properties.

  For elements a, b ∈ L, the set [a, b] := {l ∈ L | a l b} is a closed, bounded interval in L, and (a, b) := {l ∈ L | a < l < b} is an open bounded interval; similarly for half-open/half-closed bounded intervals [a, b) and (a, b]. For right unbounded intervals, we write [a, ∞) := {l ∈ L | a l}. Any subset T ⊆ L gives a linear order (T, < T ), where < T :=< ∩(T × T ). Define a partial function succ L : L L, for a, b ∈ L, by succ L (a) := b iff a < b and there does not

Definition 2 .

 2 Let (L, <, 0) be a time line. A bounded time domain in L is a proper subset T ⊂ L with least element 0 and a largest element b T such that T is a finite union of closed intervals in L, of the form T = i<N [a i , b i ], where N ∈ N and a 0 = 0 and a i b i < a i+1 for i < N -1, and b N -1 = b T . Let BT(L) ⊂ 2 L denote the set of all bounded time domains in L. Also define BI(L) := {T ∈ BT(L) | (∃b ∈ L) T = [0, b] } to be the subset of interval time domains. Over any set (signal space) X = ∅, define the set of L-paths in X, by Path(L, X) := { γ : L

  be the set of all C-valid formulas, and define CTL ⋆ := Valid( TR(N) ) and GFL ⋆ := Valid( GF(Σ) ).

  for T := dom(η) and 0 ∈ dom(succ T ) and k := succ T (0) and M, k |η |= ϕ Different versions of until come by varying the constraints on end-values of the bounded paths that satisfy ϕ until they satisfy ψ :

Definition 10. Given a class of logic models C ⊆ GF(Σ), the validity problem for C is to determine, for any given formula ϕ ∈ L(Σ), whether or not ϕ ∈ Valid(C). The validity problem for C is decidable if there is a recursive procedure for determining membership of Valid(C) that finitely terminates on all input formulae ϕ ∈ L(Σ).

Proposition 10. [START_REF] Emerson | Deciding Full Branching Time Logic[END_REF][START_REF] Emerson | Complexity of tree automata and modal logics of programs[END_REF] The validity problem is decidable CTL ⋆ (the class TR(N) of discrete time models), with complexity double exponential time in the length of the formula.

We conjecture that the validity problem is decidable for the class DF(R +

• ) of deterministic, total, interval path, non-blocking flows described by functions φ : X ×R → X satisfying the group action laws. These models are studied in [START_REF] Coulthard | Temporal Logics of Dynamical Systems in Discrete and Dense Time[END_REF], where they are used to give semantics for until and since (the time-reversal or past tense correlate) in the language of Linear Temporal Logic (LTL), with no path quantifiers, and the validity problem for that logic is decidable.

Axiomatisation and soundness

We seek formal deductive proof systems for GFL ⋆ := Valid(GF(Σ)), or for the validity set of distinguished subclasses of general flow models. The soundness or adequacy of a proof system Λ for a semantically characterized formula set such as GFL ⋆ , is the property that if ϕ is provable in Λ, then ϕ ∈ GFL ⋆ . For soundness proofs, the larger the class of semantic models, the stronger the result (so we do rather well here on that score). The technically much more challenging task is to establish completeness of a proof system Λ, which in our case is the property: if ϕ ∈ GFL ⋆ , then ϕ is provable in Λ. Proofs of completeness proceed via the contrapositive, and in that form, are essentially a model realization problem: if ϕ is Λ-consistent (i.e. the formula ¬ ϕ is not provable in Λ), then there exists a logic model M ∈ GF(Σ) in which ϕ is satisfiable. Generally speaking, the smaller the class from which the realization models are drawn, the stronger or tighter the completeness result.

An axiomatic proof system Λ consists of a recursive list of axioms, usually given by taking all instances in the language of some finite set of formula schemes, together with a finite list of inference rules, of the form: if ϕ is provable in Λ, then ψ is provable in Λ. A formula is provable in Λ if it is an axiom of Λ or is derivable from provable formulas by a finite sequence of applications of inference rules. We write ⊢ Λ ϕ to mean that ϕ is provable in the system Λ.

A sound and complete axiomatic proof system for the logic CTL ⋆ remained an open problem for almost 20 years, and was solved by Reynolds quite recently [START_REF] Reynolds | An Axiomatization of Full Computation Tree Logic[END_REF]. That axiomatization lays side by side a list of axioms for path formulae, obtained from axiomatizing LTL together with a list of axioms for universal quantification over paths. In addition, Reynolds' proof system includes the axiom ⊥U⊤, which asserts that the underlying time line is discrete, or equivalently, the discrete successor map is total. It also includes an additional inference rule, which is an induction rule for "recursively unwinding" Until formulae in terms of the next-time operator. The axiomatic proof system we present for GFL ⋆ consists of Reynolds' system for CTL ⋆ , minus those last two "discrete" items, the axiom and rule.

Let Λ be the proof system having as axioms all formulae of L(Sig) that are instances of propositional tautologies, or are instances of the schemes (P1) -(P6) and (Q1) -(Q5) below, and having as rules of inference the propositional rule of Modus Ponens (MP) along with three monotonicity rules:

Proposition 11. (Soundness of Axiomatisation) For every formula ϕ ∈ L(Sig),

The verification of soundness of an axiom scheme ϕ consists of showing that M |= ϕ for every model M ∈ GF(Σ), and for an inference rule of the form if ⊢ Λ ϕ then ⊢ Λ ψ , one needs to show that if M |= ϕ, then M |= ψ, for all models M ∈ GF(Σ).

We give some verbal explanation for a selection of the axioms. The first axiom, (P1), asserts that the union over a of all type-a paths is equal to the whole ω-path space of the model. To understand (P5), suppose γ is an a-path satisfying ϕ U a ψ. Then there must be some positive time t along γ at which the suffix path t |γ satisfies ψ and at all strictly intermediate points along γ the suffix paths satisfy ϕ. In particular at all those strictly intermediate points, the suffix paths satisfy ϕ and ϕ U a ψ, meaning that γ satisfies (ϕ ∧ ϕ U a ψ) U a ψ. The axiom (P6) is sound because of the fusion closure of the ω-path space since the antecedent contains embedded Until operators. The axioms (Q1-Q5) all follow directly from the meaning of the universal (and existential) quantification. The three rules all express the monotonicity of the operators with respect to subset inclusion.

Summary and discussion

In this paper, we propose and develop a quite general class of dynamical system models we call general flow systems which include and extend the broad class of evolutionary systems identified by Aubin, and the complete state behaviours of Willems. The advance specifically consists in modelling hybrid time paths as entities in their own right. We take the syntactic constructs of the non-deterministic and branching temporal logic CTL ⋆ originally developed for discrete time models, and re-interpret them in a semantics over general flow systems and with respect to arbitrary time lines. We propose a first candidate for an axiomatic proof system for the class of general flow models, and establish the soundness or adequacy of the proof system.