We propose a strong notion of viability for a set of states of a nonlinear switched system. This notion is defined with respect to a fixed region of the state space and can be interpreted as a condition under with a system can be forced to stay in a given safe set by applying a specific control strategy only when its state is outside the fixed region. When the state of the system is inside the fixed region, the control can be kept constant without the risk of driving the system into unsafe set (the complement of the safe set). We investigate and give a convenient sufficient condition for strong viability of the complement of the origin for a nonlinear switched system with respect to a fixed region.
A subset of the state space of a control system is called viable, if for any initial point in this set there exists a solution of the control system which stays forever in this set. Usual problems associated with viability are checking if a given set is viable, finding a solution (and/or the corresponding control input) which stays forever in this set (viable solution), designing a viable region [2]. Viability was studied in many works on the theory of differential equations and inclusions and the control theory [20,5,2,3,9,19,24,21,7,10,1,16,6]. The corresponding results can be straightforwardly applied to control and verification problems for hybrid (discrete-continuous) systems [11] and other models of cyber-physical systems [22,4,17,23], assuming that viable sets are interpreted as safety regions. However, this interpretation suggests certain natural generalizations of sufficient condition which can be used to verify that for a given system, X, and Y , X is Y -strongly viable.
To do this we will use the notion of a Nondeterministic Complete Markovian System (NCMS) [14] which is based on the notion of a solution system by O. Hájek [12]. More specifically, we will represent the system (1) using a suitable NCMS and reduce the problem of Y -strong viability of a set X to the problem of the existence of global-in-time trajectories of NCMS which was investigated in [14,15] and apply a theorem about the right dead-end path in NCMS [15] in order to obtain a condition of Y -strong viability.
To make the paper self-contained, in Section 2 we give the necessary definitions and facts about NCMS. In Section 3 we formulate and prove the main result of the paper.
We will use the following notation: N = {1, 2, 3, ...}, N 0 = N ∪ {0}, R is the set of real numbers, R + is the set of nonnegative real numbers, f : A → B is a total function from a set A to a set B, f : A →B denotes a partial function from a set A to a set B. We will denote by 2 A the power set of a set A and by f | A the restriction of a function f to a set A.
If A, B are sets, then B A will denote the set of all total functions from A to B and A B will denote the set of all partial function from A to B.
For a function f : A →B the symbol f (x) ↓ (f (x) ↑) mean that f (x) is defined, or, respectively, undefined on the argument x.
We will not distinguish the notions of a function and a functional binary relation. When we write that a function f : A →B is total or surjective, we mean that f is total on the set A specifically (f (x) is defined for all x ∈ A), or, respectively, is onto B (for each y ∈ B there exists x ∈ A such that y = f (x)).
We will use the following notations for f : A →B: dom(f ) = {x | f (x) ↓}, i.e. the domain of f (note that in some fields like category theory the domain of a partial function is defined differently), and range(f ) = {y | ∃x f (x) ↓ ∧ y = f (x)}. We will use the same notation for the domain and range of a binary relation
We will denote by f (x) ∼ = g(x) the strong equality (where f and g are partial functions): f (x) ↓ if and only if g(x) ↓, and f (x) ↓ implies f (x) = g(x).
We will denote by f • g the functional composition:
For any set X and a value y we will denote by X → y a constant function defined on X which takes the value y.
Also, we will denote by T the non-negative real time scale [0, +∞) and assume that T is equipped with a topology induced by the standard topology on R.
The symbols ¬, ∨, ∧, ⇒, ⇔ will denote the logical operations of negation, disjunction, conjunction, implication, and equivalence respectively.
The notion of a NCMS was introduced in [13] for studying the relation between the existence of global and local trajectories of dynamical systems. It is close to the notion of a solution system by O. Hájek [12], however there are some differences between these two notions [14].
Denote by T the set of all intervals (connected subsets) in T which have the cardinality greater than one.
Let Q be a set (a state space) and T r be some set of functions of the form s : A → Q, where A ∈ T. The elements of T r will be called (partial) trajectories.
The set (T r, ) is a (possibly empty) partially ordered set. Definition 4. ( [13,14]) A nondeterministic complete Markovian system (NCMS) is a triple (T, Q, T r), where Q is a set (state space) and T r (trajectories) is a set of functions s : T →Q such that dom(s) ∈ T, which is CPR, complete, and Markovian.
An overview of the class of all NCMS can be given using the notion of an LR representation [13][14][15]. Definition 5. ( [13,14]) Let s 1 , s 2 : T →Q. Then s 1 and s 2 coincide:
Let Q be a set. Denote by ST (Q) the set of pairs (s, t) where s : A → Q for some A ∈ T and t ∈ A. Definition 6. ( [13,14]
, and, moreover, p(s, t) holds whenever t is the least element of dom(s);
(2) right-local, if p(s 1 , t) ⇔ p(s 2 , t) whenever {(s 1 , t), (s 2 , t)} ⊆ ST (Q) and s 1 .
= t+ s 2 hold, and, moreover, p(s, t) holds whenever t is the greatest element of dom(s).
Let LR(Q) be the set of all pairs (l, r), where l : ST (Q) → Bool is a left-local predicate and r : ST (Q) → Bool is a right-local predicate.
The following theorem gives a representation of NCMS using predicate pairs.
The problem of the existence of global trajectories of NCMS was considered in [13,14] and was reduced to a more tractable problem of the existence of locally defined trajectories. Informally, the method of proving the existence of a global trajectory in NCMS consists of guessing a "region" (subset of trajectories) which presumably contains a global trajectory and has a convenient representation in the form of (another) NCMS and proving that this region indeed contains a global trajectory by finding or guessing certain locally defined trajectories independently in a neighborhood of each time moment.
Below we briefly state the main results about the existence of global trajectories of NCMS described in [15].
Let Σ = (T, Q, T r) be a fixed NCMS.
is strictly decreasing in the first argument and strictly increasing in the second argument, and for each x ≥ 0,
An example of a right extensibility measure is f + 1 (x, y) = 2y − x. Let f + be a right extensibility measure.
Theorem 2. ( [15], About right dead-end path) Assume that f + is a normal right extensibility measure and Σ satisfies LFE. Then each right dead-end path is strongly escapable if and only if each right dead-end path is f + -escapable. Lemma 1. ( [15]) Σ satisfies GFE if and only if Σ satisfies LFE and each right dead-end path is strongly escapable.
Let (l, r) be a LR representation of Σ. Then Σ has a global trajectory if and only if there exists a pair (l , r ) ∈ LR(Q) such that (1) l (s, t) ⇒ l(s, t) and r (s, t) ⇒ r(s, t) for all (s, t) ∈ ST (Q);
(2) ∀t ∈ [0, ] l (s, t) ∧ r (s, t) holds for some > 0 and a function s
Let I, I, and f i , i ∈ I, and x(t; t 0 ; x 0 ; σ) be defined as in Section 1. Let X = R n \{0} and Y ⊂ R n be a set. Let denote D = R n \Y .
Let us state the main result:
Theorem 4. Assume that:
(1) for each t ∈ T there exist i 1 , i 2 ∈ I such that f i 1 (t, 0) and
Then X is Y -strongly viable.
We will need several lemmas to prove this theorem. Let us fix an element x * 0 ∈ X. Let Q = R n × I. Denote by pr 1 : Q → R n , pr 2 : Q → I the projections on the first and second component, i.e. pr 1 ((x 0 , i)) = x 0 and pr 2 ((x 0 , i)) = i.
Let T r be the set of all functions s : A → Q, where A ∈ T, such that the following conditions are satisfied, where x = pr 1 • s and σ = pr 2 • s:
x is absolutely continuous on each segment [a, b] ⊆ A (a < b) and satisfies the equation d dt x(t) = f i (t, x(t)) a.e. on A; 3) x(t) = 0 for all t ∈ A; 4) for each non-maximal t ∈ A such that x(t) / ∈ D there exists t ∈ (t, +∞)∩A such that σ(t ) = σ(t) for all t ∈ [t, t ); 5) for each non-minimal t ∈ A such that x(t) / ∈ D there exists t ∈ (0, t) ∩ A such that σ(t ) = σ(t) for all t ∈ (t , t]; 6) if 0 ∈ A, then x(0) = x * 0 . It follows straightforwardly from this definition that Σ(x * 0 ) = (T, Q, T r) is a NCMS (i.e. T r is a CPR, Markovian, and complete set of trajectories).
Let us find a sufficient condition which ensures that Σ has a global trajectory. (2) Let us choose any i 0 ∈ I and define x : T → R n as x(t) = x(t; 0; x * 0 ; σ 0 ) for all t ∈ T , where σ 0 (t) = i 0 for all t. Then x is continuous and x(0) = x * 0 = 0, so there exists ε > 0 such that x(t) = 0 for all
Lemma 3. Assume that:
(1) for each t ∈ T there exist i 1 , i 2 ∈ I such that f i1 (t, 0), f i2 (t, 0) are (nonzero) noncollinear vectors, i.e.
then pr 1 (s(t)) ∈ D for some t ∈ [t 1 , t 2 ).
Then each right dead-end path in Σ(x * 0 ) is f + 1 -escapable, where f + 1 (x, y) = 2y −x is a right extensibility measure. Firstly, consider the case when x l = 0. Then x l > 0. Let us choose an arbitrary t 0 ∈ (a, b) such that b − t 0 < x l /(4M ) and x(t 0 ) − x l < x l /2 (this is possible, because x l = lim t→b− x(t)). Let σ : [t 0 , +∞) → I and x : [t 0 , +∞) → R n be functions such that σ (t) = σ(t 0 ) for all t ≥ t 0 and x (t) = x(t; t 0 ; x(t 0 ); σ ) for all t ≥ t 0 . Then x (t 0 ) = x(t 0 ) − x l + x l ≥ x l −
x(t 0 ) − x l > x l /2 > 2M (b − t 0 ). Then for all t ≥ t 0 we have
We have proposed the notion of an Y -strongly viable set X for nonlinear switched systems. This notion follows naturally from interpretation of viable sets as safety regions. We have considered the case when X is the complement of the origin (i.e. the origin may be interpreted as a safety hazard) and proposed a convenient sufficient condition which can be used to verify that for a given system, X, and Y , X is Y -strongly viable. In the forthcoming papers we plan to investigate other cases give the corresponding conditions.
Let d = 2b − t 0 . Then d > t 0 because t 0 < b. Then x (t) = 0 for all t ∈ [t 0 , d]. Let s * : [t 0 , d] → Q be a function such that s * (t) = (x (t), σ (t)) for all t ∈ [t 0 , d]. It follows immediately that s * ∈ T r. Also, s * (t 0 ) = s(t 0 ) and d = 2b − t 0 = f + 1 (t 0 , b). Then s * is an escape from s and s is f + 1 -escapable. Now consider the case when x l = 0. Let us choose i 1 , i 2 ∈ I such that v 1 = f i 1 (b, 0) and v 2 = f i 2 (b, 0) are noncollinear (this is possible by the assumption 1 of the lemma). Then the function h
Let ε = M/2 > 0. Because f is continuous, there exists δ > 0 such that for each j = 1, 2, t ∈ T , and
Let us choose an arbitrary c
Then the following two cases are possible. a) There exists j ∈ {1, 2} such that 0 / ∈ range(x j ). Let us choose any d ∈ (max{2b − t 0 , t 0 }, t 2 ) (this is possible, because t 0 < b < t 2 and 2b − t 0 ≤ 2b − c < b + R/2 < b + R = t 2 ). Then let s * : [t 0 , d] → Q be a function such that s * (t 0 ) = s(t 0 ) = (x(t 0 ), σ(t 0 )) and s * (t) = (x j (t), i j ) for all t ∈ (t 0 , d]. Because x j (t 0 ) = x(t 0 ) ∈ D and x j (t) = 0 for all t ∈ [t 0 , t 2 ] ⊃ [t 0 , d], we have that s * ∈ T r. Besides, s * (t 0 ) = s(t 0 ) and d > 2b − t 0 = f + 1 (t 0 , b), so s * is an escape from s and s is f + 1 -escapable. b) 0 ∈ range(x 1 )∩range(x 2 ). Then because x 1 , x 2 are continuous, there exist
If we suppose that x j (t) < R for each j = 1, 2 and t ∈ [t 0 , t j ], then d j (t) = f ij (t, x j (t)) − v j < ε for each j = 1, 2 and t ∈ [t 0 , t j ], whence
We have a contradiction, so there exists j ∈ {1, 2} and t ∈ [t 0 , t j ] such that x j (t ) ≥ R. This implies that
Lemma 4. Assume that:
(1) for each t ∈ T there exist i 1 , i 2 ∈ I such that f i 1 (t, 0) and f i 2 (t, 0) are noncollinear;
(2) {0} is a path-component of {0} ∪ Y .
Then Σ(x * 0 ) has a global trajectory.
Proof. Let us show that the assumption 2 of Lemma 3 holds. Let s ∈ T r,
) and γ(1) = 0. Then γ is continuous, so there is a path from γ(0) = x(t 1 ) = 0 to 0 in {0}∪(R n \D) = {0}∪Y (considered as a topological subspace of R n ). This contradicts the assumption that {0} is a path-component of {0} ∪ Y . Thus x(t) ∈ D for some t ∈ [t 1 , t 2 ).
The assumption 1 of Lemma 3 also holds, so by Lemma 2, Lemma 3, Lemma 1, Theorem 2, Σ satisfies GFE. Besides, by Lemma 2 there exists s ∈ T r with dom(s) = [0, ε] for some ε > 0, so by the GFE property, Σ has a global trajectory.
Proof (of Theorem 4). Follows straightforwardly from Lemma 4, because the statement of Lemma 4 holds for any x * 0 ∈ X.