C Combastel

Functional sets with typed symbols : Mixed zonotopes and Polynotopes for hybrid nonlinear reachability and filtering

Keywords: Functional sets, Polynomial dependencies, Mixed encoding, Logic, Hybrid dynamic systems, Reachability, Robust state estimation, Kalman filters, Zonotopes, Polynotopes

Verification and synthesis of Cyber-Physical Systems (CPS) are challenging and still raise numerous issues so far. In this paper, based on a new concept of mixed sets defined as function images of symbol type domains, a compositional approach combining eager and lazy evaluations is proposed. Syntax and semantics are explicitly distinguished. Both continuous (interval) and discrete (signed, boolean) symbol types are used to model dependencies through linear and polynomial functions, so leading to mixed zonotopic and polynotopic sets. Polynotopes extend sparse polynomial zonotopes with typed symbols. Polynotopes can both propagate a mixed encoding of intervals and describe the behavior of logic gates. A functional completeness result is given, as well as an inclusion method for elementary nonlinear and switching functions. A Polynotopic Kalman Filter (PKF) is then proposed as a hybrid nonlinear extension of Zonotopic Kalman Filters (ZKF). Bridges with a stochastic uncertainty paradigm are briefly outlined. Finally, several discrete, continuous and hybrid numerical examples including comparisons illustrate the effectiveness of the theoretical results.

Introduction

Uncertainty management undoubtedly remains a great challenge when designing, observing, controlling and verifying systems with stringent safety, reliability and accuracy requirements. Common industrial practice still makes intensive use of Monte-Carlo simulations and design of experiments to check for robustness, perform sensitivity analysis and optimize tuning. Meanwhile, given some model of the available knowledge, which is by essence subject to uncertainties, formal methods provide verification and synthesis tools likely to ensure a full coverage wrt to the range of specified behaviors, including off-nominal and worst cases. Dealing with complex dynamics such as nonlinear and hybrid ones remains challenging and the achieved trade-off between computation time and accuracy heavily depends on underlying set representations. However, a direct use of set-membership techniques (e.g. intervals, ellipsoids, etc) is often subject to the so-called This paper was not presented at any IFAC meeting. Corresponding author: C. Combastel. ©2022. This manuscript version is made available under the CC-BY-NC-ND 4.0 license https://creativecommons.org/licenses/by-nc-nd/4.0/ Email address: christophe.combastel@u-bordeaux.fr (C. Combastel).

dependency problem and/or the wrapping effect. The former comes from the loss of variable multi-occurrences when overloading basic operators. The latter results from the necessary approximate (usually outer) description of true solution sets. This has motivated the use of affine arithmetic [START_REF] Henrique | Affine arithmetic: Concepts and applications[END_REF][START_REF] Rump | Implementation and improvements of affine arithmetic[END_REF] and other set representations of intermediate complexity between intervals [START_REF] Jaulin | Applied interval analysis[END_REF][START_REF] Raïssi | Some recent results on the design and implementation of interval observers for uncertain systems[END_REF][START_REF] Thach | On fixed-time interval estimation of discretetime nonlinear time-varying systems with disturbances[END_REF] or ellipsoids [START_REF] Kurzhanskiy | Ellipsoidal techniques for reachability analysis of discrete-time linear systems[END_REF] and polytopes [START_REF] Grünbaum | Convex Polytopes[END_REF] or level sets [START_REF] Mitchell | The flexible, extensible and efficient toolbox of level set methods[END_REF], like zonotopes [START_REF] Kühn | Rigorously computed orbits of dynamical systems without the wrapping effect[END_REF][START_REF] Combastel | A state bounding observer based on zonotopes[END_REF][START_REF] Goubault | A zonotopic framework for functional abstractions[END_REF], a class of convex and centrally symmetric polytopic sets defined as the affine image of a unit hypercube. Zonotopes have been used to address the reachability of linear [START_REF] Puig | Worst-case simulation of discrete linear time-invariant interval dynamic systems[END_REF][START_REF] Girard | Reachability of uncertain linear systems using zonotope[END_REF][START_REF] Combastel | On computing envelopes for discrete-time linear systems with affine parametric uncertainties and bounded inputs[END_REF], nonlinear [START_REF] Althoff | Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets[END_REF][START_REF] Althoff | Reachability analysis of nonlinear differential-algebraic systems[END_REF][START_REF] Goubault | Robust underapproximations and application to reachability of non-linear control systems with disturbances[END_REF] and hybrid e.g. [START_REF] Maïga | A comprehensive method for reachability analysis of uncertain nonlinear hybrid systems[END_REF] systems, as well as state bounding observation [START_REF] Combastel | A state bounding observer based on zonotopes[END_REF][START_REF] Alamo | Guaranteed state estimation by zonotopes[END_REF][START_REF] Combastel | A state bounding observer for uncertain non-linear continuous-time systems based on zonotopes[END_REF][START_REF] Vu Tuan | Zonotopic guaranteed state estimation for uncertain systems[END_REF], possibly with links to a stochastic paradigm [START_REF] Combastel | Zonotopes and Kalman observers: Gain optimality under distinct uncertainty paradigms and robust convergence[END_REF][START_REF] Combastel | An extended zonotopic and gaussian kalman filter (EZGKF) merging set-membership and stochastic paradigms: Toward non-linear filtering and fault detection[END_REF], or in a distributed context [START_REF] Orihuela | Negotiated distributed estimation with guaranteed performance for bandwidth-limited situations[END_REF][START_REF] Combastel | A distributed Kalman filter with symbolic zonotopes and unique symbols provider for robust state estimation in CPS[END_REF]. With zonotopes, affine function transforms correspond to implicit set operations and the evaluation of bounds can be delayed (lazy evaluation [START_REF] Sinot | Complete laziness: A natural semantics[END_REF]), to the benefit of a better management of dependencies. Moreover, an analogy can be noticed between such affine function transforms and the manipulation of symbolic expressions at a syntactic level (e.g. x -x simplified as 0 before substituting the unit interval [-1, +1] for x in x -x). In addition, the important distinction between syntax (e.g. formal transformation rules) and semantics (e.g. the interpretation/evaluation of some expression) is easily lost when directly operating sets. By extending ideas originating from affine arithmetic [START_REF] Henrique | Affine arithmetic: Concepts and applications[END_REF] and further developed, e.g., for the static analysis of programs by abstract interpretation [START_REF] Goubault | A zonotopic framework for functional abstractions[END_REF], symbolic zonotopes and USP (Unique Symbol Provider) in [START_REF] Combastel | A distributed Kalman filter with symbolic zonotopes and unique symbols provider for robust state estimation in CPS[END_REF] showed the relevance of these concepts in a context of distributed state estimation. To summarize, a clear distinction between syntax and semantics is a key point to struggle against the dependency problem in set-membership computations.

When addressing core problems like reachability, state estimation, identification, invariant sets [START_REF] Wang | Set-invariance characterizations of discrete-time descriptor systems with application to active mode detection[END_REF] and fault diagnosis [START_REF] Xu | Set-theoretic methods in robust detection and isolation of sensor faults[END_REF][START_REF] Scott | Constrained zonotopes: A new tool for set-based estimation and fault detection[END_REF][START_REF] Pourasghar | A zonotopic Kalman filter optimizing fault detection rather than state estimation[END_REF], non-convex and possibly nonconnected sets are often required when dealing with nonlinear and/or hybrid systems. Taylor models [START_REF] Makino | Rigorous integration of flows and odes using taylor models[END_REF] are an alternative to represent non-convex sets. Dealing with non convex and/or non-connected sets is also possible through pavings [START_REF] Jaulin | Applied interval analysis[END_REF] or level sets [START_REF] Mitchell | The flexible, extensible and efficient toolbox of level set methods[END_REF] but costly since related algorithms respectively rely on bisections or grids, both yielding an exponential complexity. Using properties like monotony/cooperativity [START_REF] Ramdani | A hybrid bounding method for computing an over-approximation for the reachable set of uncertain nonlinear systems[END_REF] often impose restrictions either on the class of dynamics that can readily be handled, or on accuracy due to the lack of richer internal set descriptions. In the hybrid case, the crossing of guards can generate many pieces of flows. Bissection/branching may be used, but the benefit of fast methods is then often lost due to the complexity induced by the propagation of a large number of (possibly smaller) instances which unduly become fully independent after branching/bissection. Thus, two complementary directions can be considered and combined : finding more versatile set representations possibly i) non convex while preserving scalability, and ii) non connected to propagate unions/bundles of a possibly large number of (implicit) sets characterizing distinct/discrete configurations/modes, without full bissections/branching, that is, while sharing and keeping trace of the common features between all these sets. The combination of i) and ii) pleads in favor of searching for some kind of unified representation to encode and operate mixed sets (i.e. hybrid sets).

Though zonotopic sets catch some linear dependencies, their convex, connected, and centrally symmetric nature still impose restrictions to address the reachability of nonlinear and hybrid (i.e. mixed continuous/discrete) dynamic systems. To overcome these restrictions, Taylor models [START_REF] Makino | Rigorous integration of flows and odes using taylor models[END_REF], polynomial zonotopes [START_REF] Althoff | Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets[END_REF] and sparse polynomial zonotopes (spz) [START_REF] Kochdumper | Sparse polynomial zonotopes: A novel set representation for reachability analysis[END_REF] rely on sets defined as polynomial images rather than affine/linear ones. spz can thus efficiently store and operate a large class of non convex continuous sets. However, spz do not natively handle the case of discrete or mixed sets, which motivates the distinct features introduced with the polynotopes proposed in this paper. Moreover, constraints can be also introduced in set representations as with constrained zonotopes [START_REF] Scott | Constrained zonotopes: A new tool for set-based estimation and fault detection[END_REF] and, recently, constrained polynomial zonotopes [START_REF] Kochdumper | Constrained polynomial zonotopes[END_REF]. Note that the evaluation of bounds under constraints, even if delayed, may be costly and involve iterative algorithms (e.g. linear programming with constrained zonotopes). Polynotopes will thus introduce typed symbols whose management involves specific polynomial constraints that can be efficiently handled.

Contributions. This paper introduces a new concept of jointly mathematical and computational objects called polynotopes allowing to define and operate functional sets with typed symbols. By focusing on one continuous (interval) and two discrete (signed, boolean) symbol types, it is shown how the resulting non convex, non centrally symmetric and non connected mixed sets extending zonotopes (including polynomial ones) can be used to implement advanced hybrid nonlinear reachability and filtering algorithms without relying on costly bissections. Syntax and semantics are explicitly distinguished while combining both a strict/eager evaluation of polynotope objects (mainly addressing the dependency problem) and a lazy/delayed evaluation of bounding sets (mainly addressing the wrapping effect). Mixed encoding of intervals and dependency preserving inclusion methods for elementary nonlinear and switching functions are proposed. Polynomial representation of logic functions defined on {-1, +1} (signed logic) or {0, 1} (boolean logic) is analyzed and a functional completeness result is given for polynotopes. Based on operator overloading, the generic implementation of an original Polynotopic Kalman Filter (PKF) extending Zonotopic Kalman Filters (ZKF) to hybrid nonlinear systems is obtained. Several discrete, continuous and hybrid numerical examples illustrate the main theoretical results.

Organization. After extending the notion of inclusion function classically used in interval arithmetic to general sets in section 2, the motivation and the construction/composition of polynotope objects is treated in section 3. Uniquely identified typed symbols are also introduced in this section. A possible implementation of the polynotope objects is then gradually introduced in section 4 by first starting from symbolic/mixed zonotopes and mixed encoding of intervals, and then extending sparse polynomial zonotopes with specific features making it possible to handle mixed sets in a unified way. In section 5, modeling tools for nonlinear hybrid systems are given with emphasis placed on a compositional approach relying on basic logic gates and basic nonlinear continuous and switching functions. Inclusion methods are also given. Then, a Polynotopic Kalman Fiter (PKF) extending ZKF to hybrid nonlinear systems is developed in section 6. Through basic operators/functions overloading, its implementation can benefit from the proposed dependency preserving compositional inclusion methods. The links between PKF, ZKF and the basic stochastic Kalman Filter KF [START_REF] Kalman | A new approach to linear filtering and prediction problems[END_REF] are made explicit. In section 7, numerical examples including comparisons illustrate the effectiveness of the proposed scheme, before concluding remarks in section 8. included in some set X. Thus, ĪX = {IX}. The continuous example with DX = Ī Rn is classically used to define inclusion functions in the particular case of interval arithmetic with possibly unbounded1 intervals.

Definition 1 (imset) Given a function f : Dx → Dy, x → y = f (x), and a set X ⊂ Dx, the imset of X by f is:

f (X) = {f (x) | x ∈ X}.

Definition 2 (Inclusion function)

The function g : DX → DY , X → Y = g(X) is an inclusion function for f : Dx → Dy, x → y = f (x), if Dx ∈ DX and: ∀X ∈ DX, f (X) ⊂ g(X), where f (X) is the imset of X ⊂ Dx by f , and g(X) is the image of X ∈ DX by g. Corollary 3 g must not be monotone wrt inclusion to be an inclusion function. Even without this requirement, it can be inferred that:

∀X ∈ DX, f (X) ⊂ g(Dx). Proof. Firstly, imset f : DX → DY , X → Y = f (X) is monotone wrt inclusion: X 1 ⊂ X 2 ⇒ imset f (X 1 ) ⊂ imset f (X 2 )
. Moreover, from the definition 2, ∀X ∈ DX, X ⊂ Dx, and the monotony of imset f wrt inclusion gives: ∀X ∈ DX, f (X) ⊂ f (Dx). Also, since Dx ∈ DX, f (Dx) ⊂ g(Dx). Thus, ∀X ∈ DX, f (X) ⊂ g(Dx), without requiring the additional statement that g must be monotone wrt inclusion to be an inclusion function.

Remark 4

In general, 2 Dx ⊂ DX. This may lead to some conservatism when using an inclusion function de-fined over DX to enclose the image of any arbitrary subset X ∈ 2 Dx of Dx. This kind of wrapping effect is hardly avoidable in practice since, in most cases, not all subsets of Dx can be exactly represented in machine, especially when dealing with continuous and/or hybrid domains.

Remark 5 Syntax and semantics are not distinguished in this section 2 where the same notation x may refer to the (name of a) variable or a taken value.

A basic illustration of interval arithmetic's dependency problem is first given and analyzed. Let x denote any real such that

x ∈ [-1, +1] ⊂ R. Let f : R → R, x → x -x. i) Since ∀x, x -x = 0, f is the null function and the im- set f ([-1, +1]) of the interval [-1, +1
] by f is obviously the singleton {0}. ii) Let g be the natural interval extension of f i.e. g : I R → I R, x → x -x, where the minus operator is "overloaded" to deal with interval operands. g is an inclusion function for f . Thus:

