Jan Sliwka (ENSTA-Bretagne, Brest, France), Benoît Clement (ENSTA-Bretagne, Brest, France), Irvin Probst (ENSTA-Bretagne, Brest, France): Sea glider navigation around a circle using distance measurements to a drifting acoustic source

Abstract

We present a simple yet robust sea-glider navigation method in a constellation of drifting Lagrangian drifters under the polar ice cape. The glider has to perform oceanographic measurements; mainly conductivity, temperature and depth, in an area enclosed by the drifters. The glider can not rely on Global Navigation Satellite System (GNSS) positioning data as the ice cape makes it impossible to surface. The presented method does not use a localization algorithm to estimate state space model data. The originality of the presented method resides in the use of only one acoustic beacon and a very simple PID controller based on a basic kinematic model. Interval analysis is used to bound the errors in the estimation of the measured value and its derivative in the presence of noise and outliers. Validation is performed through intensive simulations.

Attached files:

Vu Tuan Hieu Le (SUPELEC Systems Sciences (E3S) – Automatic Control Department, Gif-sur-Yvette, France), C. Stoica (SUPELEC Systems Sciences (E3S) – Automatic Control Department, Gif-sur-Yvette, France), T. Alamo (Department of Ingeniería de Sistemas y Automática, Universidad de Sevilla, Spain), E.F. Camacho (Department of Ingeniería de Sistemas y Automática, Universidad de Sevilla, Spain), D. Dumur (SUPELEC Systems Sciences (E3S) – Automatic Control Department, Gif-sur-Yvette, France): Guaranteed state estimation by zonotopes for systems with interval uncertainties

Abstract

This talk focuses on guaranteed state estimation by zonotopes [1], [2] applied to multivariable linear discrete-time systems in the presence of disturbances, noises and interval uncertainties. Suppose that the perturbations and the noise are unknown but bounded by some zonotopic sets. Under this hypothesis the information about the system states at each sample time is characterized as a zonotope containing all possible system states that are consistent with the considered perturbations and measurement noise.

In [2] a zonotopic outer approximation of the state estimation domain is computed based on the minimization of the $P$-radius associated to the zono- tope. The main idea consists in an outer approximation of the intersection of a zonotope (corresponding to the prediction of the states) with a strip (the measurement from the available sensor). Despite the good approximation, this approach is applied in [2] only to Single-Input Single-Output systems that are not affected by uncertainties. In order to extend this approach to multivariable systems with interval uncertainties, this talk proposes a zonotopic approximation of the intersection between a zonotope (the prediction of the states) and a polytope (the intersection of the measurements from all the sensors). The size of this zonotope is decreased in time by solving an off-line optimization problem. The advantages of this approach are illustrated via a numerical example.

References

[1]	T. Alamo, J.M. Bravo, and E.F. Camacho. Guaranteed state estimation by zonotopes. Automatica, 41:1035–1043, 2005.
[2]	V.T.H. Le, T. Alamo, E.F. Camacho, C. Stoica, and D. Dumur. A new approach for guaranteed state estimation by zonotopes. In Proc. of the 18th IFAC World Congress, Milan, Italy, 2011.

Attached files:

Jun Xiong (LAAS-CNRS & Université de Toulouse; UPS, INSA, INP, ISAE, Toulouse, France), Carine Jauberthie (LAAS-CNRS & Université de Toulouse; UPS, INSA, INP, ISAE, Toulouse, France), Louise Travé-Massuyès (LAAS-CNRS, Toulouse, France): Advances in Interval Kalman Filtering: theoretical aspects and examples

Abstract

State estimations from experimental measures are usually obtained within a stochastic framework in which uncertainty is taken into account through appropriate assumptions about probability distributions of noise and model error.

However, some sources of uncertainty are not well-suited to the stochastic uncertainty assumption and are better modeled as bounded uncertainty. This is typically the case for modeling the tolerance on parameter values, for which the manufacturer provides low and high bounds corresponding to the inherent variance of technological processes.

In this presentation, we consider filtering of discrete time linear models with bounded uncertainties on parameters and measurement noise modeled by gaussian distribution. This work is based on a previous work [1] in which the classical Kalman filtering technique [2] has been extended to interval linear models with known classical statistical assumptions. As the expressions for deriving the Kalman filter involve matrix inversion, one must find a way to implement this tricky algebraic operation whithin an interval framework. In [1] it is suggested to use upper bound of interval matrix as a regular matrix to-be-inverse to provide a sub-optimal solution that does not preserve guaranteed results, some solutions are lost. Our contribution consists in proposing an alternative approach to solve the interval matrix inversion problem without loss of solution while controlling the inherent pessimism of interval calculus.

An original approach is proposed to limit highly overestimation effects propagating within the interval Kalman filter recursive structure. In particular the gain of the filter is obtained by a calculus based on the set inversion algorithm inspired by SIVIA. Some examples are developed.

References

[1]	Guanrong Chen, Jianrong Wang, and Leang S. Shieh. Interval kalman filtering. IEEE Transactions on Aerospace and Electronic Systems, 1997.
[2]	RE Kalman. A new approach to linear filtering and prediction problems. Journal of basic Engineering, 1960.

Attached files:

Gilles Chabert (Ecole des Mines de Nantes, France): IBEX 2.0, a constraint programming library over the reals

Abstract

In this talk, we will make a short demo of the upcoming release 2.0 of the IBEX library. We will give different examples in C++ code of how to solve various problems with IBEX, including systems of equations, global optimization and robust parameter estimation.

Attached files:

Moussa Maïga (Université d’Orléans, PRISME, Bourges, France & CNRS, LAAS, Toulouse, France), Nacim Ramdani (Université d’Orléans, PRISME, Bourges, France), Louise Travé-Massuyès (CNRS, LAAS, Toulouse, France): First results on nonlinear hybrid reachability combining interval Taylor method and IBEX library.

