Specifications, constraints and Proofs

Permanents staff

• 2 Professors: Jean-François Dufourd and Pascal Schreck
• 4 Assistant professors: Caroline Essert, Nicolas Magaud, Pascal Mathis, Julien Narboux

Other participants

• 1 Associate researcher: Gabriel BRAUN (MC UFR LSHA, 09/2009-)
• 1 Maître de conférence en délégation CNRS: Laurent FUCHS (MC Poitiers, 09/2010-09/2011)
• 3 Post-doctoral: Claire BAEGERT (ATER, 01/2010-08/2010), Christophe BRUN (ATER, 01/2011-08/2011), Simon THIERRY (ATER, 10/2010-08/2011)
• 1 PhD students: Rémi IMBACH (Ministère, 10/2010-)
• 3 Former PhD students: Claire BAEGERT (Région Alsace-IRCAD, 10/2005-12/2009), Christophe BRUN (Ministère, 12/2007-12/2010), Simon THIERRY (Ministère, 10/2006-09/2010).

Specification and constraint solving

The specification of data objects from their dimensions (distances, angles, tangencies, indicences) is a important issue in the field of design and computer aided design (CAD). It is closely related to the production of figures meeting the constraint system given by users. Since the 80s, several methods have been developed to solve geometrical constraint systems. There are three main approaches: numerical methods that solve iteratively equation systems, methods based on graph to make planning and the rule-based approach that solve systems constructively (ruler and compass construction). These latter lead to a formalization of the geometry on which our team has always worked. There are also symbolic algebraic methods such Gröbner bases, but their complexity usually disqualifies them for CAD systems.

Two main features have guided the work of experts in the field in recent years:

• the large size and sparse character of constraint systems
• displacement invariance (or more generally by groups of transformations)

The first point has led teams interested in the decomposition of constraint systems and the second to reflect the displacment invariance in these decompositions. We then obtain special methods that do not necessarily resemble the methods of flow encountered in the methods of decomposition of equation systems.

These issues of invariance and decomposition have been theorized by our team (see MATH10), which helped to develop methods taking into account several groups. A implementation was made ​​in the form of a multi-agent system that combine several different solvers. Moreover, a probabilistic approach has led us to suggest an incremental method to decompose constraint systems (work done in collaboration with Dominique Michelucci, / MSTF10).

The problem of decomposition of geometric constraint systems often implies that the isolated subsystems are well-constrained modulo a given transformation group. Indeed, the classical solvers usually only manage systems with a finite number of solutions, possibly after quotiented the solution space by an equation related to the action of a transformation group. Unfortunately, many simple examples show that in 3D, the decomposition is no more convenient: most of the polyhedra are rigid and generically indecomposable. Therefore in the thesis of Arnaud Fabre, we are interested in a notion of quasi-decomposability in which we allow in a first step the change of the constraint system. Constraints removed in this step are then caught up by using a numerical method (see FASC07 and / Publications/2008/FASC08 / FASC08).

Following that approach led to consider under-constrained systems (TSMF08 and [http:// lsiit-cnrs.unistra.fr/Publications/2007/TMS07 / TMS07]). It was the issue addressed in the thesis of Thierry Simon (THIE10), whose purpose was to study under-constriction of constraint systems and their specific transformation groups. An original approach has also been established by Simon Thierry who can solve (in some sense) system constraints under or even over-constrained (see THIE11 / THIE11).

Formalisation and planning of surgical interventions

In these works, we propose an original approach to assist automatically the planning of a position of a surgical tool. Our method allows for elaborating an optimal strategy of intervention, specific to the patient and to the type of intervention, thanks to an automatic computation which is based on the expertise of the field and the preoperative data.

To this end, we put into play some approaches coming from declarative modeling and geometric constraint solving, to compute automatically optimal trajectories for rigid and straight surgical tools. The comutation of the trajectory is performed in several steps. First, the expertise of the surgeon on a given type of intervention is transcribed under the form of mathematical equations (equalities, cost functions). Then those equations are formalized into geometric constraints, written under the form of terms combining geometric and arithmetic operators and the data coming from the medical images (MRI, CT). A first computation solves the so-called "strict" geometric constraints (boolean constraints) to provide the space of possible solutions. Finally a second computation solves the so-called "soft" geometric constraints called (numerical constraints) thanks to a numerical optimization, to provide the optimal solution.

We tested our approaches on 2 types of interventions : the ablation of hepatic tumors by radiofrequency (hyperthermia) in collaboration with Pr. Gangi from the service of radiology of the Hôpital Civil of Strasbourg, and the implantation of electrodes of deep brain stimulation in collaboration with Dr. Haegelen from the service of neurosurgery of Renn's University hospital Pontchaillou.

The PhD thesis of Claire Baegert dealt with this topic 8-Baeg09. Various papers were published regarding radiofrequency 4-EBS09, 2-BESS07, 4-BESS07, 4-BESS07b, 4-BESS07c and deep brain stimulation 4-EHJ10. These works also leaded to a collaboration with DKFZ Heidelberg on the acceleration of occlusions solving thanks to GPU 5-ESFR10, 2-SESR11.

These works gave rise to the ANR project ACouStiC, which started in january 2011 for 4 years, and in which IGG team is a partner. This research topic is part of the IHU of Strasbourg.

Perspectives

Specification and constraint solving

To solve geometric constraint systems, our team mainly worked on geometrical methods. Besides their ability to provide all the solutions, they offer a diagnostic failure. However, geometrical approaches fail in solving some specific 2D cases and many 3D problems.

So, we go on to study reparametrization consisting in the transformation of a system S into a system S' that can be solved geometrically. Solutionx of S are computed from solutions of S' with numerical methods. This current work addresses two problems. The first concerns the relationship between the transformation of a system and its decomposition in order to facilitate the numerical solving. The second concerns the adaptation of numerical methods based on all available geometric information (the sketch provided by the user, the construction plan produced by the resolution).

Besides this work which attempts to combine the numerical methods used in industry and geometric method preferred by the academic world, we work on the implementation of a solver framework. This work is based on a description language for constraint systems, both their syntax as their semantics, initiated some years ago by the team.

Formalisation and planning of surgical interventions

Regarding surgical interventions planning, in the framework of ACouStiC project among others, we are beginning an extension of the field of possible solutions, by studying curved, multiple and volumetric trajectories. This will allow us to extend the posible applications to deformable surgical tools, within deformable tissues, or multiple tools used simultaneously (for instance cryoablation of hepatic tumors), or even access volumes such as craniotomy in the context of exeresis of cerebral lesions. We will also work on constrained surgical navigation within the solution space, in order to restrain the interactive modification of the proposed trajectory into a space of possible/reasonable solutions. To this end, the link will be done with "Visualization and interactions" axis of our team, in particular the haptic interfaces topic.