f ([-1, +1]) ⊂ g([-1, +1]) = [-1, +1] -[-1, +1] = [-2, +2]. Conclu- sion: Though inclusion is preserved, [-2, +2] is a poor outer approximation of f ([-1, +1]) = {0}.
Whereas simply overloading basic interval operators would be the dream of a programmer wishing to implement uncertainty propagation computations, the natural interval extension is often subject to a significant conservatism. This is mainly due to the loss of dependencies between multiple occurrences of variables in the expressions to be evaluated (e.g. notice that x occurs twice in f and g). Indeed, important symbolic links are lost when substituting some interval value (semantics) for a given variable name/symbol (syntax) occurring in expressions/formula used to define mathematical functions and/or imsets as in definition 1. Moreover, iterative evaluations, e.g. to compute reachable sets of dynamical systems, often emphasize the drawbacks of a natural interval extension.

Then, should we definitely abandon the dream of encoding guaranteed (inclusion preserving), accurate and fast uncertainty propagation algorithms simply by overloading the operators used to define and program explicit mathematical functions? Beyond the natural interval arithmetic extension, how to tackle the dependency problem while dealing with possibly mixed (hybrid: continuous and discrete), non-convex and non-connected sets in a unified way?

3 Polynotope objects: Why and how?

Functional sets

Starting from intervals to represent bounding sets over continuous domains, explicit descriptions of more general sets is a possible direction to struggle against the dependency problem. Though general polytopes may look attractive to represent/approximate a large class of convex sets, the enumeration of their vertices and/or faces often remains poorly scalable. Paving and extensive use of contractions and bissections (branching) is another possible direction. However, bissections often restrict the scalability of accurate set approximations as the space dimension increases. Implicit rather than explicit set descriptions have also received a significant attention along the years e.g. ellipsoids described through a symmetric and positive definite (spd) matrix or as the imset of a unit hypersphere by a linear function, zonotopes (resp. polynomial zonotopes) most often viewed/defined as the imset of a unit hypercube [-1, +1]

[f c,R (s a )] of f c,R (s a ) is [f c,R (s a )] = f c,R ([s a ]) = f c,R ([-1, +1] p ) = c, R and idem with s b since [s b ] = [s a ] = [-1, +1] p (and so, even if s a = s b ). In this context, what about the composition of set-based enclosures? [f c,R (s a ) + f 0,-R (s a )] . . . a 1 ) . . . ⊂ [c + Rs a -Rs a ] ⊂ {c} = c, 0 a 2 ) . . . ⊂ [f c,R (s a )] + [f 0,-R (s a )] ⊂ c, 2R [f c,R (s b ) + f 0,-R (s a )] . . . b 1 ) . . . ⊂ [c+Rs b -Rs a ] ⊂ {c}+R[s b ]-R[s a ] ⊂ c, 2R b 2 ) . . . ⊂ [f c,R (s b )] + [f 0,-R (s a )] ⊂ c, 2R
In the cases a 1 and b 1 , a transformation/simplification of the symbolic expressions is first conducted (possibly based on an eager evaluation of terms interpreted as symbols rather than values) and the evaluation of set-based enclosures is delayed as much as possible (lazy evaluation). In the cases a 2 and b 2 , an eager evaluation using set-based enclosures as possible values is performed without any prior symbolic transformation. In the case of a 2 and compared to a 1 , this second approach yields a significant conservatism originating from the loss of dependencies between the two (thus, multiple) occurrences of s a which distinguish

a 1 , a 2 from b 1 , b 2 .
At this step, several directions orienting the following of this work can be drawn: i) Functions can be used to implicitly define sets as the image of their definition domain (e.g. unit hypercubes with affine functions f c,R for classical zonotopes).

ii) Working out a traceability of variable multioccurrences within the (possibly incrementally built) symbolic expressions used to define such functions/sets can help to struggle against the dependency problem.

iii) While elementary operators overloading is preferred to encapsulate the code required to easily compose com-plex functions/sets from simple ones, a global2 scope should be maintained for symbolic variables to prevent from losing global dependencies. iv) A trade-off between the efficiency of symbolic operations, their memory footprint, and the ability to quickly compute guaranteed and accurate set-based enclosures has to be found, possibly involving reduction schemes. v) By default, binding/linking/sharing is preferred to systematic bissection/branching in this work. vi) Set-based enclosures should be computed only when needed (call by need), so leading to a lazy/delayed evaluation of wrapping sets and/or bounds.

vii) The tight interactions between symbolic expressions and mathematical definitions as well as numerical computations reveals the need for distinguishing between syntax (symbolic level) and semantics (mathematical interpretations of symbolic expressions possibly resulting from numerical computations).

Syntax and semantics

With the ultimate goal of better managing dependencies that constitute a key for an accurate propagation of uncertainties, an explicit distinction between syntax and semantics is considered. Whereas syntax refers to rules defining symbol combinations that are correct in some language, semantics refers to the interpretation or meaning of related sentences. In other words, syntax refers to how writing correct statements, semantics indicates what they mean.

Let z denote a (symbolic) name that should be understood/interpreted as an object ιz. The interpretation operator ι assigns a meaning (e.g. mathematical or computational object, set, numerical value, etc) to the symbolic name z (and possibly to other symbols/names). In this paper, ι is a generic notation used to disambiguate symbolic names (syntax) from their meaning and/or taken values (semantics), whenever necessary. ιz can be viewed as a shortcut for ι(z) or [[z]] ι which is a usual notation for valuation (semantics) in logic and computer science. However, systematic formal definitions of interpretation/valuation operators are out of scope in this paper: ι simply reads as "interpretation of" for the sole purpose of drawing an explicit separation between operations at syntactic and semantic levels.

For example, Dx denoting a set containing the possible values (definition domain) of a variable named/symbolized by x. Then, ιx ∈ Dx reads as "the interpretation/value assigned to the variable named x belongs to the definition domain of x". Notice that usual mathematical notations do not distinguish between variable names and values (e.g. when writing x ∈ Dx for the variable x, as in section 2). Similarly, f may denote the name/symbol referring to a function explicitly denoted as ιf . Then, ιf stands for an interpretation of f (e.g. as a mathematical function, as a subroutine/algorithm, etc). Moreover, an evaluation ιf (ιx) of the function named f stands for the image/result obtained by applying ιf to the value ιx assigned to the input variable named x.

Typed symbols and unique identifiers

The so-called polynotope objects are interpreted (semantics) as image sets of vector polynomial functions defined from symbolic expressions (syntax) on domains related to different types of symbolic variables. For instance, continuous (unit interval) and/or discrete (signed, boolean) symbols can be combined to define and operate possibly mixed/hybrid sets. Following [START_REF] Combastel | A distributed Kalman filter with symbolic zonotopes and unique symbols provider for robust state estimation in CPS[END_REF], each of these symbols are uniquely identified in order to preserve dependencies while simplifying otherwise possible name binding issues. Considering other basic symbol types than interval (i), signed (s) and boolean (b) is among possible extensions that are left to future works:

Assumption 6 (Basic types) Let S be a finite set of typed symbols. Each typed symbol s i ∈ S is uniquely identified by an integer i ∈ N. In this paper, the type τ s i of any s i belongs to the set T = {i, s, b} of three basic symbol types respectively referring to interval (i), signed (s) and boolean (b). As shown in table 2, a definition domain is related to each of these basic types as

= [-1, +1], | + -| = {-1, +1}, | 1 0 | = {0, 1}
, respectively. By default, basic scalar values are assumed to be interpreted in the real field R equipped with the usual sum and product operators. A partition of T into continuous and discrete types is given by T = T c ∪ T d with T c = {i} and T d = {s, b}.

Definition 7 (Mixed, continuous, discrete) Let I ⊂ N and T I = ∪ i∈I {τ s i }. The symbolic vector s I is mixed (resp. continuous, discrete) if

(T I ∩ T c = ∅) ∧ (T I ∩ T d = ∅) (resp. T I ⊂ T c , T I ⊂ T d )
. By extension, any formula F (s I ) and/or related interpretation as (s-)function, (s-)zonotope, (s-)polynotope, etc can be qualified as mixed, continuous3 or discrete accordingly.

Corollary 8

In an entirely continuous case, following the assumption 6, all the symbols in s I are of type (unit) interval: ∀i ∈ I, τ s i = i, that is, ∀i ∈ I, ιτ s i = = [-1; +1]. As a result, for any vector I of n unique identifiers only referring to continuous symbols, any singlevalued interpretation4 ιs I of the symbolic vector s I belongs to the unit interval n , that is, ιs I ∈ [-1; +1] n . Assumption 9 (USP) A Unique Symbol Provider (USP) is assumed to be implemented as a global function (or service in a distributed context) called as !(n, t) Table 2 Notations for three basic symbol types in T = {i, s, b} respectively referring to "interval", "signed", "boolean". syntax semantics typed symbol si = x:i ιsi ∈ Dsi interval:

symbol type τ si = i ιτ si = Dsi = = [-1, +1]
typed symbol sj = z:s ιsj ∈ Dsj signed:

symbol type τ sj = s ιτ sj = Dsj = | + -| = {-1, +1} typed symbol s k = y:b ιs k ∈ Ds k boolean: symbol type τ s k = b ιτ s k = Ds k = | 1 0 | = {0, 1}
x, y, z : particular examples of (untyped) symbol names. The unique identifier of any typed symbol si ∈ S is i ∈ N.

with (n, t) ∈ N × T and then returning an n-dimensional vector I ∈ N n of n new unique identifiers referring to n new typed symbols of type t i.e. ∀i ∈ I, τ s i = t.

Remark 10 A simple implementation of !(n, t) is "l = l + n, return(h(t)1 n + 2 n h [l -n + 1, ..., l]
)" where 1 n denotes a vector of n ones, l is a persistent counter initialized to 0 at startup, and h : T → N assigns to each type t ∈ T a unique integer tag encoded with at most n h bits. Under the assumption 6, reserving n h = 2 bits and taking h({i, s, b}) = {1, 2, 3} is a possible choice to efficiently manage type tags within the unique integer identifiers of typed symbols. Extensions include an overflow checking or an implementation (possibly distributed) as a service in a CPS (Cyber-Physical System): see [START_REF] Combastel | A distributed Kalman filter with symbolic zonotopes and unique symbols provider for robust state estimation in CPS[END_REF] for details.

Construction/composition of polynotope objects

Based on uniquely identified typed symbols as in 3.3, the remainder of this section 3 aims at describing how the directions listed at the end of 3.1 can be achieved through polynotope objects, while introducing useful definitions to build well-grounded (e.g. inclusion preserving) mathematical interpretations. Consistently with the encapsulation principle [START_REF] Pierce | Types and Programming Languages[END_REF], internal data structures are left open in this section whereas some choice for them will be made explicit in section 4. Polynotopes interprets as functional sets based on vector polynomial functions with typed symbols i.e. any polynotopic set can be viewed as the imset of the definition domain of a vector polynomial function depending on variables/symbols of different types such as, e.g., the basic types in assumption 6. Meanwhile, a mechanism compatible with operator overloading is needed to achieve the direction iii) in 3.1, that is, providing a simple interface for the user to naturally encode non trivial compositions of elementary polynotopes, while maintaining a) a global scope for typed symbols to struggle against the so-called dependency problem and b) the rigor of inclusion preserving set-based interpretations. For this purpose, a formal grammar describing the syntax of a prototype language is given in Table 3. It supports a basic polynotope composition scheme (mainly Table 3 Context-free grammar in Backus-Naur Form (BNF) describing the syntax of a prototype language supporting the basic construction (through typed symbols) and composition of Polynotope objects.

Table 4

Left: Sample code accepted by the grammar in Table 3. Right: Evaluation of bounds resulting from a natural interval extension (int.) or some † polynotope computations (pol.). † here, e.g., interval hull of an outer zonotope. sample code

1 u=symb:i, 2 x=0.5+0.5*u, 3 f1=[x*x; x], 4 f2=f1(2)-f1(1), 5 f3=[x^2; x], 6 f4=f1-f3, 7 r=remainder:i, 8 f5=[x+-0.125+0.125*r; x], 9 f6=f5(2)-f5(1) int. [-1,+1] [0,1] [0,1]^2 [-1,1] [0,1]^2 [-1,+1]^2 [-1,+1] (*) [-1,5/4] pol. [-1,+1] [0,1] (*) [0,1/4] (*) {0}^2 [-1,+1] (*) [0,1/4] (*) = [[-1/4,1];[0,1]]
based on the <sfunref> lexical tokens5 ), as exemplified with the sample code in Table 4. Also, polynomials being closed under a finite6 number of compositions, it describes/accepts a set of well-formed formulas (wff) that can be operated at a symbolic level 7 .

Such operations preserve the ability to delay as much as needed set-based evaluations of typed symbols (lazy evaluation), while providing the formal ground for inclusion preserving mathematical interpretations8 . Moreover, the eager evaluation of an <sfunprog> source code (like the sample in table 4) using polynotope objects allows to transform polynotopic symbolic function (sfunction) declarations <sfundecl> (see also note (c) in Table 3) into s-function definitions <sfundef>, that is, a canonical kind of <sfunction> such that all the references <sfunref> to other s-functions have been resolved 9 . Concretely, polynotope objects store (the abstract syntax tree of) vector polynomial functions of typed symbols as sole variables, without any reference <sfunref> to other polynotope objects. <sfunref> references however remain a key enabler to compose non trivial polynotopes (by using intuitive operator overloading) from basic ones, which are typically constructed from <typedsymbol>s as shown at lines 1 and 7 in Table 4. Though an eager evaluation is firstly used to solve <sfunref> tokens only, <typedsymbol> tokens are not immediately evaluated. This makes it possible to delay their evaluation while keeping trace of global dependencies between polynotope objects since each typed symbol is encoded through a unique identifier. By tagging the symbol identifiers with their type, not only the symbols evaluation can be delayed (lazy evaluation) but also adapted to their type (polymorphism). As a result, polynotopes permit some kind of polymorphic delayed evaluation of uncertain symbols/variables. Moreover, a global scope is preserved for the latter, which is the basic key to address the dependency problem arising from a direct use of interval arithmetic. The interplay between mathematical definitions and the semantics attached to the intermediate (polynotope objects) and finally computed values (e.g. zonotopes, intervals) also requires a special attention to ensure inclusion is preserved, not only on continuous domains, but also on discrete and mixed ones, as is made possible with polynotopes.

s-functions

In order to transform and evaluate expressions based on typed symbols, the notion of (polynotopic) symbolic function or, shortly, s-function, is precised. s-function definitions (sfd), some of their interpretations (sffi) and related evaluations (sffe) are then considered. Whereas sfd refers to syntax, sffi and sffe refer to semantics. Let F denote the set of finite length well-formed formulas (wff) corresponding to canonical polynotopic symbolic functions as described by <sfundef> in paragraph 3.4 and, more specifically, in footnote 9. Let f ∈ F be such a wff. Firstly, f describes a possibly scalar polynomial vector (see lines 20 and 22 in table 3) of finite dimension n f ∈ N. Also, f contains a finite number p f ∈ N of typed symbols (<typedsymbol> tokens). Let I = I f ⊂ N be the set10 of their unique identifiers. Then, to emphasize its dependence on the typed symbols in s I , the wff f can be equivalently11 denoted as F (s I ) with f = F (s I ). Definition 11 (s-function: sfd/sffi/sffe) :