Abstract

Computing the reachable set of hybrid dynamical systems in a reliable and verified way is an important step when addressing verification or synthesis tasks. This issue is still challenging for uncertain nonlinear hybrid dynamical systems.

In a previous work [1], we introduced a method for solving the flow/sets intersection issue that is at the core of hybrid reachability. It derives first an analytical expression for the boundaries of continuous flows using interval Taylor methods and techniques for controlling the wrapping effect. Then, it expresses the event detection and localization problems underlying flow/sets intersection as constraint-satisfaction problems (CSP), which were then solved using global search methods based on some ad-hoc branch-and- prune algorithms, interval analysis and consistency techniques.

In this talk, we report the technical improvements of the above method as obtained by using the IBEX (www.emn.fr/z-info/ibex/) library [2] for solving the underlying CSPs. The performance of the new method is illustrated on several hybrid systems benchmarks.

References

[1]	N. Ramdani and N. S. Nedialkov. Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques. Nonlinear Analysis: Hybrid Systems, 5(2):149 – 162, 2011.
[2]	G. Chabert and L. Jaulin. Contractor programming. Artificial Intelligence, 173:1079 – 1100, 2009.

Attached files:

Elke Just (Applied Computer Science Group, University of Wuppertal, Germany): Recent Progress in SONIC

Abstract

We will present a short overview of our solver SONIC followed by a more detailed presentation of some features. SONIC contains a verified solver and optimizer for nonlinear equation systems and is achieving rigor by working with interval arithmetics using different interval libraries such as C-XSC and filib++.

Focus will be put on the utilization of the extended Newton method in a hierarchy of extended systems, i.e., systems with additional variables for subterms in the original system. In particular the usage of different preconditioners in this method will be considered.

We will also discuss whether restricting the method to a subset of variables may diminish the computational costs on large extended systems while still providing good results.

Attached files:

Karsten Scheibler (Institute of Computer Science, Albert-Ludwigs-University, Freiburg im Breisgau, Germany), Felix Neubauer (Institute of Computer Science, Albert-Ludwigs-University, Freiburg im Breisgau, Germany), Bernd Becker (Institute of Computer Science, Albert-Ludwigs-University, Freiburg im Breisgau, Germany): Integration of Fourier-Motzkin based Variable-Elimination into iSAT

Abstract

Over the past decades the complexity of embedded systems increased dramatically. Today, embedded systems often contain analog parts in addition to their digital components – making them to embedded hybrid systems. Especially in safety critical environments like automotive or avionics applications it is desired to be able to prove the correctness of such hybrid systems.

SAT modulo Theories (SMT)-Solvers are able to handle boolean combinations of linear and nonlinear arithmetic constraints and thus are a natural choice to verify safety properties of systems with hybrid discrete-continous behaviour. The SMT- Solver iSAT additionally provides support for transcendental functions like sine or cosine. Furthermore iSAT tightly integrates interval-based arithmetic reasoning into the Conflict Driven Clause Learning (CDCL) framework used by most modern SAT-Solvers. But because of the use of interval-arithmetic, iSAT may not always be able to give a conclusive result.

The talk addresses this problem and presents the integration of a variable elimination technique based on Fourier-Motzkin into iSAT.

Acknowledgment

This work has been partially supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center Automatic Verification and Analysis of Complex Systems (SFB/TR 14 AVACS, www.avacs.org).

Attached files:

Luc Jaulin (ENSTA-Bretagne, LabSticc, Brest, France): An interval approach for stability analysis of nonlinear systems

Abstract

This talk proposes a new interval-based method for robust stability analysis of nonlinear systems. The principle of the approach is to represent uncertain systems by differential inclusions and then to perform a Lyapunov analysis in order to transform the stability problem within a set-inversion framework. With this approach, we can show that for all feasible perturbations, (i) there exists a safe subset A of the state space the system cannot escape as soon as it enters in it and (ii) if the system is outside A, it cannot stay outside A forever. In a second step, the methodology is used to build reliable robust controllers. An illustration related to the line following problem of sailboat robots is then provided.

Attached files:

Fabrice Le Bars (ENSTA-Bretagne, LabSticc, Brest, France): An experimental validation of reliable controllers on a sailboat robot

Abstract

Interval methods make it possible to validate theoretically the reliability of robust controllers. Now, this theoretical validation is based on assumptions (such as state equation, bounds of measurement errors, etc) that are not fully satisfied in practice. A validation on convincing experiments is always required. This talk describes an actual experiment that took place on January 2012. In this experiment the sailboat robot, named Vaimos, has gone autonomously from Brest to Douarnenez (around 100 km). It is also explained how simulators with hardware in the loop are fundamental to detect bugs, mechanical failures and also the plan the mission.

Attached files:

Max Demenkov (Institute of Control Sciences Russian Academy of Sciences, Moscow, Russia): Real-time control allocation using zonotopes

Abstract

Control allocation is related to control of overactuated systems, and provides a method of distributing the total control demand among the individual actuators. The idea of control allocation allows to deal with control constraints and actuator faults separately from the design of the main regulator, which uses virtual control input. In many cases, this input consists of three moments or angular rates used to control a mechanical system [1, 2], while the number of physical actuators can be much higher. In case of fault in an actuator, instead of reconfiguring the main control law, we need to change only the distribution of the virtual input among other actuators that are still in use.

Using linearization, control allocation of virtual input $v$ is equivalent to linear inverse problem with interval-constrained vector $u$, which we need to figure out: $v=Bu$, where $B$ has more columns than rows. The problem can be solved by linear or quadratic programming [3], but this solution in some cases cannot be adopted due to the safety sertification issues or high complexity of optimization routines for on-board realization.

