eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-04-27
9471
1
24
10.4230/DagSemProc.09471.1
article
09471 Abstracts Collection – Computer-assisted proofs - tools, methods and applications
Brown, Malcolm B.
Kaltofen, Erich
Oishi, Shin'ichi
Rump, Siegfried M.
From 15.11. to 20.11.2009, the Dagstuhl Seminar 09471 ``Computer-assisted proofs - tools, methods and applications '' was held
in Schloss Dagstuhl~--~Leibniz Center for Informatics.
During the seminar, several participants presented their current
research, and ongoing work and open problems were discussed. Abstracts of
the presentations given during the seminar as well as abstracts of
seminar results and ideas are put together in this paper. The first section
describes the seminar topics and goals in general.
Links to extended abstracts or full papers are provided, if available.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09471/DagSemProc.09471.1/DagSemProc.09471.1.pdf
Verification methods
computer algebra
computer-assisted proofs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-04-27
9471
1
0
10.4230/DagSemProc.09471.2
article
09471 Executive Summary – Computer-assisted proofs - tools, methods and applications
Brown, Malcolm B.
Kaltofen, Erich
Oishi, Shin'ichi
Rump, Siegfried M.
From November 15-20, 2009, the Dagstuhl seminar on "Computer-assisted proofs - tools, methods and applications" continued a series of previous successful seminars. Participants from 10 different countries presented recent results in verification methods, computer algebra, and other computer-assisted-proof related areas.
We had lively talks and discussions, during the regular times for talks, during meals and afterwards. In the following links to abstracts and/or the presentation are given were applicable.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09471/DagSemProc.09471.2/DagSemProc.09471.2.pdf
Verification methods
computer algebra
computer-assisted proofs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-04-27
9471
1
28
10.4230/DagSemProc.09471.3
article
Interval Approaches to Reliable Control of Dynamical Systems
Rauh, Andreas
Auer, Ekaterina
Recently, we presented an implementation of interval-based algorithms which can be applied in real-time to control dynamical processes and to estimate internal states and disturbances. The approach is based on verified methods for sets of algebraic equations, ordinary differential equations as well as differential-algebraic equations. Due to this fact, the same program code can be used for two different tasks. On the one hand, we can use it online to estimate non-measurable internal system states which are necessary for nonlinear model-based control strategies. On the other hand, we can verify the admissibility and feasibility of these control strategies offline.
Although we use the same code for the online and offline tasks, there is an important difference between them. While the computing time is of minor importance in offline applications, we have to guarantee that the necessary online computations are completed successfully in a predefined time interval. For that reason, the role of verification is slightly different depending on the task. In offline applications, our goal is to compute tightest possible bounds for the sets of all solutions to the control problem under consideration. In contrast to that, we restrict the online mode to a search for a single solution that matches all demands on feasibility of control inputs and admissibility of the trajectories of the state variables in a reliable way.
To highlight the practical applicability of the underlying computational routines, we present the following cases for the use of verified solvers in real-time [1-3].
Case 1: Direct computation of feedforward control strategies with the help of differential-algebraic equation solvers. In this application, both verified and non-verified solvers can be used to determine open-loop control strategies for a dynamical system such that its output coincides with a predefined time response within given tolerances. This procedure corresponds to a numerical inversion of the dynamics of the system to be controlled. In this case, verified solvers are used to prove the existence of a control law within given physical bounds for the admissible range of the system inputs.
Case 2: If measured data and their time derivatives are available, the same procedures as in case 1 can be used to estimate non-measured state variables as well as non-measurable disturbances. Since the verified algorithms used in this context are capable of propagating bounded measurement uncertainties, the quality of the state and disturbance estimates can be expressed in terms of the resulting interval widths. Moreover, assumptions about the parameters and the structure of the underlying model can be verified.
Case 3: Routines for verified sensitivity analysis provide further information on the influence of variations of control inputs on the trajectories of the state variables. We present novel procedures implementing a sensitivity-based framework for model-predictive control. These procedures can be integrated directly in a feedback control structure.
Sometimes it is necessary to combine verified and non-verified algorithms to solve a given control problem. In this case, it is important to certify the results of the algorithm appropriately. Based on the four-tier hierarchy presented in earlier works [4], we develop a measure for characterizing such mixed approaches.
The presentation is concluded with simulation and experimental results for the example of temperature control of a distributed heating system.
[1] Rauh, Andreas; Auer, Ekaterina: Applications of Verified DAE Solvers in Engineering, Intl. Workshop on Verified Computations and Related Topics, COE Lecture Note Vol. 15: Kyushu University, pp. 88-96, Karlsruhe, Germany, 2009.
[2] Rauh, Andreas; Menn, Ingolf; Aschemann, Harald: Robust Control with State and Disturbance Estimation for Distributed Parameter Systems, Proc. of 15th Intl. Workshop on Dynamics and Control 2009, pp. 135-142, Tossa de Mar, Spain, 2009.
[3] Rauh, Andreas; Auer, Ekaterina; Aschemann, Harald: Real-Time Application of Interval Methods for Robust Control of Dynamical Systems, CD-Proc. of IEEE Intl. Conference on Methods and Models in Automation and Robotics MMAR 2009, Miedzyzdroje, Poland, 2009.
[4] Auer, Ekaterina; Luther, Wolfram: Numerical Verification Assessment in Computational Biomechanics, in A. Cuyt, W. Krämer, W. Luther, P. Markstein: Numerical Validation in Current Hardware Architectures, LNCS 5492, pp. 145-160, Springer-Verlag, Berlin, Heidelberg, 2009.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09471/DagSemProc.09471.3/DagSemProc.09471.3.pdf
Robust control
Ordinary differential equations
Differential-algebraic equations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-04-27
9471
1
22
10.4230/DagSemProc.09471.4
article
Verification and Validation for Femur Prosthesis Surgery
Auer, Ekaterina
Cuypers, Roger
Dyllong, Eva
Kiel, Stefan
Luther, Wolfram
In this paper, we describe how verified methods we are developing
in the course of the project TellHim&S (Interval Based Methods
For Adaptive Hierarchical Models In Modeling And Simulation Systems)
can be applied in the context of the biomechanical project PROREOP
(Development of a new prognosis system to optimize patient-specific pre-
operative surgical planning for the human skeletal system). On the one
hand, it includes the use of verified hierarchical structures for reliable geometric
modeling, object decomposition, distance computation and path
planning. On the other hand, we cover such tasks as verification and validation
assessment and propagation of differently described uncertainties
through system models in engineering or mechanics.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09471/DagSemProc.09471.4/DagSemProc.09471.4.pdf
Graphical interface construction
superquadrics
3D modeling
biomedical engineering