• s-function definition (sfd) : f = F (s I ) ∈ F. F (s I ) is a wff involving the (typed) symbolic variables in s I which become bound in the formula: indeed, F (s I ) depends on s I , at least from a syntactical viewpoint.

• s-function functional interpretation (sffi) : denoted as ιf (.) to emphasize its functional nature, an sffi of f is an interpretation ιf of f that has the ability to define and/or return output values from input values corresponding to an interpretation/valuation of the (typed) symbols in s I .

• s-function functional evaluation (sffe) : Let ιs I be an interpretation/valuation of the symbolic vector s I and let ιf (.) be an sffi of f = F (s I ). Then, the sffe ιf (ιs I ) is the result obtained by applying ιs I to the sffi ιf (.).

Remark 12 (sffi vs sffe) An s-function interpretation ιf , as long as it is also an sffi ιf (.), should be understood as a mathematical function or subroutine or algorithm or any transformation process related to f but not as some returned output value obtained from such a function or process. By contrast, an sffe ιf (ιs I ) should be understood as some returned value obtained from an sffi ιf (.) fed by some interpretation/valuation ιs I of the typed symbols s I referring to its (possibly uncertain) inputs. Though out of scope in this work, note that there is no incompatibility with taking functions as possible values, like in functional paradigms. Moreover, random variables being nothing else but functions from a set of outcomes to a set of possible values, the proposed approach is open to extensions involving stochastic descriptions.

An s-function definition (sfd) usually results from the eager evaluation of some program containing s-functions declarations like, e.g., <sfunprog> in Table 3. For polynotopes, this evaluation is based on a systematic expansion leading to a polynomial vector with variables corresponding to typed symbols only, and no more reference to any other s-functions which are all resolved. In other words, the systematic polynomial expansion gives a fully unfolded abstract syntax tree, up to typed symbols i.e. s-function uncertain inputs. For example, based on the sample code in lines 1-4 of Table 4, the following s-function definitions (sfd) are obtained:

f 1 = [0.25+0.5*symb:i+0.25*symb:i 2; 0.5+0.5*symb:i], f 2 = 0.25-0.25*symb:i 2.
Note that the elimination of 0.5*symb:i in the sfd of f 2 is made possible at the symbolic level. This greatly helps to improve the evaluation of some bounds in Table 4.

Several interpretations of an s-function f = F (s I ) may coexist but a basic one is as a mathematical function like

ιf : ιτ s I → R n f , ιs I → ιf (ιs I ), (1)
which is an sffi. It is important to note in (1) that the definition domain ιτ s I of ιf depends on the types τ s I of the typed symbols s I involved in the wff F (s I ) defining the s-function f ∈ F. See also Table 2. Continuing the example, symb:i being of type i (interval), it comes:

ιf 1 : [-1, +1] → R 2 , σ → [0.25 + 0.5σ + 0.25σ 2 ; 0.5 + 0.5σ], ιf 2 : [-1, +1] → R, σ → 0.25 -0.25σ 2 .
An hybrid example mixing continuous and discrete types is also given with a s-function f ∈ F defined as the wff F (s I ) = 1+x:i+4*y:b*z:s. Then, n f = 1 (scalar output), and the p f = 3 involved typed symbols s I1 = x:i, s I2 = y:b, s I3 = z:s are respectively of type i (interval), b (boolean), s (signed). In this example, the symbol names in F (s I ) coincide with those in Table 2. Following ( 1), an sffi of f as a mathematical function is:

ιf : × | 1 0 | × | + -| → R, [x; y; z] → 1 + x + 4yz, and the imset of ιτ s I by ιf is [-4, -2] ∪ [0, 2] ∪ [4, 6]
which is a non-convex and non-connected set. This can be generalized with image-sets.

Image-sets

Set-based rather than functional (sffi) interpretations of s-functions are considered with the image-sets defined in this paragraph. They provide set-based wraps ensuring the consistency between some intended mathematical meaning and the actually computed sets through an inclusion preserving approach. This is obtained by first extending the imsets and inclusion functions in section 2 to a symbolic context with typed symbols through image-sets and inclusion s-functions, respectively. Then, a notion of inclusion preserving symbolic reduction operator is introduced. This gives control to maintain finite representations of prescribed complexity for the underlying approximate polynomial expansions while preserving a set inclusion property ensuring consistency of the computed polynotopic image-sets.

Definition 13 (Image-set) The image-set f ι of the s-function f = F (s I ) ∈ F is the imset of the domain ιτ s I by a functional interpretation ιf of f :

f ι = {ιf (σ) | σ ∈ ιτ s I } = ιf (ιτ s I ).
Remark 14 The domain ιτ s I is a set related to the types of the symbols in s I (see assumption 6 and table 2) and ιf (σ) stands for an sffe as in definition 11.

Definition 15 (Inclusion s-function)

The s-function g = G(s J ) is an inclusion s-function for f = F (s I ) under functional interpretations ιf of f and ιg of g if ιg is an inclusion function for ιf defined on the domain ιτ s I .

Corollary 16 From the definition 2 and its corollary 3, ⊂ ιτ s I being a set of subsets of ιτ s I including ιτ s I itself, ιf (Σ) being the imset of Σ by ιf , and ιg(Σ) being the image of Σ by ιg, it comes:

∀Σ ∈ ⊂ ιτ s I , {ιf (σ) | σ ∈ Σ} = ιf (Σ) ⊂ ιg(Σ), (2) ∀Σ ∈ ⊂ ιτ s I , ιf (Σ) ⊂ ιg(ιτ s I ). ( 3
)
Definition 17 (Reduction) A reduction is an operator ↓ q transforming an s-function f = F (s I ) into an s-function f = ↓ q f = F (sĪ ) such that f is an inclusion s-function for f depending on at most q generator symbols: card( Ī) ≤ q ∈ N and card(.) gives the cardinal.

Remark 18 (Reduction) Ī ∩ I = ∅ is not mandatory but often useful to limit the inclusion conservatism while controlling the complexity of f through its input dimension. In other words, a reduction operator should preserve the more important symbols/dependencies i.e. the ones which significantly contribute to shaping the graph of the mathematical function symbolized by the s-function f .

Example 19 (Inclusion s-function)

In the sample code of Table 4, the step 8 declares the s-function f 5 which is an inclusion s-function for the s-function f 1 (resp. f 3 ) declared at step 3 (resp. step 5). Subsequently, f 6 (step 9) is also an inclusion s-function for f 2 (step 4).

The example 19 illustrates how (vector) polynomial sfunctions like f 1 or f 3 can be rewritten as (vector) linear ones like f 5 while preserving the inclusion property of related set-based interpretations as image-sets. This can even be done automatically by following a general scheme similar to automatic differentiation which makes systematic use of basic operator overloading. Pushing further this idea, the graph of non-polynomial functions, possibly including switching ones, can be enclosed within polynotopes, as it will be further addressed in section 5. This approach contributes to significantly enlarge the class of dynamical systems for which reachability and filtering algorithms (like PKF in section 6) can be readily implemented right from the model equations, just by composing polynotope objects i) through intuitive operator/function overloading and ii) while preserving the efficiency of uncertainty propagation computations possibly involving continuous, discrete or mixed image-sets.

From symbolic zonotopes and mixed encoding to polynotopes

The description of specific data structures and algorithms actually implementing methods related to poly-notope objects was left opened to a large extent in section 3, consistently with the encapsulation principle. Such descriptions are the main subject of this section 4. They are gradually introduced by first dealing with symbolic zonotopes, then mixed encoding, before addressing the more general case of polynotopes.

Affine s-functions and zonotopes

Definition 20 (Affine/linear wff ) The wff F (s I ) is affine in s I if it can be written as c + Rs I where the vector c and the matrix R do not depend on the symbolic variables in s I . In particular, it is linear when c is null or can be omitted i.e. F (s I ) = Rs I . Shortly, Affine wff:

F (s I ) = c + Rs I .
Definition 21 (s-zonotope) A symbolic zonotope (szonotope) f s,τ is an s-function f = F (s I ) such that the wff F (s I ) is affine in the symbolic variables in s I .

Definition 22 (e-zonotope) The e-zonotope related to the s-zonotope f s,τ is the image-set f s,τ,ι of f = f s,τ under an affine interpretation ιf of f . An e-zonotope is thus a set-valued evaluation (semantics) related to a given s-zonotope (syntax).

One possible data structure to store a symbolic zonotope is (c, R, I). The related s-function defined by a wff denoted c, R, I s,τ is f = c + Rs I , and the related ezonotope is in (5):

c, R, I s,τ = c + Rs I (syntax) (4) c, R, I s,τ,ι = {c + Rσ | σ ∈ ιτ s I } (semantics) (5)
The main differences with classical zonotopes defined as

c, R = {c + Rs | s ∈ [-1, +1] n } are twofold:
Firstly, the interplay between syntax and semantics is not caught by the classical definition, whereas it plays a key role in the management of the so-called dependency problem. For example, assuming an entirely continuous case i.e. all the symbols s i are of type (unit) interval, let us consider the sum S (resp. Minkowski sum S ι ) of the szonotopes 0, 1, 1 s,τ and 0, -1, 1 s,τ (resp. 0, 1, 1 s,τ,ι and 0, -1, 1 s,τ,ι ). Then, S = 0 + s 1 -s 1 = 0 (resp.

S ι = + = 2 = [-2, +2]
), and the set-valued interpretation ιS = {0} of S is much less conservative than S ι = [-2, +2] while preserving the inclusion property under the considered semantics. Indeed, some uncertainty cancellation has been made possible by formal/symbolic transformations respecting operators syntactic rules, whereas this is no more possible through the Minkowski sum following a set-valued evaluation. One strategy to improve accuracy thus consists in delaying such set-valued evaluations. Moreover, whereas ∀i ∈ N, 0, 1, i s,τ,ι = 0, 1 = [-1; +1], 0, 1, i s,τ = s i is distinct from 0, 1, j s,τ = s j as long as i = j.

From a computational perspective, Matrices with Labelled Columns (MLC) featuring a column-wise sparsity as first introduced in [START_REF] Combastel | A distributed Kalman filter with symbolic zonotopes and unique symbols provider for robust state estimation in CPS[END_REF] lead to efficient implementations of s-zonotope operators such as sum, linear image, interval/box hull, etc. The reader is referred to [START_REF] Combastel | A distributed Kalman filter with symbolic zonotopes and unique symbols provider for robust state estimation in CPS[END_REF] for a detailed description, especially in the sections 4 "Matrices with Labeled Columns (MLC)" and 6 "Symbolic zonotopes". Notice that the definition of symbolic zonotopes in [START_REF] Combastel | A distributed Kalman filter with symbolic zonotopes and unique symbols provider for robust state estimation in CPS[END_REF] only considers one type of symbols interpreted as random variables with support in the unit interval [-1, +1]. This outlines how the approach described in section 3 can also be used in a stochastic paradigm: Indeed, it suffices to consider other types of symbols interpreted as random variables (which are themselves functions, so emphasizing the relevance of cross-connections with functional paradigms). In order to give a flavor about MLC, an informal definition and a sum example are provided. An MLC M |I is a pair (M, I T ) where M is an n × p matrix and I ∈ N p is a vector such that each scalar I j for j = 1, . . . , p, uniquely identifies the jth column M :,j of M . Shortly, the column of M |I labeled as I j refers to M :,j . An example illustrating the sum of two MLC,

M |I + N |J = P |K is:     2 1 5 1 0 1 0 1 1     +     3 5 2 8 2 0 4 6 0 3 5 7     =     1 2 5 3 8 0 5 1 2 6 1 5 4 0 7     . (6)
  0 5 1 2 6 1 5 4 0 7            s1 s2 s5 s3 s8          =   1 0 1 0 1 1       s2 s1 s5     +   2 0 4 6 0 3 5 7          s3 s5 s2 s8        (7)
As shown in [START_REF] Combastel | Zonotopes and Kalman observers: Gain optimality under distinct uncertainty paradigms and robust convergence[END_REF], an equal number of columns/generators of the operands is not mandatory, and the labels are reported on the first lines (e.g. I T = [2, 1, 5]). ( 7) illustrates the column-wise (not row-wise) sparsity granted by MLC operators, and that the sum of two MLC gives the exact sum of two centered s-zonotopes since 0, P, K s,τ = 0, M, I s,τ + 0, N, J s,τ . Indeed, Secondly, another main difference with classical zonotopes is the introduction of symbol typing. This makes it possible to combine several kinds of interpretations. Following the assumption 6, this paper mainly focuses on mixed, continuous and discrete values in a setmembership paradigm, though the approach described in section 3 is more general. For example, let us consider five symbols s i , i = 1, . . . , 5, such that s 1 , s 2 , s 3 are of type s (signed) i.e. s 1 , s 2 , s 3 take their values

M |I + N |J = P |K ⇒ M s I + N s J = P s K . K ⊂ I ∪ J
= [R 1 , R 2 ] of ιτ s I = [{-1, +1} 3 ; [-1; +1] 2 ].
It is also the Minkowski sum of the (discrete) ezonotope 0, R 1 , I 1 s,τ,ι and the (continuous) e-zonotope 0, R 2 , I 2 s,τ,ι . The resulting set is neither convex nor connected, as shown in Fig. 1, where the dashed line is the border of the classical (continuous) zonotope 0, R . This example illustrates that mixed zonotopes can provide a very compact representation (Fig. 1: R ∈ R 2×5 and 5 bits encoding the symbol types) for the union of a same13 (continuous) zonotopic shape centered on each point of a discrete set possibly containing a high number of configurations (Fig. 1:

2 3 = 8 = cardinal of {-1, +1} 3 ).

Mixed encoding

The notion of mixed encoding is introduced in the same spirit as the example illustrated in Fig. 1. It also provides an approach for a hierarchical modeling of dependencies making it possible to tune the granularity level of the description. Notation: Let i (resp. | + -| i , | 1 0 | i ) denote the symbol s i provided it is of type interval (resp. signed, boolean) i.e. τ s i = i (resp. s, b). Under the assumption 6, a compact notation for typed symbols is so obtained, each being uniquely identified by i. Also, let n+1) . By induction, the row sum of ρ(n) is 1.