Note that if $u$ constrained to a box, then $v$ is constrained to its linear image, a zonotope. Zonotopes have been used previously for state and reachable sets estimation in linear discrete systems, also they are naturally considered in the affine arithmetics approach. We propose a method for calculating $u$, based on control box bisection and explicit description of its image in the form of a system of linear inequalities [4]. In our aproach, no over-approximation problem occurs - we immediately discard boxes that contain no given $v$ in their image. If we divide control box into many parts in once, we can use convex function of $u$ for choosing boxes with some additional optimization criteria.

References

[1]	T. Fossen, T. Johansen, T. Perez, “A survey of control allocation methods for underwater vehicles”, InA. Inzartsev (ed.), Intelligent Underwater Vehicles, I-Tech Education and Publishing, Vienna (2009).
[2]	B. Schofield, T. Hagglund, “Optimal control allocation in vehicle dynamics control for rollover mitigation”, In Proceedings of the American Control Conference, Seattle, Washington, USA (2008).
[3]	M. Bodson, “Evaluation of optimization methods for control allocation”, AIAA Journal of Guidance, Control, and Dynamics, 25, No. 4, 703-711 (2002).
[4]	M. Demenkov, “Interval bisection method for control allocation”, In Proceedings of the 17th IFAC Symposium on Automatic Control in Aerospace, Toulouse, France (2007).

Acknowledgment

This work has been partially supported within Program 1 (”Theoretical foundations of robotics and mechatronics”) by the Russian Academy of Sciences (Brancn for Power Industry, Machine Building, Mechanics and Control Processes)

Attached files:

Tomáš Dzetkulič (Institute of Computer Science, Academy of Sciences of the Czech Republic, Prague, Czech Republic): Endpoint and Midpoint Interval Representations - Theoretical and Computational Comparison

Abstract

In classical interval analysis [2] a real value $x$ is represented by an interval $x \in [x_{lo}, x_{hi}]$ where $x_{lo}$ and $x_{hi}$ are two floating point numbers. There are further possible representations of the value of $x$ using two or three floating point numbers:

• $x \in [x_{mid} -e, x_{mid} +e]$ using two floating point numbers $x_{mid}$ and $e$
• $x \in [x_{mid} -e_{lo}, x_{mid} +e_{hi}]$ using three floating point values $x_{mid}$, $e_{lo}$ and $e_{hi}$

Intervals of the form $[x_{mid} -e, x_{mid} +e]$ and operations with those were used in [3], but their main purpose was multi-precision arithmetic. In our work, we introduce intervals of the form $[x_{mid} -e_{lo}, x_{mid} +e_{hi}]$ and we show, that intervals in both alternative forms provide tighter enclosures compared to the classical interval form. We also compare all interval representations on computational examples.

To motivate our work, let us consider an example where $x = 1/15$. Using the classical interval format, the tightest possible interval that contains $x$ using standard double precision floating point format [1] is $$[6.66666666666666657415 \times 10^{-2}, 6.66666666666666796193 \times 10^{-2}]$$ The width of this interval is approximately $1.387779\times 10^{-17}$. Using the alternative representation with $x_{mid} \doteq 6.66666666666666657415 \times 10^{-2}$, we can obtain $$e = e_{hi} \doteq 9.252 \times 10^{-19}; e_{lo} = 0$$ With either one of the alternative representations, we can obtain an order of magnitude tighter enclosure of the actual value of $x$. In general, the obtained precision is not that high. Still, both alternative representations provide tighter interval enclosures of $x$ on average compared to classical interval analysis.

References

[1]	IEEE Standards Board. IEEE standard for binary floating-point arithmetic. Technical report, The Institute of Electrical and Electronics Engineers, 1985. Technical Report IEEE Std 754- 1985.
[2]	R. E. Moore, R. B. Kearfott, and M. J. Cloud. Introduction to Interval Analysis. SIAM, 2009.
[3]	A. Wittig and M. Berz. Rigorous high precision interval arithmetic in COSY INFINITY. Proceedings of the Fields Institute, 2009.

Acknowledgment

This work was supported by Czech Science Foundation grant 201/09/H057, Ministry of Education, Youth and Sports project number OC10048 and long-term financing of the Institute of Computer Science (RVO 67985807). The author would like to thank Stefan Ratschan for a valuable discussion and helpful advice.

Attached files:

Jaroslav Horáček (Charles University, Faculty of Mathematics and Physics, Department of Applied Mathematics, Prague, Czech Republic & University of Economics, Faculty of Informatics and Statistics, Prague, Czech Republic), Milan Hladík (Charles University, Faculty of Mathematics and Physics, Department of Applied Mathematics, Prague, Czech Republic & University of Economics, Faculty of Informatics and Statistics, Prague, Czech Republic): Pitfalls of Computing Enclosures of Overdetermined Interval Linear Systems

Abstract

Real-life problems can be described by different means – difference and differential equations, linear and nonlinear systems etc. The description can be often transformed to another one using only linear equalities (or inequalities). That is why interval linear systems are still in the focus of researchers. There are plenty of methods for enclosing the solution set of square interval linear systems (systems in the form Ax=b, where A is a square matrix). That is the impact of some possibly good properties of square matrices. They can be diagonally dominant, positive definite, M-matrices and many more. And we know that our algoritms behave well in those cases. However we have some systems called overdetermined. Simply said, they consist of more equations than variables.

There are some known methods for solving them – Gaussian elimination, classical iterative methods, the Rohn method, the least squares, supersquare and subsquare methods or linear programming. Of course, in applications the matrices can often be of some very specific form. But if we consider random matrices, there are some cases when these methods can fail to compute any result. Here we would like to present a brief summary of existing methods for solving overdetermined linear systems and the problems we met when testing those methods on random matrices with specific properties. Our task was to achieve the best possible enclosures on solutions of interval linear systems with various radii of intervals. It is interesting to observe how some efficient methods fail when the radii of intervals change and, on the other hand, to see how some simple, one could say ”stupid” methods rule. We do not want to criticize yet developed methods, we just want to point out that we must be careful when applying chosen methods to solve our desired problems. As always it holds that not every method is useful for every problem.

Attached files:

Aymeric Bethencourt (ENSTA-Bretagne, Brest, France): 3D reconstruction with interval analysis using the Kinect device and an IMU

Abstract

The principle behind Visual Simultaneous Localization And Mapping (VSLAM) applications like 3D object reconstruction or indoor mapping is to estimate the spatial transformation between two poses which consist of large clouds of points. They can further be processed to obtain detailed surfaces. The standard algorithm for finding the alignment between two points clouds is Iterative Closest Point (ICP) and its variants, combined with RANdom SAmple Consensus (RANSAC).

This researches presents a new approach using interval analysis. The idea is to define large intervals for the transformation parameters between the poses then to successively contract those intervals using the equations of the transformation of corresponding points between the poses. To contract those intervals faster, we had the idea of adding an Inertial Measurement Unit (IMU) to our system so the initial interval of the parameters is already small before applying the contractions.

We implemented our algorithm using the middleware ROS and stated our performances.

Attached files:

Andreas Baumgart (OFFIS, Oldenburg, Germany): Solving geometric constraints to verify independence properties for safety-relevant systems

Abstract

Safety-relevant systems like an automotive airbag controller or the wheel-braking system of an airplane may not fail due to a single fault. Typically redundancy is introduced into the system as a safety-means e.g. by adding another realization of the same sub-system. However, single faults can exists which are common causes for the failure of redundant sub-systems. Therefore, safety-standards like ISO26262 [1] or ARP4761 [2] require to verify these systems to be independent from such single faults as common causes. Independence includes spatial separation of redundant sub-systems to avoid effects of environmental factors or installation faults. In this presentation environmental factors are considered, each of which is a potential common cause. Typical environmental factors are radiation like electromagnetic fields and heat or objects on trajectories with high kinetic energy like accidentially occuring wheel fragments, turbine blades and birds. Subject of this investigation is the physical space claimed by a system- component and by a potential object due to an environmental factor. If such common space exists the system-component is affected by the environmental factor and its provided service potentially fails.

To be more specific in this presentation we will show how to apply interval-based constraint- solving methods to tackle this problem. In an independence analysis each system-component is considered to have a shape in a cartesian coordinate system. This shape defines the physical volume of the system-component and thus all positions belonging to it. If a system-component is installed to a system all of its positions are translated to coordinates relative to the system. Shapes are described in terms of primitive shapes like cylindroids, spheroids, cuboids, arbitrary polyhedrons or combinations thereof. Physical space claimed by an object of an environmental factor is also described as a shape which corresponds either to a fixed location in a system or to a trajectory. The mathmatical description of such installed shapes and trajectories is a system of non-linear equations and inequalities. They constrain the positions claimed by the installation of the system-components or by the environment factors. These equations and inequalities are used to formalize the question whether there are positions claimed by the environment factor which are also claimed by all installations of the redundant sub-systems. A candidate-solution provides a counter-example for the verification problem whether an installation of redundant sub-systems cannot fail due to single faults.

References

[1]	Road Vehicles - Functional Safety. International Standard Organization, November 2011.
[2]	Society of Automotive Engineers, SAE ARP4761 Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment. Warrendale, USA, December 1996.

Attached files:

Clément Aubry (IRENav, École navale, Brest, France), Luc Jaulin (ENSTA Bretagne, LABSTICC, Brest, France): Existence and uniqueness tests to solve image evaluation problem

Abstract

The problem to be considered is the characterization of the set $$\mathbb{S} = \{\mathbf{p} \in \mathbb{R}^m, \exists \mathbf{x} \in [\mathbf{x}] \subset \mathbb{R}^n , \mathbf{f}(\mathbf{p}, \mathbf{x}) = \mathbf{0}\}.$$ where $\dim(\mathbf{x}) = \dim(\mathbf{f}).$ We shall consider the case where $[\mathbf{x}]$ is small but where $\dim \mathbf{x}$ is large whereas $\dim \mathbf{p}$ is small. As a consequence, we want to avoid any bissection over the $\mathbf{x}$-space. The set $\mathbb{R}^m$ will be partionned into four zones. The first zone contains points that are outside $\mathbb{S}$. The second zone contains $\mathbf{p} \in \mathbb{S}$ such that there exists a unique $\mathbf{x}$ that satisfies the equations. The third zone constains $\mathbf{p} \in \mathbb{S}$ such that the unicity of the corresponding $\mathbf{x}$ is not proved. The last zone contains $\mathbf{p}$ for which nothing has been proved.

Examples from [MB79], [JKDW01], [GJ06] are presented in order to show the efficiency of the approach.

References

[GJ06]	A. Goldsztejn and L. Jaulin. Inner and outer approximations of existentially quantified equality constraints. In Proceedings of the Twelfth International Conference on Principles and Practice of Constraint Programming, (CP 2006), Nantes (France), 2006.
[JKDW01]	L. Jaulin, M. Kieffer, O. Didrit, and E. Walter. Applied Interval Analysis. Springer, 2001.
[MB79]	Ramon E. Moore and Fritz Bierbaum. Methods and Applications of Interval Analysis (SIAM Studies in Applied and Numerical Mathematics) (Siam Studies in Applied Mathematics, 2.). Soc for Industrial & Applied Math, 1979.