ρ(0) = 1, ρ(n + 1) = 1 2 [1, ρ(n)] for n ∈ N. Then, ∀n, ρ(n) = [( 1 2 ) 1 , . . . , ( 1 2 ) n , ( 1 2 ) n ] ∈ R 1×(

Definition 23 (Mixed encoding of basic intervals)

The s-zonotope Z n s (I) is an n-level signed-interval mixed encoding of the unit interval

[-1, +1] if Z n s (I) = 0, ρ(n), I s,τ = ( n j=1 ( 1 2 ) j | + -| Ij )+( 1 2 ) n In+1 . The s-zonotope Z n b (I) is an n-level boolean-interval mixed encoding of the interval [0, 1] if Z n b (I) = 0, ρ(n), I s,τ = ( n j=1 ( 1 2 ) j | 1 0 | Ij )+( 1 2 ) n In+1 .
Corollary 24 (Mixed encoding of intervals) Let Z n s (I) be a mixed encoding of

[-1, +1]. Then, c + rZ n s (I) is a mixed encoding of c ± r = [c -r, c + r]. Let Z n b (I) be a mixed encoding of [0, 1]. Then, a + (b - a)Z n b (I) is a mixed encoding of [a, b].
Corollary 25 (Related e-zonotopes) Following the definition 23, the e-zonotope related to the s-zonotope

Z n s (I) (resp. Z n b (I)) is [-1, +1] (resp. [0, 1]).
Conversely, there is no unique mixed encoding for a given interval. The e-zonotope (c + rZ n s (I)) ι related to the s-zonotope c + rZ n s (I) satisfies (c + rZ n s (I)) ι ⊆ (c ± r) (interval hull). The equality holds in the scalar case or for r = 0.

The surjective nature of mixed encoding gives freedom degrees to model dependencies in a hierarchical way. The discrete parts feature close analogies with the usual binary encoding of integers. Moreover, the coverage of continuous domains is achieved through remainder terms. The width of the set-valued interpretation of these terms is related to the granularity of the mixed-encoding. It can be refined or reduced by adapting the level value n. Since affine s-functions and zonotopes essentially provide operators managing affine dependencies only, and since this yields some restrictions on the possible uses of mixed encoding (among others: see, e.g., footnote 13), an extension to polynomial dependencies is considered.

Polynomial s-functions and polynotopes

Let ( , ) denote a generic matrix product: M ( , )N = p j=1 (M ij N jk ), where p both refers to the number of columns of M and the number of rows of N . For example, M N = M (+, .)N is the classical matrix product. +, ., ^respectively denote sum, product, power.

Definition 26 (Monomial matrix notation) The monomial matrix θ E is (θ T (., ^)E) T , where θ (resp. E) is a so-called variable matrix (resp. exponent matrix) of dimension compatible with the generic matrix product (., ^). The operator T refers to transposition.

Examples: Taking θ = [s 1 ; s 2 ] and E = [1, 0, 2; 0, [START_REF] Althoff | Reachability analysis of nonlinear differential-algebraic systems[END_REF][START_REF] Combastel | A state bounding observer based on zonotopes[END_REF] yields θ E = [s 1 ; s 3 2 ; s 2 1 s 4 2 ]. θ I = θ with I = identity.

Definition 27 (Polynomial wff ) The wff F (s I ) is polynomial in s I if it can be written as c + Rs E I where the vector c and the matrices R and E do not depend on the symbolic variables in s I . Shortly, Polynomial wff:

F (s I ) = c + Rs E I .
Then, c, R, s I , E, s E I are respectively the so-called constant vector, coefficient/generator matrix, symbol(ic variable) vector, exponent matrix, monomial vector. Definition 28 (s-polynotope) A symbolic polynotope (s-polynotope) f s,τ is an s-function f = F (s I ) such that the wff F (s I ) is polynomial in the symbolic variables in s I .

Definition 29 (e-polynotope) The e-polynotope related to the s-polynotope f s,τ is the image-set f s,τ,ι of f = f s,τ under a polynomial interpretation ιf of f . An e-polynotope is thus a set-valued evaluation (semantics) related to a given s-polynotope (syntax).

The name polynotope introduced in this work originates from a contraction of polynomial and zonotope. Following [START_REF] Kochdumper | Representation of polytopes as polynomial zonotopes[END_REF], it is also willingly close to polytope. So, polynotope gathers, at least partially, the Greek roots of polynomial (from polus:numerous and nomos:division) and polytope (from polus and topos:location). Under the assumption 6, polynotopes are to sparse polynomial zonotopes what mixed zonotopes are to zonotopes. They can also be viewed as constrained polynomial zonotopes with polynomial constraints managed through a possibly extensible set of symbol types.

One possible data structure to store a symbolic polynotope is (c, R, I, E). The related s-function defined by a wff denoted c, R, I, E s,τ is f = (I, c + Rs E I ), and the related e-polynotope is in (9):

c, R, I, E s,τ = c + Rs E I (syntax) (8) c, R, I, E s,τ,ι = {c + Rσ E | σ ∈ ιτ s I } (semantics) (9)
Polynotopes as in ( 8)-( 9) generalize zonotopes as in (4)- [START_REF] Combastel | A state bounding observer for uncertain non-linear continuous-time systems based on zonotopes[END_REF]. Indeed, zonotopes are obtained for E = I (identity matrix) which is highly sparse and can thus be stored very efficiently. Using a sparse E with integer entries in N leads to a data structure similar to sparse polynomial zonotopes (spz) in [START_REF] Kochdumper | Sparse polynomial zonotopes: A novel set representation for reachability analysis[END_REF], where no typing of symbols is considered (continuous case only). The sparsity of E extends the column-wise sparsity of MLC to polynomial (rather than affine) dependencies with a compact description of monomials featuring (almost) no restriction on the highest degree. The example ( 10)-( 11) shows how the s-polynotope related to (11) can be compactly encoded using (c, R, I, E) as in [START_REF] Thach | On fixed-time interval estimation of discretetime nonlinear time-varying systems with disturbances[END_REF]. See also Fig. 2.

  I E c R   =        1 1 0 1 8 0 3 1 2 5 3 -1 1 2 0 4        , ( 10
)
s 1 s 8 → 2 + 5s 1 + 3s 3 8 -s 1 s 8 1 + 2s 1 + 4s 1 s 8 . ( 11
)
The implementation of continuous polynotopes operations used in this work is close to the one described in [START_REF] Kochdumper | Sparse polynomial zonotopes: A novel set representation for reachability analysis[END_REF] for spz. In particular, each time monomial redundancies might occur, they are removed by summing the related generators: all the columns of E remain distinct. The main differences are:

1) The case of independent generators is not treated separately i.e. all the generators are possibly dependent (provided they share some common symbol),

2) The implementation of a symbolic addition is considered and optimized by taking into account the fact that monomials/generators involving at least one own variable from an operand can be simply copied in the result since no similar monomial exists in the other operand, 3) A vertical concatenation extends the one of MLC, 4) An element-wise product is used as a special case of quadratic map and the reduction extends the one in [START_REF] Combastel | A distributed Kalman filter with symbolic zonotopes and unique symbols provider for robust state estimation in CPS[END_REF].

Our implementation of polynotopes also supports discrete and mixed operations through symbol typing as described in section 3 and assumption 6. Compared to a strictly continuous case as in [START_REF] Kochdumper | Sparse polynomial zonotopes: A novel set representation for reachability analysis[END_REF], the main difference is the introduction of rewriting rules taking the specific nature of signed and boolean symbols into account. Related substitutions (→) are implemented very efficiently using the (c, R, I, E) attributes with sparse E, e.g.

(| + -| i ) n → (| + -| i ) mod(n,2) , (12)
(| 1 0 | i ) n → (| 1 0 | i ) max(n,1) . ( 13
)
Definition 30 (Rewriting rules and inclusion) A rewriting rule is inclusion preserving if:

( f s,τ → g s,τ ) ⇒ ( f s,τ,ι ⊆ g s,τ,ι ).

It is inclusion neutral if:

( f s,τ → g s,τ ) ⇒ ( f s,τ,ι = g s,τ,ι ).

Proposition 31

The rewriting rules in ( 12) and ( 13) are inclusion neutral under the assumption 6.

Notice the syntactical (resp. semantic) nature of the premises (resp. conclusions) of the implications (⇒) in the definition 30. To give insight into the proposition 31, let x be a possible value of any signed symbol: x ∈ {-1, +1} ⊂ R. Thus, (x + 1)(x -1) = 0 i.e. x 2 = 1 as polynomial constraint. By induction, x n = x for odd n, x n = 1 for even n, that is x n = x mod(n,2) which shows the inclusion neutrality of ( 12). Similarly, let x be a possible value of any boolean symbol: x ∈ {0, 1} ⊂ R. Thus, (x -0)(x -1) = 0 i.e. x 2 = x. By induction, 1) which shows the inclusion neutrality of ( 13).

x n = x if n > 1, x n = 1 if n = 0, that is x n = x max(n,
The rewriting rules ( 12)-( 13) apply for operations modifying the monomial degrees like product; the number of distinct monomials induced by discrete operations is drastically reduced compared to continuous ones, since the exponent in the right term of ( 12)-( 13) is either 0 or 1 instead of any n ∈ N. Thanks to inclusion neutrality, such simplifications of formal expressions induce no conservatism in the related set-valued interpretations.

Other rewriting rules are only inclusion preserving:

Proposition 32 The rewriting rules in ( 14), ( 15) and ( 16) are inclusion preserving under the assumption 6.

(| 1 0 | i ) → 1/2 + (| + -| j )/2, ( 14
) (| + -| i ) → ( j ), ( 15
) ( i ) 2 → 1/2 + ( j )/2, ( i )( j ) → ( k ). (16)
(14)-( 16) apply before computing the zonotope/interval enclosure of a (possibly mixed) polynotope. Notice that ( 14) is inclusion neutral if applied globally i.e. without generating new symbol multi-occurrences. ( 15) is the formal/syntactical counterpart of {-1, +1} ⊂ [-1, +1] which can be viewed as a prototype of the most basic inclusion of two discrete modes/configurations (-1 and +1) into a single continuous domain (the unit interval). By using appropriate reductions of formal expressions based on inclusion preserving rewriting rules, mixed polynotopes provide a highly versatile, scalable and computationally efficient approach to combine and enclose possibly non convex and non connected sets under dependency constraints. Hence, they look appealing to deal with verification and synthesis of Cyber-Physical Systems (CPS) whose modeling often relies on mixed/hybrid dynamics. They also exemplify the generality of the approach of image sets with typed symbols described in section 3.

5 Modeling tools for nonlinear hybrid systems

Discrete: Signed and Boolean logic functions

This paragraph shows how signed (resp. boolean) symbolic variables can be used in a polynomial framework, like the one of polynotopes under the assumption 6, to express any propositional logic formula where symbolic variables are interpreted on a bi-valued real domain:

| + -| = {-1, +1} ⊂ R (resp. | 1 0 | = {0, 1} ⊂ R).
This gives a natural interface between continuous variables (defined on a (real) domain with infinite cardinal) and discrete ones (defined on a (real) domain with finite cardinal).

Proposition 33 (Multi-affine decomposition) Let f : R p → R n be any function between finite dimensional real domains. Let x ∈ R and z ∈ R p-1 so that (x, z) ∈ R p refers to any input vector of f where a scalar input x is distinguished from the others. Let introduce four partial functions of f defined as:

f A x (z) = f (+1,z)+f (-1,z) 2 : Average of f wrt x, f H x (z) = f (+1,z)-f (-1,z) 2 : Half-gap of f wrt x, f G x (z) = f (0, z) : Ground of f wrt x, f U x (z) = f (1, z) -f (0, z) :
Unit-gap of f wrt x, Then, an affine decomposition of f wrt x under a signed (resp. boolean) x is respectively given by ( 17) and [START_REF] Jaulin | Applied interval analysis[END_REF]. Moreover, if all the scalar entries of z are signed (resp. boolean), a recursive application of (17) (resp. ( 18)) results in a (polynomial) multi-affine decomposition of f .

x ∈ {-1, +1} ⇒ f (x, z) = f A x (z) + xf H x (z), (17)
x

∈ {-0, +1} ⇒ f (x, z) = f G x (z) + xf U x (z). ( 18
)
Proof. (17

) comes from f (+1, z) = f A x (z) + f H x (z) and f (-1, z) = f A x (z) -f H x (z). Similarly, (18) comes from f (0, z) = f G x (z) and f (1, z) = f G x (z) + f U x (z)
. The multi-affine decomposition of basic propositional logic operators is reported in Table 5 both in the signed and boolean cases. At least three noticeable facts emerge from Table 5: a) The equivalence eqv in the signed case features the same multi-affine decomposition as the logical and in the boolean case, and both reduce to a simple product. b) The multi-affine decompositions with signed operands look more "balanced" in terms of involved monomials, compared to the boolean case. This is visible right from the basic affine decompositions in [START_REF] Immler | ARCH-COMP18 cat. report: Cont. and hybrid sys. with nonlinear[END_REF] and [START_REF] Jaulin | Applied interval analysis[END_REF]. Indeed, the average of both alternatives (resp. the 0 alternative) serve as reference to express the impact of a switching controlled by x in the signed (resp. boolean) case. c) Interpreting in R the polynomial expression of a multi-affine decomposition yields some interpolation between discrete configurations initially expressed in a (bi-valued) propositional logic framework. Theorem 35 (Functional completeness) Under the assumption 6, let I ⊂ N be a finite set of unique symbol identifiers with at least p elements of type signed (resp. boolean). s-polynotopes based on wff interpreted as multivariate polynomials R[s I ] with coefficients in the real field (R, +, .) can describe any function f :

a + b -ab nand ↑, +1-a-b-ab 2 1 -ab nor ↓, -1-a-b+ab 2 1 -a -b + ab imp ⇒, ≤ +1-a+b+ab 2 1 -a + ab eqv ⇔, = +ab 1 -a -b + 2ab xor , = -ab 0 + a + b -2ab pow a n , n ∈ N a mod(n,2) a max(n,1)
| + -| p → | + -| (resp. f : | 1 0 | p → | 1 0 |), where | + -| = {-1, +1} ⊂ R (resp. | 1 0 | = {0, 1} ⊂ R).
Proof. Theorem 35 follows from the functional completeness of the nand (or nor) logical operator and the fact that the composition of polynomials in R[s I ] result in polynomials in R[s I ]. Indeed, the nand operator is defined as a polynomial function with signed (resp. boolean) operands and codomain in Table 5. Thus, the composition of any number of such nand operations on signed (resp. boolean) symbolic variables evaluated in | + -| (resp. | 1 0 |) result in a polynomial s-function i.e. a spolynotope according to the definition 28.

Corollary 36 Given any pair (a, b) ∈ R 2 satisfying a < b, all the finite dimensional Boolean functions and operations can be plunged in {a, b} p ⊂ R p for some p ∈ N after suitable re-scaling compared to the usual Boolean case i.e. (a, b) = (0, 1). This is exemplified with the so-called signed case i.e. (a, b) = (-1, +1) in table 5, where the direct and inverse affine re-scaling functions are r :

| + -| → | 1 0 |, x → 1+x 2 and r -1 : | 1 0 | → | + -|, x → 2x -1.

Continuous: Nonlinear functions

Whereas the imset (see definition 1) of a polynotope (resp. zonotope) by a polynomial (resp. affine) function is still a polynotope (resp. zonotope), the imset by non-polynomial (resp. non-linear) functions is not. This paragraph proposes a method to obtain guaranteed inclusions of non-polynomial (resp. non-linear) functions while maintaining dependency links between inputs and outputs. Indeed, breaking such links (e.g. by a naive use of interval arithmetic) is often the source of overapproximations and/or wrapping effect.