Attached files:

Evgenija D. Popova (Institute of Mathematics and Informatics, Bulgarian Academy of Sciences, Sofia, Bulgaria ): Properties and Estimations of Parametric AE Solution Sets

Abstract

Consider linear systems $A(p)x = b(p)$ whose input data are linear functions of uncertain parameters varying within given intervals, $p_i \in [p_i]$, $i = 1, \dots, k$. Such systems are common in many engineering analysis or design problems, control engineering, robust Monte Carlo simulations, etc., where there are complicated dependencies between the model parameters which are uncertain. We are interested in the parametric AE solution sets, which are defined by universally and existentially quantified parameters, and the former precede the latter. For two disjoint sets $\mathcal{E}$ and $\mathcal{A}$, such that $\mathcal{E} \cup \mathcal{A} = \{1, \dots, k\}$, $$\Sigma^p_{AE} = \Sigma(A(p), b(p), [p]) := \{ x \in \mathbf{R}^n \mid (\forall p_{\mathcal{A}} \in [p_{\mathcal{A}}]) (\exists p_{\mathcal{E}} \in [p_{\mathcal{E}}]) (A(p)x=b(p))\}.$$

In this talk we present the explicit description of some parametric AE solution sets together with some important inclusion relations between such solution sets. In the special cases of parametric tolerable and controllable solution sets we discuss some newly proven properties of these solution sets. Numerical examples accompanied by graphic representations illustrate the solution sets and their properties. Some methods for inner and outer estimations of parametric AE solution sets will be also presented. Special discussion on the properties of these methods for estimating the parametric tolerable and controllable solution sets will be provided.

As an application of the parametric AE solution set estimations we consider parametric AE solution sets of the interval Lyapunov matrix equation of small size. The most common approach in solving matrix equations is to transform the matrix equation into a corresponding linear system. The state matrix in the Lyapunov matrix equation can be either interval or can have linear uncertainty structure. In both cases the parametric approach is applicable if we want sharp estimations.

Attached files:

Andreas Eggers (Carl von Ossietzky Universität, Oldenburg, Germany), Nacim Ramdani (Université d’Orléans, PRISME, Bourges, France), Nedialko S. Nedialkov (McMaster University, Hamilton, Ontario, Canada), Martin Fränzle (Carl von Ossietzky Universität, Oldenburg, Germany): Recent Improvements of iSAT-ODE

Abstract

In this talk, we will present our improvements to the iSAT-ODE solver, which extends the iSAT solver for Boolean combinations of arithmetic constraints over integer- and real-valued variables with enclosure methods for solution sets of Ordinary Differential Equations (ODEs). Such constraint systems occur naturally e.g. when encoding reachability properties of hybrid discrete-continuous systems. The iSAT-ODE solver combines an interval-based extension of SAT solving with validated ODE enclosure generation using VNODE-LP and bracketing systems.

Since ODE enclosures in iSAT-ODE play a role similar to propagators in Interval Constraint Propagation, often similar requests are made to the ODE solver which can benefit significantly from reusing intermediate results from previous computation steps. One improvement that we want to present in this talk is therefore based on extracting the Taylor coefficients, which are computed by VNODE-LP, and reusing them to avoid unnecessary expensive recomputations.

A second improvement is the support for box-shaped flow invariants, which allow the solver to detect earlier when all trajectories emerging from a pre-valuation have left e.g. the mode invariant of a hybrid automaton, which can now be encoded directly by a flow-invariant constraint.

Acknowledgment

This work has been supported by the German Research Council DFG within SFB/TR 14 “Automatic Verification and Analysis of Complex Systems” (www.avacs.org), by the French National Research Agency under contract ANR 2011 INS 006 04 “MAGIC-SPS” (projects.laas.fr/ANR-MAGIC-SPS), and by the Natural Sciences and Engineering Research Council of Canada.

Attached files:

Andreas Eggers (Carl von Ossietzky Universität, Oldenburg, Germany), Nacim Ramdani (Université d’Orléans, PRISME, Bourges, France), Nedialko S. Nedialkov (McMaster University, Hamilton, Ontario, Canada), Martin Fränzle (Carl von Ossietzky Universität, Oldenburg, Germany): On Set-Membership Estimation of Hybrid Systems via SAT Modulo ODE

Abstract

Set membership estimation (SME) of nonlinear hybrid systems is still a challenging issue. Although SME of nonlinear continuous systems has made significant progress recently, the direct extension of these methods to the hybrid case is not easy.

Meanwhile, satisfiability (SAT) checkers for Boolean combinations of arithmetic constraints over real- and integer-valued variables have made significant progress, as they can effectively deal with algebraic constraints between variables and non-linear ODEs, what is denoted as SAT Modulo ODE [1]. Finally, the corresponding solvers solve in a natural way the hybrid differential and algebraic constraints satisfaction problems that underlie SME of hybrid systems.

This talk presents the first results of the application of such a SAT Modulo ODE solver to SME of hybrid dynamical systems [2].

References

[1]	A. Eggers, N. Ramdani, N. S. Nedialkov, and M. Fränzle. Improving SAT Modulo ODE for hybrid systems analysis by combining different enclosure methods. In G. Barthe, A. Pardo, and G. Schneider, editors, Software Engineering and Formal Methods, volume 7041 of LNCS, pages 172–187. Springer, 2011.
[2]	A. Eggers, N. Ramdani, N. S. Nedialkov, and M.Fränzle. Set-Membership Estimation of Hybrid Systems via SAT Modulo ODE. In 16th IFAC Symposium on System Identification, SYSID 2012, July 11-13, Bruxelles, 2012.

Acknowledgment

This work has been supported by the German Research Council DFG within SFB/TR 14 “Automatic Verification and Analysis of Complex Systems” (www.avacs.org), by the French National Research Agency under contract ANR 2011 INS 006 04 “MAGIC-SPS” (projects.laas.fr/ANR-MAGIC-SPS), and by the Natural Sciences and Engineering Research Council of Canada.

Attached files:

Tomáš Dzetkulič (Institute of Computer Science, Academy of Sciences of the Czech Republic, Prague, Czech Republic): Rigorous Computation with Function Enclosures in Chebyshev Basis

Abstract

When rigorously computing with a real function, a truncated Taylor series polynomial approximation is commonly used to replace the actual function. One of the applications of such a rigorous function enclosure lies in verified algorithms for integration of non-linear ordinary differential equations [4].

In this paper, we present a multi-variable function enclosure using the Chebyshev series approximation and the remainder term stored as an interval. Since the Chebyshev series converge faster for all analytic functions compared to the Taylor series, our function enclosures approximate real functions with tighter remainder intervals.

In existing work [1,2], only operations with functions in one variable are described. In [1], the function approximation is stored in the form of function values in the Chebyshev nodes. The authors use non-rigorous methods to compute coefficients of Chebyshev polynomials and no enclosure of the exact function value is guaranteed. On the other hand, the authors in [2] use rigorous methods, but only addition, multiplication and composition of one variable functions are presented.

We present an efficient algorithm for rigorous addition, substraction, multiplication, division, composition, integration and derivative of multi-variable Chebyshev function enclosures. Our publicly available implementation [3] supports function enclosures based on both Taylor and Chebyshev truncated series and allows their comparison. Computational experiments with the initial value problem of ordinary differential equations show that the approach is competitive with the best publicly available verified solvers.

References

[1]	Z. Battles and L. N. Trefethen. An extension of MATLAB to continuous functions and operators. SIAM J. Sci. Comput., 25:1743–1770, May 2004.
[2]	N. Brisebarre and M. Joldeş. Chebyshev interpolation polynomial-based tools for rigorous computing. In Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, ISSAC ’10, pages 147–154, New York, NY, USA, 2010. ACM.
[3]	T. Dzetkulič. ODEINTEGRATOR. http://odeintegrator.sourceforge.net, 2012. Software package.
[4]	K. Makino and M. Berz. Rigorous Integration of Flows and ODEs using Taylor Models. Symbolic Numeric Computation, pages 79–84, 2009.

Acknowledgment

This work was supported by Czech Science Foundation grant 201/09/H057, Ministry of Education, Youth and Sports project number OC10048 and long-term financing of the Institute of Computer Science (RVO 67985807). The author would like to thank Stefan Ratschan for a valuable discussion and helpful advice.

Attached files:

Xin Chen (RWTH Aachen University, Germany), Erika Ábrahám (RWTH Aachen University, Germany), Sriram Sankaranarayanam (University of Colorado, Boulder, CO, USA): Using Taylor Models in the Reachability Analysis of Non-linear Hybrid Systems

Abstract

We propose a novel approach to use Taylor models, independently developed by Berz and Makino, in the reachability analysis of non-linear hybrid systems. A Taylor model $\mathbb{T} = (p, I)$ over domain $D$ is specified by an $n$-dimensional polynomial $p$ and interval domains (boxes) $D$, $I \subseteq \mathbb{R}^n$ and represents the set $$\mathbb{T} = \{\mathbf{x} \in \mathbb{R}^m | \exists \mathbf{x}_0 \in D. \exists \mathbf{i} \in I. \mathbf{x} = p(\mathbf{x_0} ) + \mathbf{i}\}.$$ A Taylor model $(p, I)$ over domain $D$ is a $k$-order over-approximation for a $(k + 1)$ times differentiable function $f : D \rightarrow \mathbb{R}^m,$ if the polynomial $p$ is the order $k$ Taylor expansion of $f$ around the center point of $D$ and the interval $I$ encloses the remainder. Taylor model arithmetic can be used to apply basic arithmetic operations to Taylor models as well as, e.g., anti-derivation and Lie derivation w.r.t. a non-constant vector field.

Our goal is to integrate Taylor models into the reachability analysis of hybrid systems. Hybrid systems, often modeled as hybrid automata, exhibit both continuous dynamics (flows modeled by ordinary differential equations and restricted by invariants) and discrete behaviour (guarded jumps). Besides the higher-order approximations of the flows by Taylor models, the main challenge in our work is the computation of flow/invariant and flow/guard intersections. Note that, given a Taylor model representing a flowpipe, in general the above intersections cannot be exactly represented by Taylor models.

Assume a Taylor model $\mathbb{T}$ and a convex polytope $S$ (representing an invariant or a guard). We introduce three techniques to over-approximate $T \cap S$ by a Taylor model $\mathbb{T}^*.$ Firstly, our domain contraction technique of polynomial complexity computes a contraction $D^*$ of $D$ such that $\mathbb{T}^*$ resulting from $\mathbb{T}$ when replacing $D$ by $D^*$ overapproximates $T \cap S$. We use a combination of the branch-and-prune algorithm and interval constraint propagation to compute $D^*$ . Secondly, we present the template method which computes $\mathbb{T}^*$ by SMT solving as an instance of a template $(p^*, [0, 0]^m)$ over $D^*,$ where $D^*$ is fixed and $p^*$ is a polynomial with parametric coefficients, whose parameters are fixed by the computation. Thirdly, we offer some geometric methods to wrap the intersection by some geometric objects, e.g., zonotopes or support functions.

We have implemented our ideas in a tool, which we use to show results for several interesting and challenging benchmarks.