For the sake of simplified notations, the distinction be-

Given an interval

[x] ⊂ R, let f : [x] → R, x → y = f (x)
be a function that does not satisfy a property π (i.e. ¬π(f ) is true) required for a given class of image-sets to be closed under the (element-wise) application of f to the underlying s-functions. For example: π being the property of being linear (resp. polynomial), the class of e-zonotopes (resp. e-polytopes) are closed under the application of linear (resp. polynomial) functions to the underlying s-zonotopes (resp. s-polytopes). ¬π(f ) then means that f is non-linear (resp. non-polynomial) for zonotopes (resp. polynotopes). The considered structural property π is assumed to be preserved through function composition.

Lemma 38 (Generic inclusion method) Given an interval

[x] ⊂ R and f : [x] → R, x → y = f (x) with ¬π(f ). Let g : 2 → R, (δ, ) → g(δ, ) be a function satisfying ∀x ∈ [x], ∃ ∈ , f (x) = g(µ(x),
), where µ is the unit range mapping of [x]. Then, f (.) = g(µ(.), ) is an inclusion function for f (.). Also, π(g) ∧ π(µ) ⇒ π( f ). According to Lemma 38, enclosing a non-linear (resp. non-polynomial) function f in a linear (resp. polynomial) framework can be achieved by finding an adequate linear (resp. polynomial) function g. In order to exemplify the generic inclusion method, a more focused approach is proposed for increasing/decreasing and convex/concave functions f on some interval [x]. Notation:

[∂ x f ](.) = ∂f (x) ∂x x=. . Theorem 39 (An inclusion method) Let f : [x] → R, x → y = f (x) be a class C 1 convex or concave function on a given interval [x] = x ± x = [x, x] ⊂ R with x > 0. Let y = f (x), y = f (x), ŷ = (y + y)/2, ẙ = (y -y)/2. Let δ = µ(x) where µ is the unit range mapping of [x] (so, x ∈ [x] ⇔ δ ∈ ). Let r(δ) = f (x + xδ) -(ŷ + ẙδ). Let δ * be the solution of [∂ x f ](x + xδ) = ẙ/x. Then, g(δ, ) = g 0 +g 1 δ +g 2 with g 0 = ŷ + 1 2 r(δ * ), g 1 = ẙ, g 2 = 1 2 |r(δ * )| satisfies ∀x ∈ [x], ∃ ∈ , f (x) = g(µ(x), ). f (.) = g(µ(.), ) is an inclusion function for f (.) on [x].
Proof. The regularity of f on

[x] ensures that [∂ δ r](δ * ) = 0 i.e. [∂ x f ](x + xδ * ) = ẙ/x has a unique solution. Since r(-1) = r(+1) = 0, if f is convex (resp. concave) on [x], then r(δ) ∈ [r(δ * ), 0] (resp. r(δ) ∈ [0, r(δ * )]
) for δ ∈ . The two cases are gathered as:

r(δ) ∈ 1 2 r(δ * ) ± 1 2 |r(δ * )| Thus, ∃ ∈ , r(δ) = f (x)-(ŷ+ẙδ) = 1 2 r(δ * )+ 1 2 |r(δ * )| , as x =
x+xδ by definition of µ as in Lemma 37. Then, g(δ, ) and the proof follow from the last equality.

Corollary 40

The s-function [µ -1 (δ); g(δ, )] where δ and refer to symbols of type (unit) interval is a continuous s-zonotope since µ -1 and g are affine. ∀x ∈ [x], [x; f (x)] ∈ [µ -1 (δ); g(δ, )] s,τ,ι , an e-zonotope usually not reduced to an aligned box due to the dependency of both dimensions on common symbol(s) referred as δ. Moreover, if x is a polynotope, so is [µ -1 (δ); g(δ, )] s,τ .

An illustrative example with f (x) = e x is reported in Fig. 3 and further remarks are reported hereafter: a) The inclusion proposed in theorem 39 is entirely parameterized by the input domain [x] while not being sub-

(= y + pos(x -y)) Minimum min(x, y) = x+y 2 -|x-y| 2 (= x -pos(x -y)) Saturation sat(x, x, x) = 1 2 (x + x + |x -x| -|x -x|) Deadzone dz(x, x, x) = x -sat(x, x, x) ReLU * pos(x) = max(0, x) = x+|x| 2 * Rectifier Linear Unit (remark: |x| = 2pos(x) -x).
ject to the arbitrary choice of a point used as reference for linearizing or computing a Taylor expansion. b) δ * often has an explicit form, e.g., x +xδ * = log(ẙ/x), x/ẙ, 1 4 (x/ẙ) 2 for f (x) = e x , log(x), √ x, respectively. c) If x = 0, then the input is a point value and f (x) = f (x). This is consistent with the limit x → 0 since the continuity of f gives ẙ → 0, g 0 → ŷ, g 1 → 0 and g 2 → 0. d) If f is decreasing, then y < y and ẙ < 0 in theorem 39. e) r(δ) is the remainder term wrt to a (linear) approximation of f (x) which itself (linearly) depends on x: ŷ + ẙµ(x). The purpose of a dependency-preserving inclusion (dpi) is thus achieved, at least for a structural property π referring to being linear. Note that polynomial dependencies possibly modeling x (then, x(.) and δ(.) = µ(x(.)) are polynomials) are readily propagated by a linear enclosing approximation f (.) of f (.). Indeed, the composition of affine and polynomial functions is still polynomial. Thus, the result in theorem 39 is readily applicable with polynotopes. Moreover, the generic inclusion method in Lemma 38 encompasses polynomial enclosing approximations of non-polynomial functions.

Hybrid: Switching functions

In the last paragraph ( §5.2), an inclusion method for functions f satisfying the regularity conditions of being C 1 has been proposed in Theorem 39. Following the generic inclusion method stated in Lemma 38, the case of a prototypical C 0 but not C 1 function is considered in this paragraph: the absolute value. The motivation for this is summarized in Table 6 which shows that several useful switching functions can be built by composing basic operators (like +, -, taking the half) with the absolute value operator abs(x) = |x|. Thus, a dependencypreserving inclusion of a prototypical switching function like abs is highly desirable to model and efficiently propagate uncertainties within hybrid dynamical systems, without necessarily requiring costly bisections and/or a specific management of guard conditions.

abs(.) = x x (.) + x2 -x2 2x (1 + ). ( 19
)
Proof. If 0 ∈ [x] (case 1 or 2), abs(.) is linear and no dedicated inclusion is then required. If 0 ∈ [x] (case 3), the inclusion method of theorem 39 is applied stepby-step: Let µ be the unit range mapping of [x] and δ = µ(x). Since abs(.) is only C 0 and convex on [x], but not C 1 , the range of the remainder r(δ) ≤ 0 (still such that r(-1) = r(+1) = 0) is computed by noticing that its minimum is obtained for

x = x + xδ * = 0. Then, δ * = -x/x gives r(δ * ) = (x 2 -x 2 )/x and satisfies ∀δ ∈ , r(δ) ∈ [r(δ * ), 0]. It comes g(δ, ) = g 0 +g 1 δ +g 2 with g 0 = x2 +x 2 2x , g 1 = x, g 2 = x2 -x 2 2x (|x| < x in case 3). Finally, g(µ(x), ) = ( x x )x + ( x2 -x 2 2x
)(1 + ). Corollary 40 still applies to f = abs, as a corollary of theorem 41 rather than theorem 39. A dependencypreserving inclusion of abs(.) has been obtained. By extension, dependency-preserving inclusions (dpi) for the switching functions reported in table 6, among others possibly resulting from functional compositions are also obtained. Moreover, the vertical concatenation operator implemented for zonotopes and polynotopes allows to build n-dimensional dpi from scalar ones through basic compositions. These can be implemented by using the overloading capability of some object oriented languages, to the benefit of code readability. This feature holds not only for switching functions, but also for non-linear/non-polynomial ones. This makes polynotopes a relevant tool to compute and analyze mixed uncertainty propagation within non-linear hybrid dynamical systems. Indeed, their polynomial nature, efficiently encoded by combining full and sparse data structures, looks appropriate to model a wide spectrum of nontrivial dependencies, as shown by the functional completeness result given in theorem 35.

Polynotopic Kalman Filter (PKF)

An extension of Kalman Filtering to discrete-time nonlinear hybrid dynamical systems is proposed in this section. It is based on polynotopes and interpretations related to a set-membership uncertainty paradigm. Let x(s) be a s-polynotope (8): x(s) = c, R, I, E s,τ = c + Rs E I (syntax). By analogy with zonotopes, its covariation [START_REF] Combastel | Zonotopes and Kalman observers: Gain optimality under distinct uncertainty paradigms and robust convergence[END_REF] is defined as: cov(x(s)) = RR T . In order to possibly take symbol types and/or the monomial structure into account 15 , a covariation weighted by Φ (pos-sibly Φ(I, E) or any Φ(.) depending on known values) is introduced as: Definition 42 (Weighted covariation) Given a symmetric matrix Φ (Φ = Φ T ), the weighted covariation of x = c, R, . . . s,τ (,ι) (polynotope or zonotope) is:

cov Φ (x) = RΦR T .
x(s) formalizes a vector polynomial (s-)function of the symbolic variables in s I . The execution of polynotope operations like sum, linear image, concatenation, reduction, zonotopic hull Zx(s), interval/box hull Bx(s), etc mainly work at a syntactic level by manipulating polynomial expressions (e.g. encoded as (c, R, I, E) with sparse E) while preserving semantic properties. In particular, inclusion is viewed as a semantic property related to a set-membership interpretation of polynomial functions depending on typed 16 symbolic variables. From ( 9), it comes: ∀σ ∈ ιτ s I , ιx(σ) ∈ Px(s) = c, R, I, E s,τ,ι (semantics), where ιx(.) stands for the interpretation of x(.) as a vector of polynomial mathematical functions (R dim(I) → R nx ) with real coefficients (under assumption 6). Since probability theory is the most commonly used framework for nonlinear filtering, some analogies and exploratory links are briefly outlined as a remark:

Remark 43 A first idea to introduce probability theory in the proposed scheme simply consists in extending the basic symbol types in assumption 6 to other types like (some class of ) random variables defined on a given probability space. This can work in the linear case with symbolic zonotopes and/or independent Gaussian random variables (e.g. see §2.2 and definition 6.1 in [START_REF] Combastel | A distributed Kalman filter with symbolic zonotopes and unique symbols provider for robust state estimation in CPS[END_REF]). Pushing further in such a direction could be an option. Another one may rely on interpreting σ (as in definition 13, ( 5) and ( 9)) as an "outcome", the function ιx(.) as a "random variable", [ιx] -1 (S) as an "event" related to any set S of output values taken by ιx(.). A measure π(.) of events on the domain ιτ s I induced by an interpretation of symbol types would then become some kind of conditional probability wrt ιτ s I . The typed symbols s I would then contribute to define the probability space itself.

In the following, no probability measure is considered. Notations: x = x(s) denotes a s-polynotope.

x = ιx(σ) ∈ R nx denotes a point evaluation of x obtained for some so-called outcome σ ∈ ιτ s I . Then, x ∈ Px, the e-polynotope related to x. Also, x ∈ Zx (resp. x ∈ Bx) means that x belongs to a zonotopic (resp. interval/box) hull of x.

The state observation (or filtering) problem addressed in this section deals with discrete-time non-linear hybrid 16 Notice that the set-membership interpretation is also related to the types considered under the assumption 6.

dynamical systems modeled as:

x + = f (x, u, v), x 0 ∈ Px 0 , v ∈ Pv, (20) 0
= g(x, u, v, y), (21)
where the functions f (.) and g(.) result from the composition of elementary functions and operators for which inclusion preserving polynotope versions are available.

In practice, this is not much restrictive since sum, linear image, reduction, concatenation, product are available (see §4.3) and the modeling tools for nonlinear hybrid systems developed in section 5 can be used to that purpose. Then, by overloading17 these elementary functions and operators with their inclusion preserving polynotopic version, and by applying the same composition, inclusion functions with polynotopic inputs and outputs f (.) and g(.) can be obtained for f (.) and g(.), respectively. In [START_REF] Kochdumper | Representation of polytopes as polynomial zonotopes[END_REF], the index + refers to the next time step k + 1 and the current time step k is omitted to simplify the notations, except for the initial state x 0 at time k = 0. x 0 ∈ R nx is assumed unknown but bounded by the e-polynotope Px 0 related to a known s-polynotope

x 0 . x ∈ R nx , u ∈ R nu , y ∈ R ny , v ∈ R nv respectively
stand for the states, the known (control) inputs, the known measurements, the unknown but bounded uncertainties (state and measurement noises, disturbances, modeling errors, etc) at time k. v is assumed bounded by a known polynotope Pv. Notice that u ∈ Pu = {u} (singleton) for u = u, ∅, ∅, ∅ s,τ . Similarly, y ∈ Py with y = y, ∅, ∅, ∅ s,τ . The problem addressed is that of designing a one step-ahead prediction filter (or state observer) minimizing the trace tr(.) of the (weighted) covariation of a polynotope enclosing the predicted state.

Filtering is mainly a data fusion process. So, how to merge (vector) sources? Weighting is a usual solution:

z 1 ∈ Pz 1 ∧ z 2 ∈ Pz 2 ⇒ z = G 1 z 1 + G 2 z 2 ∈ Pz with z = G 1 z 1 + G 2 z 2 . (22)
Two noticeable ways to particularize [START_REF] Kochdumper | Sparse polynomial zonotopes: A novel set representation for reachability analysis[END_REF] are: 23) which parameterizes enclosures of a polynotope intersection that could be used to design a state bounding observer:

a) Taking z 1 = z 2 under G 1 + G 2 = I gives (
z ∈ (Pz 1 ∩ Pz 2 ) ⇒ z ∈ P(G 1 z 1 + G 2 z 2 ). (23) z ∈ Pz 1 ∧ 0 ∈ Pz 2 ⇒ z ∈ P(z 1 -Gz 2 ). (24)
b) Taking z 2 = 0 and G 1 = I under G 2 = -G gives [START_REF] Kurzhanskiy | Ellipsoidal techniques for reachability analysis of discrete-time linear systems[END_REF] which parameterizes an update (or correction) of an initial knowledge Pz 1 about z with some other depending knowledge, Pz 2 , such as the one obtained through some measurements. [START_REF] Kurzhanskiy | Ellipsoidal techniques for reachability analysis of discrete-time linear systems[END_REF] thus looks as a prototypical weighting underlying the structure of Kalman Filters. Moreover, in our approach, the symbols possibly shared be-

x+ = PKF(x, u, v, y, f , g, Φ, q): x = ↓qx, reduction (25)
p = f (x, u, v), prediction (26)
e = g(x, u, v, y), innovation (27) c,
  Rp Re   , Ȋ, Ȇ s,τ =   p e   , alignment (28)
G = (RpΦR T e )(ReΦR T e ) -1 , optimal gain (29)