Attached files:

Thomas Dötschel (University of Rostock, Germany), Ekaterina Auer (University of Duisburg-Essen, Germany), Andreas Rauh (University of Rostock, Germany), Harald Aschemann (University of Rostock, Germany): Sliding Mode Control for Uncertain Thermal SOFC Models with Physical Actuator Constraints

Abstract

Mathematical models for the dynamics of high-temperature Solid Oxide Fuel Cells (SOFCs) can be subdivided into thermal, fluidic, and electro-chemical system components. For the purpose of automatic control design of such systems, it is especially important to focus on the thermal subsystem. This results from the fact that high operating temperatures are advantageous for the efficiency of SOFCs. Moreover, high operating temperatures are necessary to enable the conductivity of oxygen ions through the electrolyte [1]. Typically, thermal models for SOFCs are characterized by their instationarity, where three different operating phases can be distinguished.

Firstly, the heating phase is characterized by a transient process which starts at the thermo- dynamic equilibrium and leads the SOFC stack module to its high-temperature operating point. Secondly, variable electrical loads influence the thermal behavior of the SOFC during its usual operating mode. Thirdly, again an instationary cooling process takes place during the shutdown phase of the system.

In this contribution, a model-based robust control law is derived with the focus on the rejection of disturbances in the standard operating point of SOFCs. For that purpose, a mathematical model is derived for the thermal behavior of the stack module on the basis of the first law of thermodynamics. To approximate the spatial temperature distribution in the interior of the stack module, a semi-discretization scheme is applied to determine a finite volume representation in terms of a set of nonlinear coupled ordinary differential equations (ODEs). In [3] and [4], interval- based global optimization routines accounting for an imperfect system knowledge were introduced for the identification of the parameters of these ODEs. These methods start with an initial guess for a parameter range, in which the a-priori unknown parameters are guaranteed to be included. Then, a bisection scheme is employed to determine feasible enclosures for the parameter ranges which are consistent with both the semi-discretized system model and the measured data.

These parameter intervals are treated as uncertainties for which a robust control law has to be determined. In this presentation, interval methods are used for the derivation of guaranteed stabilizing control procedures on the basis of suitable Lyapunov functions making use of the sliding mode control approach. In [2], a first attempt has been published for the design of such controllers under consideration of interval parameters representing a limited system knowledge as well as the effects of disturbances. In SOFC systems, the enthalpy flow of the cathode gas is provided as a control input for the thermal behavior. This enthalpy flow can be adapted by both manipulating the air mass flow and the temperature difference between the supplied air in the preheating unit and in the inlet elements of the fuel cell stack module. If the above-mentioned sliding mode control procedure is employed to determine the enthalpy flow, further physical restrictions have to be accounted for which result from the admissible operating ranges of both the valve for the air mass flow and the temperature of the preheating unit. Moreover, the variation rate of the temperature difference between the preheating unit and the stack module's inlet elements has to be restricted to prevent damages due to thermal stress. These feasibility constraints are taken into account in terms of an appropriate cost function which is evaluated along with the design criteria for the guaranteed stabilizing interval-based sliding mode control law.

Results for the interval-based verified parameter identification of the SOFC test rig available at the Chair of Mechatronics at the University of Rostock and simulation results for the above-mentioned control approach conclude the presentation, along with an outlook on our future research.

References

[1]	R. Bove and S. Ubertini, editors. Modeling Solid Oxide Fuel Cells. Springer, Berlin, 2008.
[2]	A. Rauh and H. Aschemann. Parameter Identification and Observer-Based Control for Distributed Heating Systems -- The Basis for Temperature Control of Solid Oxide Fuel Cell Stacks. Mathematical and Computer Modelling of Dynamical Systems, 2011.
[3]	A. Rauh, T. Dötschel, E. Auer, and H. Aschemann. Interval Methods for Control-Oriented Modeling of the Thermal Behavior of High-Temperature Fuel Cell Stacks. In Proc. of 16th IFAC Symposium on System Identification SysID 2012, Brussels, Belgium, 2012. Accepted.
[4]	A. Rauh, L. Senkel, and H. Aschemann. Sensitivity-Based State and Parameter Estimation for Fuel Cell Systems. In Proc. of 7th IFAC Symposium on Robust Control Design, Aalborg, Denmark, 2012. Accepted.

Attached files:

Andreas Rauh (University of Rostock, Germany), Julia Kersten (University of Rostock, Germany), Thomas Dötschel (University of Rostock, Germany), Harald Aschemann (University of Rostock, Germany): Interval-Based Model-Predictive Control for Uncertain Dynamic Systems with Actuator Constraints

Abstract

Model-predictive control approaches are well-known means to stabilize dynamical systems and to compute input signals online which allow for the tracking of desired state trajectories. These control procedures, which are partially implemented by means of algorithmic differentiation, are inherently robust and can, therefore, be used to compensate unknown disturbances to some extent [1, 2]. This holds even if the disturbances are neglected during the derivation of the predictive control strategy. Besides tracking desired state trajectories, model-predictive controllers can be employed to enhance the overall system performance by the minimization of suitable cost functions in real time. These criteria typically take into account the control effort in addition to the deviation of the state variables (or system outputs) from their corresponding desired values. In such a way, it becomes possible to compute control strategies online which account for both influence factors simultaneously.

In this presentation, an overview of different verified extensions is given for the design of model- predictive control strategies. These controllers are implemented by applying interval arithmetic procedures in real time. In such a way, the influence of uncertain parameters and measurement uncertainties, which can be described by interval vectors, can be taken into account directly. This allows one to design control laws which definitely prevent the violation of predefined tolerance intervals around the desired state trajectories. Additionally, the application of interval arithmetic procedures gives the possibility for an online redesign of desired trajectories if the violation of the above-mentioned tolerance intervals cannot be avoided due to the activation of actuator saturations [3, 4].