x+ = p -Ge. update (30)
tween z 1 and z 2 play a key role in the modeling of dependencies. This makes it possible to tune/optimize G so as to maximize uncertainty cancellation 18 when computing z 1 -Gz 2 . The general idea of Kalman Filters is indeed to optimize the precision of a prediction p = z 1 by using a dependent yet complementary source, the innovation e = z 2 , to update the prediction as p -Ge (30). Then, the algorithm ( 25)-( 30) implementing an iteration of the proposed Polynotopic Kalman Filter (PKF) follows as in Table 7 and theorem 44.

Theorem 44 (PKF: inclusion and optimal gain) Given a system modeled as in ( 20)-( 21), the PKF iteration in ( 25)-( 30) (Table 7) satisfies a) and b):

a) x ∈ Px ∧ v ∈ Pv ⇒ x + ∈ Px + , b) Let G * = arg min G tr(cov Φ (x + )
). G * is the optimal gain computed as in [START_REF] Mirman | Differentiable abstract interpretation for provably robust neural networks[END_REF]:

G * = (R p ΦR T e )(R e ΦR T e ) -1 .
Proof. a) : By construction, f (.) and g(.) are inclusion functions for f (.) and g(.). Since the reduction step ( 25) is inclusion preserving, the inclusion property a) is a direct consequence of (24) with z 1 = p and z 2 = e. : ∂ X h(X) denoting ∂h(X)/∂X, if h(.) returns scalar values and

X = [X ij ] is a matrix, then ∂ X h(X) = [∂ Xji h(X)]. X, A, B, C being matrices of correct size, ∂ X tr(AX T B) = A T B T , (31)
∂ X tr(AXBX T C) = BX T CA + B T X T A T C T . ( 32
)
Let J(G) = tr(cov Φ (x + )). In [START_REF] Meyer | TIRA : Toolbox for interval reachability analysis[END_REF], c = [c p ; c e ] and [p; e] is such that 19 p = c p + R p s Ȇ Ȋ and e = c e + R e s Ȇ Ȋ . From [START_REF] Mitchell | The flexible, extensible and efficient toolbox of level set methods[END_REF], x + = c p -Gc e , R p -GR e , Ȋ, Ȇ s,τ and J(G) = tr((R p -GR e )Φ(R p -GR e ) T ) = tr(R p ΦR T p ) -2tr(R p ΦR T e G T ) + tr(GR e ΦR T e G T ). Using (31) and 18 which is impossible with usual interval arithmetic, subject to the so-called dependency problem. 19 The polynotope concatenation [p; e] gives expressions of p and e such that the generators related to their common monomials (i.e. dependencies) become "aligned" in the same columns of the matrices Rp and Re. This is the reason why ( 28) is called the alignment step. Theorem 45 (PKF vs. ZKF) Let consider the particular case of linear functions f (.) and g(.) defined as: f (x, u, v) = Ax + Bu + Ev p , g(x, u, v, y) = Cx + Du + F v e -y, where v = [v p ; v e ] (state noise and measurement noise), and A, B, C, D, E, F are (possibly time-varying) matrices with appropriate dimensions. Only symbols of type (unit) interval are considered and Φ = I. Also, let f (.) = f (.), g(.) = g(.), x 0 ∈ Px 0 with x 0 = c 0 , R 0 , I 0 , I s,τ (then, Px 0 = Zx 0 is a zonotope), v ∈ Pv with v = 0, I, I v , I s,τ (then, Pv = Zv = Bv is a unit hypercube). It is also assumed that I 0 and all I v 's have no common scalar elements/identifiers which are all unique (then, no symbol being shared between x 0 and all the v's, this is in fact an independence assumption). Then, PKF computes the same centers c (state point estimates) and generator/shape matrices R as ZKF in [START_REF] Combastel | Zonotopes and Kalman observers: Gain optimality under distinct uncertainty paradigms and robust convergence[END_REF] would do, up to column permutations; all the computed polynotopes are also zonotopes, and the optimal gain G = AK corresponds to the usual Kalman gain K = P C T (C P C T + F F T ) -1 with P = R RT .

Proof. Polynotopes (and zonotopes) being closed under linear transforms, taking f (.) = f (.) and g(.) = g(.) suffices to preserve inclusion when ( 20)-( 21) is a discretetime LTV (or LTI) model. Moreover, all the polynotope exponent matrices equaling I, (s-)polynotope operations naturally reduce to (s-)zonotope operations, and the generator matrix computed by the considered reduction operator does not depend on the symbolic description. The focus of the proof is first placed on the observer structure and, then, on the optimal gain. Observer structure: (25): x = c, R, Ī, I s,τ = ↓ q x where c = c, (26): p = Ax + Bu + Ev p , with v p = [I, 0]v, ( 27): e = C x + Du + F v e -y, with v e = [0, I]v, (30): x + = p -Ge gives:

x + = (Ax + Bu + Ev p ) + G(y -(C x + Du + F v e ))
, which corresponds to (( 14)) i.e. the equation ( 14) in [START_REF] Combastel | Zonotopes and Kalman observers: Gain optimality under distinct uncertainty paradigms and robust convergence[END_REF] where (v, w) stands for (v p , v e ). Also, just for insight:

x + = (A -GC)x + (B -GD)u + [E, -GF ]v + Gy.
Keeping in mind that the sum of two generators with the same monomial term (here: with the same symbol) is a classical vector sum, and an horizontal concatenation otherwise (see MLC in §4.1), the centers c * and generator matrices R * of the s-polynotopes (also s-zonotopes since E * = I) computed in [START_REF] Maïga | A comprehensive method for reachability analysis of uncertain nonlinear hybrid systems[END_REF], [START_REF] Makino | Rigorous integration of flows and odes using taylor models[END_REF] and [START_REF] Mitchell | The flexible, extensible and efficient toolbox of level set methods[END_REF] (

): R e = [C R, F ] since Ī ∩ I ve = ∅, ( 27
): c + = c p -Gc e = (A -GC)c + (B -GD)u + Gy, ( 30
): R + = R p -GR e = [(A -GC) R, E, -GF ], 30
since I vp ∩ I ve = ∅, but note that PKF can take dependent state and measurement noises into account with v.

Finally, it can be checked that c + and R + exactly coincide with (( 15)) and (( 16)), respectively, so proving that PKF reduces to the same observer structure as ZKF under the specific assumptions of theorem 45.

Optimal gain: Let P = R RT (= cov Φ (x), Φ = I). Respectively substituting [A R, E, 0] and [C R, 0, F ] for R p and R e in [START_REF] Mirman | Differentiable abstract interpretation for provably robust neural networks[END_REF] gives G = AK with K = P C T (C P C T + F F T ) -1 . Then, it can be checked that the optimal observer gain is the same as in (( 21)) -(( 22)).

Remark 46 (PKF vs. KF) Theorem 45 (PKF vs. ZKF) can be combined with Theorem 7 (ZKF vs. KF) in [START_REF] Combastel | Zonotopes and Kalman observers: Gain optimality under distinct uncertainty paradigms and robust convergence[END_REF] to make a further bridge between set-membership and stochastic paradigms. In particular, this gives the conditions under which PKF covariations and KF covariances coincide, as well as the state point estimates.

Based on modeling tools for nonlinear hybrid systems developed in the proposed approach, a compositional implementation of advanced reachability and filtering algorithms preserving inclusion is made possible by using operator overloading. This is exemplified with the Polynotopic Kalman Filter (PKF) proposed in this section.

7 Numerical Examples

Discrete: Adder

The first example illustrates some connection with basic digital circuit design. The s-polynotopes (i.e. polynomial s-functions) resulting from the multi-affine decomposition of n bits binary adders only made of nand gates are compared depending on the type of symbol(ic variable)s used: signed or boolean as explained in §5.1.

The binary adders architecture is described in Table 8 where S(i) refers to the projection of the s-polynotope S along the ith dimension, i = 1, . . . , n(S). For an n bits adder, A = s 1:n and B = s (n+1):2n each refer to a vector of n (either signed or boolean) symbolic vari- (n) . The number of (distinct) generators/monomials in S, including the center/constant term, is 1 + m(n). This number is reported in Table 9 depending on the number n of bits of the adder and the symbol types: either signed or boolean. An unexpected yet interesting result is obtained: The number of distinct monomials required to describe the full architecture of an n-bits adder is much smaller and more scalable using signed rather than boolean symbols. This example of a full n-bits adder shows the ability of spolynotopes to describe and manipulate purely discrete expressions yielding non trivial relations and dependencies between inputs and outputs. Though requiring further studies, the automatic reduction if such relations could help to struggle against combinatorial explosion by gathering into continuous domains the influence of many bits/signs having a small influence on a given criterion, while keeping trace of how the most significant ones influence that criterion. Moreover, the polynomial representation benefits from useful simplifications made possible by dealing with typed symbols.

S = c, R, Ĩ, Ẽ s,τ with c ∈ R n+1 , R ∈ R (n+1)×m(n) , Ĩ ∈ N 2n+1 , Ẽ ∈ N (2n+1)×m

Continuous: Van-Der-Pol oscillator

In order to illustrate reachability on continuous domains and compare the results with [START_REF] Kochdumper | Sparse polynomial zonotopes: A novel set representation for reachability analysis[END_REF], a Van-Der-Pol oscil- lator taken from [START_REF] Immler | ARCH-COMP18 cat. report: Cont. and hybrid sys. with nonlinear[END_REF] is considered:

ẋ1 = x 2 , ẋ2 = (1 -x 2 1 )x 2 -x 1 .
The initial state set is Px 0 of the final polynotope (at t = 6.8 s) is the green set in Fig. 4. At each iteration, the (polynotopic version of the) reduction operator ↓ q from [START_REF] Combastel | A distributed Kalman filter with symbolic zonotopes and unique symbols provider for robust state estimation in CPS[END_REF] with q = 50 is used to: a) reduce the square x 2 1 , b) reduce the product (x 2 1 )x 2 , c) reduce x. As expected, the reachability result shown in Fig. 4 is close to the one obtained with sparse polynomial zonotopes (spz) in the Figure 6 of [START_REF] Kochdumper | Sparse polynomial zonotopes: A novel set representation for reachability analysis[END_REF], where a comparison with other methods is conducted. Thus, continuous polynotopes also outperform zonotopes and quadratic zonotopes on this example, which illustrates the interest in dealing with polynomial dependencies to propagate continuous domains within nonlinear dynamics.

= P[x 1,0 ; x 2,0 ] = [[1.

Hybrid: Traffic network

In order to illustrate reachability for dynamics defined with switching functions like min (see §5.3 and table 6) and compare the results with those reported for the TIRA toolbox in [START_REF] Meyer | TIRA : Toolbox for interval reachability analysis[END_REF], the model of a 3-link traffic network representing a diverge junction is considered:

ẋ1 = -k(x)/T + p, ẋ2 = k(x)/2 -min(c, vx 2 ), ẋ3 = k(x)/2 -min(c, vx 3 ), where k(x) = min(c, vx 1 , 2w(x -x 2 ), 2w(x -x 3 )).
min(., ., ., .) is implemented as min(min(., .), min(., .)). The state x ∈ R 3 is the vehicle density on each link. p ∈ [4/3, 2] is the constant but uncertain vehicle inflow to link 1. Notice that the constant nature of this uncertainty is naturally handled by the proposed symbolic approach (no new symbol at each time for p).

As in [START_REF] Meyer | TIRA : Toolbox for interval reachability analysis[END_REF], the known parameters of the network are ]. An Euler sampling with step size h = 1 and final time t f = 30 is considered. The reduction x = ↓ q x is applied at each iteration with q = 20. Then, 0.26 s were required to compute the polynotope Px t f reported in cyan in Fig. 5. For the sake of a first comparison, the results in the Figure 2 in [START_REF] Meyer | TIRA : Toolbox for interval reachability analysis[END_REF] are also reported in Fig. 5 : C/GB (Contraction/-Growth Bound), MM (Mixed Monotonicity), SDMM-IA (Sampled Data MM-Interval arithmetic), SDMM-S/F(Sampled Data MM-Sampling/Falsification). Px t f looks competitive wrt to the results obtained with TIRA (red box in Fig. 5). Moreover, the computed polynotope captures the orientation of the "black cloud of sample successors" obtained from 5000 Monte-Carlo simulations and also reported in Fig. 5. This illustrates the ability of the proposed scheme to maintain dependency links while propagating uncertainties through hybrid dynamics modeled with switching functions.

Reachability and Filtering: Lotka-Volterra

A non-linear non-autonomous prey-predator model resulting from the discretization of a modified continuoustime Lotka-Volterra model illustrates a) the computation of reachable sets based on a mixed-encoding ( §4.2) of the initial state set, and b) Polynotopic Kalman Filtering (PKF) as developed in section §6. The modified continuous-time Lotka-Volterra model is ẋ

= f(x, u) with x ∈ R 2 , u ∈ R, (a, b, c, d) = (2, 0.4, 1, 0.1), and f(x, u) = [ax 1 -bx 1 x 2 ; -cx 2 + dx 1 x 2 + u].

Reachability with a mixed-encoding of state sets

A mixed-encoding of the initial state set is first considered and further propagated using mixed polynotope computations within the non-linear dynamics of the discretized Lotka-Volterra model. More precisely, following the definition 23 and the corollary 24, a 3-level signed-interval mixed encoding of the interval 15 ± 1 is taken as polynotopic initial state set for both x 1,0 and x 2,0 (i.e. x 1 and x 2 at t = kh = 0): [START_REF] Goubault | A zonotopic framework for functional abstractions[END_REF][START_REF] Grünbaum | Convex Polytopes[END_REF]; [START_REF] Goubault | A zonotopic framework for functional abstractions[END_REF][START_REF] Grünbaum | Convex Polytopes[END_REF]]. [START_REF] Raïssi | Some recent results on the design and implementation of interval observers for uncertain systems[END_REF] Each occurrence of !(3, s) (resp. !(1, i)) calls USP (see §3.3) which returns 3 (resp. 1) unique identifiers of symbols of type signed (resp. unit interval). Thus, x 1,0 and x 2,0 are independent since they share no common symbol. Note that the symbol types are compatible with the definition 23 of Z g s . g refers to the granularity level of the mixed-encoding. g = 3 means that 3 signed symbols are used to hierarchically decompose the range 15 ± 1 into 2 3 = 8 sub-intervals. The coverage of the continuous domain 15 ± 1 is then ensured by the remainder term modeled by the symbol of type unit interval uniquely identified by !(1, i). For instance, let I = [!(3, s); !(1, i)] and x 1,0 = 15 + 1.Z 3 s (I) as in [START_REF] Pourasghar | A zonotopic Kalman filter optimizing fault detection rather than state estimation[END_REF]. Then,

x 1,0 = 15 + 1.Z 3 s ([!(3, s); !(1, i)]), (33)
x 2,0 = 15 + 1.Z 3 s ([!(3, s); !(1, i)]), ( 34
) Px 0 = P[x 1,0 ; x 2,0 ] = [
x 1,0 = 15, [ 1 2 , 1 4 , 1 8 , 1 8 ], I, 1 s,τ = 1 2 s I1 + 1 4 s I2 + 1 8 s I3 + 1 8 s I4
, where the 3 symbols s I1:3 are of type signed i.e. ιs I1:3 ∈ {-1, +1} 3 and the symbol s I4 is of type (unit) interval i.e. ιs I4 ∈ [-1, +1], so that x 1,0 also writes as:

x 1,0 = 1 2 | + -| I1 + 1 4 | + -| I2 + 1 8 | + -| I3 + 1 8 I4 . (36)
x

2,0 = 1 2 | + -| J1 + 1 4 | + -| J2 + 1 8 | + -| J3 + 1 8 J4 . (37)
x 2,0 is obtained analogously from J = [!(3, s); !(1, i)] (I ∩ J = ∅) and x 2,0 = 15 + 1.Z 3 s (I) as in [START_REF] Puig | Worst-case simulation of discrete linear time-invariant interval dynamic systems[END_REF]. The e-polynotope (or e-zonotope) related to the spolynotope x 1,0 (or s-zonotope since E = I) is thus Px 1,0 = Zx 1,0 = 15 ± 1 (corollary 25). The independence of x 1,0 and x 2,0 coming from I ∩ J = ∅ gives [START_REF] Raïssi | Some recent results on the design and implementation of interval observers for uncertain systems[END_REF]. The polynotope x 0 = [x 1,0 ; x 2,0 ] contains all the information required to decompose the initial state set [ [START_REF] Goubault | A zonotopic framework for functional abstractions[END_REF][START_REF] Grünbaum | Convex Polytopes[END_REF]; [START_REF] Goubault | A zonotopic framework for functional abstractions[END_REF][START_REF] Grünbaum | Convex Polytopes[END_REF]] into a paving as in Fig. 6 for k = 0. Moreover, assigning values +1 or -1 to evaluate some of (or all) the signed symbols in ( 36)-( 37) makes it possible to query about the range covered under some conditional values of signed symbols. This feature makes it possible to trace how each cell and/or cell groups within the "implicit paving" of the initial state set will propagate. It is worth underlining that this can be achieved without any bissection, only through the polynomial computations implementing the basic polynotope operators.

For the sake of illustration, an Euler sampling of the Lotka-Volterra model is considered: x + = x + f(x, 0)h, where the time index k is omitted, x + stands for x k+1 , Fig. 6. Reachable sets resulting from a 3-level signed-interval mixed encoding of the initial states of a Lotka-Volterra model. The mixed polynotope computed at each time k characterizes (overlapping) outer approximations of the propagation of each of the 64 cells (red) paving the initial state set with no bissection. This also works with cell groups (green).

and the step size is h = 0.15 s. The reduction operator ↓ 50 is applied at each iteration. The reachability analysis reported in Fig. 6 results from N = 5 iterations starting from the initial state ( 33)-( 34) satisfying [START_REF] Raïssi | Some recent results on the design and implementation of interval observers for uncertain systems[END_REF]. Let These zonotopic enclosures are guaranteed to enclose the set of states reached from the initial red cell (resp. green cells) by iterating the sampled non-linear dynamics. Moreover, the initial "implicit paving" gradually leads to possibly overlapping cells (see the blue borders in Fig. 6) since the complexity of the polynotope computed at each iteration is reduced to a finite number (50) of generators. The sparse structure of the exponent matrix E of x at k = 5 is given in Fig. 7. The monomials involve 16 symbolic variables (10 of type unit interval: square marks, 6 of type signed: + marks). There are 90 non-zeros elements. The maximum degree is 3. As expected from the propagation of the initial mixed-encoding of states through a non-linear dynamic, several mixed monomials can be observed, that is, monomials involving both continuous and discrete symbolic variables. This example of reachability with a mixed-encoding of state sets illustrates the ability of mixed polynotopes to trace the propagation of a significant number of hierarchically organized cells within non-trivial dynamics. Bissections have been avoided by dealing with polynomial dependencies between symbolic variables of different types combining continuous and discrete value domains. Moreover, the ability to explicitly characterize the overlapping between cells forming a partition of the initial state set paves the way for efficient symbolic abstraction techniques.

Non-linear and mixed filtering with PKF

The Polynotopic Kalman Fiter (PKF) developed in section §6 is applied to the modified Lotka-Volterra dynamic without and with a mixed encoding of states: The initial state set is assumed to be bounded by Px 0 = [ [START_REF] Combastel | A state bounding observer for uncertain non-linear continuous-time systems based on zonotopes[END_REF][START_REF] Vu Tuan | Zonotopic guaranteed state estimation for uncertain systems[END_REF]; [START_REF] Combastel | A state bounding observer for uncertain non-linear continuous-time systems based on zonotopes[END_REF][START_REF] Vu Tuan | Zonotopic guaranteed state estimation for uncertain systems[END_REF]] ⊂ R 2 . These bounds are obtained from: where g stands for the granularity level of a mixed encoding of the initial states and the measurement noise at each sample time k. Two cases are considered: i) g = 0 corresponds to a purely continuous case (solid lines in Fig. 9) with only symbols of type unit interval.

x + = x + f(x, u)h + Ev, (38)
ii) g = 2 corresponds to a mixed case (dashed lines in Cases: continuous (g = 0) vs. mixed (g = 2), and ↓50 vs. ↓100. g = 0 g = 2 q = 50 3.4 s 3.8 s q = 100 13.9 s 14.8 s At each iteration of PKF, the reduction operator ↓ q with q = 50 or q = 100 is used to: a) implement the reduction of x as in [START_REF] Vu Tuan | Zonotopic guaranteed state estimation for uncertain systems[END_REF], b) reduce the product x 1 x 2 in f(x, u); this is the only (inclusion preserving) difference between f (20) and f (26) in this example. Notice also that g (21) equals g [START_REF] Makino | Rigorous integration of flows and odes using taylor models[END_REF] since the measurement/innovation equation (39) is linear. The simulation of the "true" system is obtained from x 0 = [22; 8] using Heun's method. Consistently with [START_REF] Sinot | Complete laziness: A natural semantics[END_REF], only the first state x 1 ∈ R is measured at each sample time k, and the main purpose of PKF is to estimate state bounds Bx for the state x ∈ R 2 while minimizing the (predicted) polynotope covariation trace. The table 10 reports the computation times with a Matlab implementation: The mixed encoding does not increase very significantly the computation time in spite of the number of discrete configurations, contrary to the number of generators. The evolution in time of the memory footprint of x with ↓ 50 is also reported in Fig. 8: once again, only a slight increase is observed in the mixed case (g = 2) compared to the continuous one (g = 0). The simulation results reported in Fig. 9 show a significant improvement of accuracy compared to EZGKF in a purely bounded-error setting which requires around 2.5 s with q = 200 generators as in [START_REF] Combastel | An extended zonotopic and gaussian kalman filter (EZGKF) merging set-membership and stochastic paradigms: Toward non-linear filtering and fault detection[END_REF]. In particular, PKF shows an enhanced ability to reconstruct x 2 from noisy measurements of x 1 . Mixed encoding tends to give results with increased accuracy, especially for x 1 , provided the number of generators is sufficient. Meanwhile, the maximum degree of computed polytopes is decreased from 6 (resp. 7) in the continuous case g = 0 with q = 50 (resp. q = 100) to only 4 in both mixed cases i.e. with q = 50 or 100. This is consistent with the reduced size of remainder intervals for g = 2 and the influence of rewriting rules, in particular the inclusion neutral rule [START_REF] Gehr | AI2: Safety and robustness certification of neural networks with abstract interpretation[END_REF]. This illustrates the ability of PKF to efficiently deal with nonlinear and mixed dynamics.

Conclusion

An approach for functional sets with typed symbols is introduced in this work. An explicit distinction between syntax and semantics helps formalize the management of dependencies, characterize sources of conservatism and analyze the impact of evaluation strategies (inner first vs. outer first/lazy/call-by-need). Image-sets with typed symbols generalize several set-representations like zonotopes and polynomial zonotopes to mixed domains, as exemplified with mixed polynotopes. The combination of polynomial functions with interval, signed and boolean symbolic variables through simple rewriting rules makes it possible to gather in a single compact and efficient data structure the description of non-convex and non-connected sets which would usually require costly bissection/splitting strategies to be propagated. The mixed-encoding of intervals proposed in this context allows to tune the granularity level of the discrete part of the description and, meanwhile, control the combinatorial complexity through the use of reduction operators. In addition, the traceability of uniquely identified typed symbols paves the way for advanced mixed sensitivity analysis and symbolic abstraction techniques. The reachability results show the relevance of the proposed approach to deal with the verification and synthesis of Cyber-Physical Systems (CPS). Based on modeling tools for nonlinear hybrid systems, a compositional implementation of advanced reachability and filtering algorithms is made possible by simply using operator overloading. This has been exemplified with the proposed Polynotopic Kalman Filter (PKF) which paves the way to advanced hybrid nonlinear filtering techniques preserving inclusion. Moreover, several bridges with random variables and stochastic filtering have been outlined as well as bridges with functional programming and object oriented paradigms, robust (and interpretable?) artificial intelligence [START_REF] Mirman | Differentiable abstract interpretation for provably robust neural networks[END_REF][START_REF] Gehr | AI2: Safety and robustness certification of neural networks with abstract interpretation[END_REF] with the neural network activation function ReLU, sensitivity analysis, and symbolic abstractions of hybrid systems. Much remains to be done to exploit these connections.

  p ⊂ R p by an affine (resp. polynomial) function f : R p → R n . For instance, the zonotope c, R = {c + Rs, s ∈ [-1, +1] p } ⊂ R n is nothing else but the imset of [-1, +1] p by the function f c,R : s → c + Rs. Though the possible shapes of zonotopes in R n with n > 2 are significantly more versatile than that of basic nD intervals, so usually providing very useful degrees of freedom to struggle against the wrapping effect, it remains worth noticing the consequences of the intrinsic symbolic (syntactic) difference between the two expressions f c,R (s a ) and f c,R (s b ) where, e.g., s a ∈ [-1, +1] p and s b ∈ [-1, +1] p . First, the possible values (semantics) taken by both expressions belong to the same zonotope c, R . Indeed, the set-based wrap/enclosure

  (a) Consistently with assumption 6. Polynotopes may support other types. (b) Efficient numeric computations of constant/center vectors and coefficient/generator matrices of polynotope objects motivate this choice. (c) At a syntactic level, canonical polynotopes (obtained after resolving <sfunref> references allowing to compose polynotopes) are polynomial vectors with only typed symbols as variables. Notice that vector linear functions (obtained from <monomial> ::= <variable> while removing <exponent>, <multerm>) give symbolic zonotopes and that nothing a priori hinders the definition of other <sfunction> as functions of typed symbols.

  results from merging the unique identifiers in I and J while removing those possibly related to null generators. The vertical concatenation [M |I ; N |J ] = [M |I ; 0] + [0; N |J ] also illustrates close links between sum and concatenation of MLC.

Fig. 1 .

 1 Fig. 1. Example of mixed e-zonotope 0, R, I s,τ,ι . in the discrete set {-1, +1}, and s 4 , s 5 are of type i (interval) i.e. s 4 , s 5 take their values in the unit interval [-1, +1] ⊂ R. Let I 1 = [1, 2, 3] and I 2 = [4, 5] be vectors of unique identifiers gathering symbols according to their type: Following the definition 7, s I1 is discrete, s I2 is continuous, and s I with I = [I 1 ; I 2 ] is mixed. Let R 1 = [3, 3, -3; 6, -5, 9], R 2 = [4, 2; 2, -4] and R = [R 1 , R 2 ]. Then, the (discrete) e-zonotope 0, R 1 , I 1 s,τ,ι is a set of eight 12 points which are the linear images by R 1 of the vertices of a 3D unit hypercube since ιs I1 ∈ ιτ s I1 = {-1, +1} 3 . The (continuous) e-zonotope 0, R 2 , I 2 s,τ,ι is the classical zonotope 0, R 2 i.e. the linear image by R 2 of a 2D unit hypercube since ιs I2 ∈ ιτ s I2 = [-1, +1] 2 . More interestingly, the (mixed) e-zonotope 0, R, I s,τ,ι is the linear image by R = [R 1 , R 2 ] of ιτ s I = [{-1, +1} 3 ; [-1; +1] 2 ]. It is also the Minkowski sum of the (discrete) ezonotope 0, R 1 , I 1 s,τ,ι and the (continuous) e-zonotope 0, R 2 , I 2 s,τ,ι . The resulting set is neither convex nor connected, as shown in Fig. 1, where the dashed line is the border of the classical (continuous) zonotope 0, R . This example illustrates that mixed zonotopes can provide a very compact representation (Fig.1: R ∈ R 2×5 and 5 bits encoding the symbol types) for the union of a same 13 (continuous) zonotopic shape centered on each point of a discrete set possibly containing a high number of configurations (Fig. 1: 2 3 = 8 = cardinal of {-1, +1} 3 ).

Fig. 2 .

 2 Fig. 2. Example of continuous e-polynotope c, R, I, E s,τ,ι .

Proposition 34 (

 34 Logical ordering) Let (a, b) be a pair of signed (resp. boolean) symbolic variables. Defining the operator > such that (a > b) = ¬(a ≤ b) holds true with operators as in table 5, then (a < b) = (b > a) and (a ≤ b) = ((a < b) ∨ (a = b)) also hold true. More generally, the operators ≤ (i.e. implication 14 ), ≥, >, < follow similar rules as classical order relation operators over reals when signed (resp. boolean) symbols are interpreted with values in {-1, +1} ⊂ R (resp. {0, 1} ⊂ R).

Lemma 37 (

 37 tween s-functions (syntax) and their usual interpretation as a mathematical function (semantic) is not systematic in the following. Example: Let f (x) = e x . Then, f refers either to the s-function built from the wff e x , or to ι m f : x → e x . The notations used for intervals are as follows:x ∈ [x] = [x, x] = x ± x = [x -x, x + x]where x, x, x, x respectively denote the lower bound, upper bound, center (or middle), radius of the interval [x] containing x. Unit range mapping)Let [x] = [x, x] = x ±x ⊂ R. Let µ : [x] → , x → δ = x-xx if x = 0, δ = 0 otherwise. µ -1 (δ) = x + xδ. Unless x = 0 (degenerate point case), the unit range mapping µ (or µ [x] ) of [x] is linear and bijective: It maps the interval range [x] of x to the unit interval containing any δ = µ(x), x ∈ [x].

Fig. 3 .

 3 Fig. 3. Inclusion method of theorem 39 applied to f (x) = e x on [x] = -1 ± 0.5 (magenta) and [x] = +1 ± 0.5 (cyan): plot of e-zonotopes as in corollary 40. x + xδ * = log(ẙ/x).

Theorem 41 (

 41 An inclusion of abs) Let abs : [x] → R, x → y = |x| be the restriction of the absolute value on a given interval [x] = x ± x = [x, x] ⊂ R. Case 1: If x ≤ 0, then abs(.) = -(.), Case 2: If x ≥ 0, then abs(.) = +(.), Case 3: If |x| < x, then abs(.) is an inclusion function for abs(.) on [x] with:

( 32 )

 32 , ∂ G J(G) = -2(R e ΦR T p ) + 2(R e ΦR T e )G T . G * being the value of G such that ∂ G J(G) = 0, it comes G * R e ΦR T e = R pΦR T e and G * = (R p ΦR T e )(R e ΦR T e ) -1 .

  are 20 : (26): c p = Ac + Bu, (26): R p = [A R, E] since Ī ∩ I vp = ∅, (27): c e = Cc + Du -y,

H

  : (a, b) → (s, c) : Half-adder with 5 nand gates t1 ← a b, t2 ← a t1, t3 ← t1 b, s ← t2 t3, c ← t1 t1. F : (a, b, cin) → (s, cout) : Full 1 bit adder with carry (r, c1) ← H(a, b), (s, c2) ← H(r, cin), cout ← ¬c1 ¬c2. N : (A, B, c) → (S, c) : Full n bits adder with carry for i ← 1 . . . n(A), (S(i), c) ← F (A(i), B(i), c).

Fig. 4 .

 4 Fig. 4. Reachability result obtained on the Van-Der-Pol oscillator with continuous polynotopes (the plot results from zonotopic enclosures Zx at each time step).

Fig. 5 .

 5 Fig. 5. Reachability result obtained with polynotopes (cyan) for the model of a 3-link traffic network representing a diverge junction. Comparison with the results reported in Figure 2 in [28]: methods C/GB (blue), SDMM-IA (magenta), MM and SDMM-S/F (red); Monte-Carlo simulations (black dots).

  [T, c, v, x, w] = [30, 40, 0.5, 320, 1/6]. The initial state set is Px 0 = [[150, 200]; [180, 300]; [100, 220]

  [+ -+] be a short notation for [+1; -1; +1] (also applying for other sign combinations). Let x|(s I = v) denote the s-polynotope obtained by substituting in x the expressions in v for the symbolic variables in s I . Unless v depends on some symbols in s I , x|(s I = v) does not depend anymore on s I . The related e-polynotope (resp. ezonotopic enclosure) is Px|(sI = v) (resp. Zx|(s I = v)).Considering the vectors of unique symbol identifiers I and J as in (36)-[START_REF] Rump | Implementation and improvements of affine arithmetic[END_REF], the red (resp. green) cell at k = 0 in Fig.6corresponds to Px 0 |(sI1:3 = [+ -+], s J1:3 = [--+]) (resp. Px 0 |(s I1 = [-], s J1:2 = [+-])).Then, the single s-polynotope x k computed at each iteration k contains all the information required to obtain the related subplot in Fig.6. In particular, the red (resp. green) zonotopic sets are Zx k |(s I1:3 = [+ -+], s J1:3 = [--+]) (resp. Zx k |(s I1 = [-], s J1:2 = [+-])) for k = 1, . . . , 5.

Fig. 7 .

 7 Fig. 7. Sparse structure of the exponent matrix E of x at k = 5: 16 symbolic variables (interval: marks, signed: + marks), 50 monomials/generators, 90 non-zero elements.

y = x 1 +

 1 F w.[START_REF] Sinot | Complete laziness: A natural semantics[END_REF] The prediction model[START_REF] Scott | Constrained zonotopes: A new tool for set-based estimation and fault detection[END_REF] (resp. measurement equation (39)) correspond to[START_REF] Kochdumper | Representation of polytopes as polynomial zonotopes[END_REF] (resp. (21)) in the formulation of PKF with v = [v; w] and Φ = I. The step size is h = 0.04 and k ∈ {0, . . . , N } ⊂ N with N = 750 iterations. The initial and final times are t 0 = 0 and t f = N h = 30. The input is u = 2 for t ∈ [10, 20[ i.e. 250 ≤ k < 500, and u = 0 otherwise. E = 3.10 -3 I, F = 1.5. The state and measurement noises are assumed to be bounded as v ∈ [-1, +1] 2 and w ∈ [-1, +1] i.e. Pv = [-1, +1] 3 .

x 1 ,

 1 0 = 15 + 10.Z g s ([!(g, s); !(1, i)]), x 2,0 = 15 + 10.Z g s ([!(g, s); !(1, i)]), v = [Z 0 s (!(1, i)); Z 0 s (!(1, i)); Z g s ([!(g, s); !(1, i)])],

Fig. 8 .

 8 Fig. 8. Memory footprint of the polynotopic state estimate x with PKF: Evolution in time under ↓50. Left: Continuous (g = 0). Right: Mixed (g = 2). Top: Memory size mem(x) in kilo-octets occupied by the object x, depending on whether the sparse exponent matrix E of x is transposed (red) or not (blue). Bottom: Number of non-zero elements in E.

Fig. 9 )

 9 Fig.9) involving symbols of different types (signed and interval) in mixed polynotope computations. At each iteration of PKF, the reduction operator ↓ q with q = 50 or q = 100 is used to: a) implement the reduction of x as in[START_REF] Vu Tuan | Zonotopic guaranteed state estimation for uncertain systems[END_REF], b) reduce the product x 1 x 2 in f(x, u); this is the only (inclusion preserving) difference between f (20) and f[START_REF] Maïga | A comprehensive method for reachability analysis of uncertain nonlinear hybrid systems[END_REF] in this example. Notice also that g (21) equals g[START_REF] Makino | Rigorous integration of flows and odes using taylor models[END_REF] since the measurement/innovation equation (39) is linear. The simulation of the "true" system is obtained from x 0 = [22; 8] using Heun's method. Consistently with[START_REF] Sinot | Complete laziness: A natural semantics[END_REF], only the first state x 1 ∈ R is measured at each sample time k, and the main purpose of PKF is to estimate state bounds Bx for the state x ∈ R 2 while minimizing the (predicted) polynotope covariation trace. The table 10 reports the computation times with a Matlab implementation: The mixed encoding does not increase very significantly the computation time in spite of the number of discrete configurations, contrary to the number of generators. The evolution in time of the memory footprint of x with ↓ 50 is also reported in Fig.8: once again, only a slight increase is observed in the mixed case (g = 2) compared to the continuous one (g = 0). The simulation results reported in Fig.9show a significant improvement of accuracy compared to EZGKF in a purely bounded-error setting which requires around 2.5 s with q = 200 generators as in[START_REF] Combastel | An extended zonotopic and gaussian kalman filter (EZGKF) merging set-membership and stochastic paradigms: Toward non-linear filtering and fault detection[END_REF]. In particular, PKF shows an enhanced ability to reconstruct x 2 from noisy measurements of x 1 . Mixed encoding tends to give results with increased accuracy, especially for x 1 , provided the number of generators is sufficient. Meanwhile, the maximum degree of computed polytopes is decreased from 6 (resp. 7) in the continuous case g = 0 with q = 50 (resp. q = 100) to only 4 in both mixed cases i.e. g = 2

2 Fig. 9 .

 29 Fig.9) involving symbols of different types (signed and interval) in mixed polynotope computations. At each iteration of PKF, the reduction operator ↓ q with q = 50 or q = 100 is used to: a) implement the reduction of x as in[START_REF] Vu Tuan | Zonotopic guaranteed state estimation for uncertain systems[END_REF], b) reduce the product x 1 x 2 in f(x, u); this is the only (inclusion preserving) difference between f (20) and f[START_REF] Maïga | A comprehensive method for reachability analysis of uncertain nonlinear hybrid systems[END_REF] in this example. Notice also that g (21) equals g[START_REF] Makino | Rigorous integration of flows and odes using taylor models[END_REF] since the measurement/innovation equation (39) is linear. The simulation of the "true" system is obtained from x 0 = [22; 8] using Heun's method. Consistently with[START_REF] Sinot | Complete laziness: A natural semantics[END_REF], only the first state x 1 ∈ R is measured at each sample time k, and the main purpose of PKF is to estimate state bounds Bx for the state x ∈ R 2 while minimizing the (predicted) polynotope covariation trace. The table 10 reports the computation times with a Matlab implementation: The mixed encoding does not increase very significantly the computation time in spite of the number of discrete configurations, contrary to the number of generators. The evolution in time of the memory footprint of x with ↓ 50 is also reported in Fig.8: once again, only a slight increase is observed in the mixed case (g = 2) compared to the continuous one (g = 0). The simulation results reported in Fig.9show a significant improvement of accuracy compared to EZGKF in a purely bounded-error setting which requires around 2.5 s with q = 200 generators as in[START_REF] Combastel | An extended zonotopic and gaussian kalman filter (EZGKF) merging set-membership and stochastic paradigms: Toward non-linear filtering and fault detection[END_REF]. In particular, PKF shows an enhanced ability to reconstruct x 2 from noisy measurements of x 1 . Mixed encoding tends to give results with increased accuracy, especially for x 1 , provided the number of generators is sufficient. Meanwhile, the maximum degree of computed polytopes is decreased from 6 (resp. 7) in the continuous case g = 0 with q = 50 (resp. q = 100) to only 4 in both mixed cases i.e. g = 2

Table 1

 1 Examples of possible domains Dx and DX for a variable x Dx denote a set (or domain) of possible values for x, that is: x ∈ Dx. Also, let DX = ⊂ Dx denote a set of subsets of Dx, including Dx itself, that is: (∀X ∈ DX, X ⊂ Dx) ∧ (Dx ∈ DX). Since the value of any X ∈ DX is a set, X is said set-valued. Notice that

	Example	Dx	DX
	Continuous Rn	Ī Rn
	Discrete	{0, 1}	{{0}, {1}, {0, 1}}
	Mixed	{0, 1} ∪ [2, 4] {{1}, I[2, 3], {0} ∪ [3, 4], Dx}
	2 Inclusion function: beyond intervals
	To begin with, a definition of sets from functions (imset)
	and a definition of inclusion functions are given and dis-
	cussed in a classical (non-symbolic) framework. Given a
	variable x, let

x ∈ Dx is not necessarily set-valued. For instance, the Table

1

reports some continuous, discrete and mixed examples, where R = R ∪ {-∞, +∞}, and ĪX (resp. IX) refers to the set (resp. collection) of real intervals

[a, b]

Table 5

 5 Signed and Boolean logic functions related to basic operators expressed in the ring of multivariate polynomials R[sI ] with coefficients in the real field (R, +, .).

		(a, b)	∈ {-1, +1} 2 ∈ {0, 1} 2
	Op.	Symb.	Signed	Boolean
	not	¬	-a	1 -a
	and	∧	-1+a+b+ab 2	ab
	or	∨	+1+a+b-ab 2

Table 6

 6 Switching functions expressed from the absolute value operator: abs(x) = |x| (or from ReLU * ).

	Function	Notation	Expression with |.| (or pos)
	Maximum	max(x, y)	= x+y 2 + |x-y| 2

Table 7

 7 PKF iteration:

Table 8

 8 Algorithm of functions building Half (H), Full 1 bit (F), and Full n bits (N) adder with nand gates (¬x ↔ x x).

Table 9

 9 Number of distinct generators/monomials of s-polynotopes representing the multi-affine decomposition of an n-bits adder (as in table8) with either signed or boolean symbol(ic variable)s. The computation time is given in seconds (s). is the set of the 2 n possible input values i.e. {-1, +1} n (resp. {0, 1} n ) in the signed (resp. boolean) case. Idem for B. These sets are never computed explicitly: they only describe the set-valued interpretation of semi-symbolic calculi based on the (c, R, I, E) data structure used to represent s-polynotope objects. Then, building the architecture of an n bits adder by computing (S, c) = N (A, B) as in table 8 with s-polynotope overloaded operators results in the s-polynotopes S (sum result) and c (output carry) of dimension n and 1, respectively. S(i) is a polynomial with scalar coefficients giving the expression of the ith bit of S as a function of the input bits/symbols in A, B and an input carry. A full n-bits adder has 2n + 1 (binary) inputs and n + 1 (binary) outputs. The s-polynotope S = [S; c] gathering the sum result and the output carry is thus given by

	n	1	2	3	4	5	6	7	8
	Signed	5	11 23 47 95 191 383 767
	(s) 0.01 0.02 0.03 0.06 0.15 0.36 1.9 8.3
	Boolean 8	23 65 188 554 1649 -	-
	(s) 0.01 0.01 0.03 0.2 2.3 29	-	-
	ables representing the (unknown) bits encoding two in-
	teger operands. The e-zonotope (or e-polynotope) re-
	lated to A

  23, 1.57]; [2.34, 2.46]] as shown by the red box in Fig. 4. 1360 iterations based on an Euler sampling with step size h = 0.005 are computed in 9.8 s with continuous polynotopes under Matlab running on a 1.8 GHz Core i5 processor with 8 Go RAM. The zonotopic enclosure Zx 1360

Table 10

 10 Computation times for 750 iterations of PKF in seconds (s).

Note here that R n = ]-∞, +∞[ n ∈ DX, Dx = Rn = [-∞, +∞] n ∈ DX, and DX = Ī Rn is a strict subset of the power set

Dx of Dx = Rn (e.g. a sphere is not an interval).

not only at a host level but also at a wider scale to also cover the network nodes of distributed systems like CPS.

Regarding functions, continuous refers here to a property of the input domain and not to continuity as in analysis.

as long as it is consistent with the type (unit) interval.

A (lexical) token is a string (i.e. a sequence of characters) with an assigned and thus identified meaning.

In this paper, a sufficiently large finite context is assumed. Concretely, this can be achieved through inclusion preserving reduction schemes, as in definition 17 for instance.

e.g. by using efficient data structures to encode and manipulate the abstract syntax trees of vector polynomials with typed symbols: see[START_REF] Combastel | On computing envelopes for discrete-time linear systems with affine parametric uncertainties and bounded inputs[END_REF] and symbolic polynotopes in 4.3.

e.g. see[START_REF] Combastel | A distributed Kalman filter with symbolic zonotopes and unique symbols provider for robust state estimation in CPS[END_REF], e-polynotopes and definition 30 in 4.3.

<sfundef> thus stands for an <sfunction> as in Table3except that <sfunref> is removed from line/rule

which then becomes <variable>::=<typedsymbol>.

or a vector. Here, the ordering of scalar elements is free.

Note that, alternately, F (sI ) (resp. F (.)) may refer to the abstract syntax tree resulting from parsing the wff f up to typed symbol leafs included (resp. not included).

It could be less if some image points are identical.

Relaxing this constraint is among the motivations to the polynomial extension in §4.3.

Notice that contraposition writes as (a ≤ b) = (¬b ≤ ¬a).

e.g. to weight the relative influence of continuous and discrete symbols/uncertainties on the accuracy criterion further chosen to optimize the mixed-set based state estimates obtained from PKF.

To the benefit of code readability and maintainability.

Up to column permutations with no impact on the interpretation.

Acknowledgements

The author would like to thank Prof. Ali Zolghadri for many insightful discussions during this research work and for his careful reading of the manuscript.