The corresponding computational procedures are described both for a simple illustrative example and for the control of the thermal behavior of high-temperature fuel cell stacks. This application scenario is characterized by the fact that internal parameters can be determined only within certain intervals due to the necessity to use mathematical system models that can be evaluated in real time. Furthermore, temperature uncertainty due to limited measurement facilities in the interior of the fuel cell stack can be expressed by interval parameters in a natural way. Finally, interval parameters describe disturbances resulting from the variation of electrical load demands which are a-priori unknown to the controller. Under consideration of these uncertainties, a reliable control strategy has to be implemented in such a way that the range of technologically feasible input values is not violated.

Like any other interval arithmetic procedure for the evaluation of dynamic system models (either discrete-time or continuous-time initial value problems), interval-based predictive control procedures suffer from overestimation resulting from both the dependency problem and the wrapping effect. In the case of predictive control procedures, this overestimation may lead to control strategies which are more conservative than necessary. To detect overestimation in the interval evaluation of the predictive control procedure, physical conservation properties (derived on the basis of the first law of thermodynamics) can be exploited in an algebraic consistency test that can be evaluated in real time in parallel to the computation of the control law. The derivation and implementation of such consistency tests is a topic of our current research.

References

[1]	Y. Cao. A Formulation of Nonlinear Model Predictive Control Using Automatic Differentiation. Journal of Process Control, 15:851--858, 2005.
[2]	Y. Cao and W.-H. Chen. Automatic Differentiation Based Nonlinear Model Predictive Control of Satellites Using Magneto-Torquers. In Proc. of IEEE Conf. on Industrial Electronics and Applications, ICIEA 2009, pages 913--918, Xi'an, China, 2009.
[3]	A. Rauh, J. Kersten, E. Auer, and H. Aschemann. Sensitivity Analysis for Reliable Feedforward and Feedback Control of Dynamical Systems with Uncertainties. In Proc. of 8th Intl. Conference on Structural Dynamics EURODYN 2011, Leuven, Belgium, 2011.
[4]	A. Rauh, J. Kersten, E. Auer, and H. Aschemann. Sensitivity-Based Feedforward and Feedback Control for Uncertain Systems. Computing, (2--4):357--367, 2012.

Attached files:

Stefan Kiel (Faculty of Engineering, INKO, University of Duisburg-Essen, Duisburg, Germany ), Ekaterina Auer (Faculty of Engineering, INKO, University of Duisburg-Essen, Duisburg, Germany ), Andreas Rauh (Chair of Mechatronics, University of Rostock, Germany): Application of Verified Optimization Techniques to Parameter Identification for Solid Oxide Fuel Cells

Abstract

Since the beginning of the 90’s at the latest, design and development of solid oxide fuel cells (SOFC) have been in the focus of research in the area of decentralized energy supply. SOFCs convert chemical energy directly into electricity and are highly efficient owing to the fact that the produced heat can be reused. On the one hand, they are flexible with respect to the kind of fuel. On the other hand, SOFCs are difficult to manufacture and require advanced control strategies for instationary operating points. Besides, their system parameters are influenced by significant uncertainty due to either measurement or model imprecision. An objective of a current research project between the Universities of Rostock and Duisburg-Essen is to develop dynamic SOFC models accurately describing their instationary behavior while accounting for the uncertainty with the help of interval-based verified methods.

Interval methods guarantee the correctness of results obtained using a computer and allow us to represent bounded epistemic uncertainty in a natural way. Their main disadvantages are possible overestimation and comparative slowness, which makes their use in real-life scenarios challenging. In this presentation, we show how to apply a verified optimization algorithm based on [2] to identify parameters of a dynamic model for the thermal SOFC subsystem derived in [3]. The model takes into account preheated air and fuel gas supplied to the SOFC system as well as the corresponding reaction enthalpies. The parameters of interest describe the thermal resistances of the stack materials, the dependency of the heat capacities on the temperature, and the heat produced during the exothermic electrochemical reactions in each individual fuel cell. We consider different model dimensions resulting in different ODE systems and cost functions. Although the obtained results are not always entirely verified since optimality of candidates for system parameterizations cannot always be rigorously proved, they can be shown to be more accurate than the results of corresponding MATLAB simulations. The accuracy is an important issue in this case, because better parameterizations facilitate more precise control.

Since the structure of the cost function for parameter identification is complex, we use our own implementation of the optimization algorithm in the framework UniVerMec [1], which currently allows for the maximum degree of flexibility and adjustment to the problem. Besides, it parallelizes the process of parameter identification reducing the overall computing time. However, these times are still high. As an outlook, we show how the GPU can be used to decrease them further. This is not an easy task since there are no interval libraries for the GPU as of now. Another problem is that double precision computations on the GPU are significantly slower than single precision ones. In this presentation, we examine how single precision GPU computations influence the quadratic cost function for our optimization problem which is generally affected by cancelation. We conclude the talk by a summary of the main results and a perspective on our future research.

References

[1]	E. Dyllong and S. Kiel. A Comparison of Verified Distance Computation between Implicit Objects Using Different Arithmetics for Range Enclosure. Computing, 2011.
[2]	E. Hansen and G. W. Walster. Global Optimization Using Interval Analysis. Marcel Dekker, New York, 2004.
[3]	A. Rauh, T. Dötschel, E. Auer, and H. Aschemann. Interval Methods for Control-Oriented Mod- o eling of the Thermal Behavior of High-Temperature Fuel Cell Stacks. In Proc. of SysID 2012, 2012. Accepted.

Attached files: