La littérature fait état des travaux de recherches qui ont été menés pour la résolution des problèmes d'ordonnancement de production. La complexité de ces problèmes rend nécessaire l'emploi de stratégies de recherche de solutions évoluées. Parmi celle-ci figure le formalisme du calcul propositionnel, le plus souvent sous forme normale conjonctive (FNC) associé au problème de satisfiabilité (SAT). Le présent travail de recherche a pour but d'intégrer les formalismes d'approches de résolution des problèmes SAT pour la résolution du problème d'ordonnancement de production, soit le problème d'ordonnancement de véhicules, proposé dans le cadre du challenge ROADEF'2005. Dans un premier temps, les principaux algorithmes pour la résolution de problème SAT sont présentés, particulièrement les algorithmes basés sur le retour en arrière tels que le retour-arrière (Backtracking) et le retour ponctuel (Backjumping) étendus sur les TL-clauses (True-Literal clauses). Ce travail de recherche couvre le développement de trois approches de résolutions du problème SAT appliquées au problème d'ordonnancement de véhicules. Pour chaque approche un encodage en FNC/TL traduisant les contraintes du problème ainsi que l'objectif à optimiser sont effectués. Ces FNC/TL sont générées en format DIMACS à l'aide du logiciel développé par l'auteur. Ensuite, une stratégie de résolution est décrite, en fixant à chaque fois l'objectif à optimiser. Dans la première approche, le problème est traité globalement. Les deux autres approches subdivisent le problème initial en sous-problèmes. Finalement une comparaison des trois approches est décrite. Les instances du problème proposées par le challenge ROADEF'2005 sont utilisées comme base d'évaluation des approches développées. Les résultats obtenus sont comparés aux meilleurs résultats obtenus par le gagnant du challenge ROADEF'2005, à l'aide du logiciel suggéré par le challenge, soit exeCarSeq. Une analyse détaillée des résultats montre que notre stratégie de résolution du problème d'ordonnancement de véhicules est une voie prometteuse. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Forme normale conjonctive, Problème de satisfiabilité, Problème d'ordonnancement de véhicules, TL-clauses, Encodage en FNC/TL.

La démocratisation des ordinateurs, des téléphones portables et surtout de l'Internet a considérablement révolutionné le monde de la communication. Les besoins en matière de cryptographie sont donc plus nombreux et la nécessité de vérifier la sûreté des algorithmes de chiffrement est vitale. Cette thèse s'intéresse à l'étude d'une nouvelle cryptanalyse, appelée cryptanalyse logique, qui repose sur l'utilisation de la logique propositionnelle - à travers le problème de satisfaisabilité - pour exprimer et résoudre des problèmes cryptographiques. Plus particulièrement, les travaux présentés ici portent sur une certaine catégorie de chiffrements utilisés dans les protocoles d'authentification et d'intégrité de données qu'on appelle fonctions de hachage cryptographiques. Un premier point concerne l'aspect modélisation d'un problème cryptographique en un problème de satisfaisabilité et sa simplification logique. Sont ensuite présentées plusieurs façons pour utiliser cette modélisation fine, dont un raisonnement probabiliste sur les données du problème qui permet, entres autres, d'améliorer les deux principaux points d'une attaque par cryptanalyse logique, à savoir la modélisation et la résolution. Un second point traite des attaques menées en pratique. Dans ce cadre, la recherche de pré-Image pour les fonctions de hachage les plus couramment utilisées mènent à repousser les limites de la résistance de ces fonctions à la cryptanalyse logique. À cela s'ajoute plusieurs attaques pour la recherche de collisions dans le cadre de la logique propositionnelle. / Democratization of increasingly high-Performance digital technologies and especially the Internet has considerably changed the world of communication. Consequently, needs in cryptography are more and more numerous and the necessity of verifying the security of cipher algorithms is essential.This thesis deals with a new cryptanalysis, called logical cryptanalysis, which is based on the use of logical formalism to express and solve cryptographic problems. More precisely, works presented here focuses on a particular category of ciphers, called cryptographic hash functions, used in authentication and data integrity protocols.Logical cryptanalysis is a specific algebraic cryptanalysis where the expression of the cryptographic problem is done through the satisfiabilty problem, fluently called sat problem. It consists in a combinatorial problem of decision which is central in complexity theory. In the past years, works led by the scientific community have allowed to develop efficient solvers for industrial and academical problems.Works presented in this thesis are the fruit of an exploration between satisfiability and cryptanalysis, and have enabled to display new results and innovative methods to weaken cryptographic functions.The first contribution is the modeling of a cryptographic problem as a sat problem. For this, we present some rules that lead to describe easily basic operations involved in cipher algorithms. Then, a section is dedicated to logical reasoning in order to simplify the produced sat formulas and show how satisfiability can help to enrich a knowledge on a studied problem. Furthermore, we also present many points of view to use our smooth modeling to apply a probabilistic reasoning on all the data associated with the generated sat formulas. This has then allowed to improve both the modeling and the solving of the problem and underlined a weakness about the use of round constants.Second, a section is devoted to practical attacks. Within this framework, we tackled preimages of the most popular cryptographic hash functions. Moreover, the collision problem is also approached in different ways, and particularly, the one-Bloc collision attack of Stevens on MD5 was translated within a logical context. It's interesting to remark that in both cases, logical cryptanalysis takes a new look on the considered problems.

Le problème de satisfaisabilité booléenne 3-SAT est connu pour présenter un phénomène de seuil en fonction du quotient entre le nombre de clauses et le nombre de variables. Nous donnons des estimations de la valeur de ce seuil au moyen de méthodes combinatoires et probabilistes: la méthode du premier moment et la méthode du second moment. Ces méthodes mettent en jeu des problèmes d'optimisation sous contraintes et nous amènent à employer de façon intensive la méthode des multiplicateurs de Lagrange. Nous mettons en œuvre une forme pondérée de la méthode du premier moment sur les affectations partielles valides de Maneva ainsi que des variantes. Cela nous conduit à élaborer une pondération générale pour les problèmes de satisfaction de contraintes qui soit compatible avec la méthode du premier moment. Cette pondération est constituée d'une graine et d'un répartiteur, et nous permet d'obtenir une pondération des affectations partielles valides meilleure que celle de Maneva. Nous comparons aussi dans certains cas les performances de la pondération et de l'orientation de l'espace des solutions des problèmes de satisfaction de contraintes relativement à la méthode du premier moment. Nous développons la première sélection non uniforme de solutions pour majorer le seuil de 3-SAT et nous montrons sa supériorité sur ses prédécesseurs. Nous construisons un cadre général pour appliquer la méthode du second moment à k-SAT et nous discutons des conditions qui la font fonctionner. Nous faisons notamment fonctionner la méthode du second moment sur les solutions booléennes et sur les impliquants. Nous étendons cela au modèle distributionnel de k-SAT.

Dans cette thèse, nous nous intéressons à la spécification et à la synthèse de contrôleurs des systèmes temps-réels. Les modèles pour ces systèmes sont des Event-recording Automata. Nous supposons que les contrôleurs observent tous les évènements se produisant dans le système et qu'ils peuvent interdirent uniquement des évènements contrôlables. Tous les évènements ne sont pas nécessairement contrôlables. Une première étude est faite sur la logique Event-recording Logic (ERL). Nous proposons des nouveaux algorithmes pour les problèmes de vérification et de satisfaisabilité. Ces algorithmes présentent les similitudes entre les problèmes de décision cités ci-dessus et les problèmes de décision similaires étudiés dans le cadre du $\mu$-calcul. Nos algorithmes corrigent aussi des algorithmes présents dans la litérature. Les similitudes relevées nous permettent de prouver l'équivalence entre les formules de ERL et les formules de ERL en forme normale disjonctive. La logique ERL n'étant pas suffisamment expressive pour décrire certaines propriétés des systèmes, en particulier des propriétés des contrôleurs, nous introduisons une nouvelle logique WTmu. La logique WTmu est une extension temps-réel faible du $\mu$-calcul. Nous proposons des algorithmes pour la vérification des systèmes lorsque les propriétés sont écrites en WTmu. Nous identifions un fragment de WTmu appelé WTmu pour le contrôle (C-WTmu). Nous proposons un algorithme qui permet de vérifier si une formule de C-WTmu possède un modèle. Cet algorithme n'a pas besoin de connaître les ressources (horloges et constante maximale comparée avec les horloges) des modèles. En utilisant C-WTmu comme langage de spécification des systèmes, nous proposons des algorithmes de décision pour le contrôle centralisé et le $\Delta$-contrôle centralisé. Ces algorithmes permettent aussi de construire des modèles de contrôleurs.

Le développement de circuits électroniques et de systèmes logiciels critiques pour le ferroviaire ou l’avionique, par exemple, demande à être systématiquement associé à un processus de vérification formelle permettant de garantir l’exhaustivité des tests. L’approche formelle la plus répandue dans l’industrie est le Model Checking. Le succès de son adoption provient de deux caractéristiques : (i) son aspect automatique, (ii) sa capacité à produire un témoin (un scénario rejouable) lorsqu’un comportement indésirable est détecté, ce qui fournit une grande aide aux concepteurs pour corriger le problème. Néanmoins, la complexité grandissante des systèmes à vérifier est un réel défi pour le passage à l’échelle des techniques existantes. Pour y remédier, différents algorithmes de model checking (e.g., parcours symbolique des états du système, interpolation), diverses méthodes complémentaires (e.g., abstraction,génération automatique d’invariants), et de multiples procédures de décision(e.g., diagramme de décision, solveur SMT) sont envisageables.Dans cette thèse, nous nous intéressons plus particulièrement à l’induction temporelle.Il s’agit d’un algorithme de model checking très utilisé dans l’industrie pour vérifier les systèmes critiques. C’est également l’algorithme principal de l’outil développé au sein de l’entreprise Safe River, entreprise dans laquelle cette thèse a été effectuée. Plus précisément, l’induction temporelle combine deux techniques :(i) BMC (Bounded Model Checking), une méthode très efficace pour la détection debugs dans un système (ii) k-induction, une méthode ajoutant un critère de terminaison à BMC lorsque le système n’admet pas de bug. Ces deux techniques génèrent des formules logiques propositionnelles pour lesquelles il faut en déterminer la satisfaisabilité.Pour se faire, nous utilisons un solveur SAT, c’est-à-dire une procédure de décision qui détermine si une telle formule admet une solution.L’originalité des travaux proposés dans cette thèse repose en grande partie sur la volonté de renforcer la collaboration entre le solveur SAT et le model checker.Nos efforts visent à accroître l’interconnexion de ces deux modules en exploitant la structure haut niveau du problème. Nous avons alors défini des méthodes profitant de la structure symétrique des formules. Cette structure apparaît lors du dépliage successif de la relation de transition, et nous permet de dupliquer les clauses ou encore de déplier les transitions dans différentes directions (i.e., avant ou arrière). Nous avons aussi pu instaurer une communication entre le solveur SAT et le model checker permettant de : (i) simplifier la représentation au niveau du model checker grâce à des informations déduites par le solveur, et (ii) aider le solveur lors de la résolution grâce aux simplifications effectuées sur la représentation haut niveau. Une autre contribution importante de cette thèse est l’expérimentation des algorithmes proposées. Cela se concrétise par l’implémentation d’un model checker prenant en entrée des modèles AIG (And-Inverter Graph) dans lequel nous avons pu évaluer l’efficacité de nos différentes méthodes. / The design of electronic circuits and safety-critical software systems in railway or avionic domains for instance, is usually associated with a formal verification process. More precisely, test methods for which it is hard to show completeness are combined with approaches that are complete by definition. Model Checking is one of those approaches and is probably the most prevalent in industry. Reasons of its success are mainly due to two characteristics, namely: (i) its fully automatic aspect, and (ii) its ability to produce a short execution trace of undesired behaviors, which is very helpful for designers to fix the issues. However, the increasing complexity of systems to be verified is a real challenge for the scalability of existing techniques. To tackle this challenge, different model checking algorithms (e.g., symbolic model checking, interpolation), various complementary methods (e.g., abstraction, automatic generation of invariants) and multiple decision procedures (e.g., decision diagram, SMT solver) can be considered. In this thesis, we particularly focus on temporal induction. It is a model checking algorithm widely used in the industry to check safety-critical systems. This is also the core algorithm of the tool developed within SafeRiver, company in which this thesis was carried out. More precisely, temporal induction consists of a combination of BMC (Bounded Model Checking) and k-induction. BMC is a very efficient bugfinding method. While k-induction adds a termination criterion to BMC when the system does not admit bugs. These two techniques generate formulas for which it is necessary to determine their satisfiability. To this end, we use a SAT solver as a decision procedure to determine whether a propositional formula has a solution. The main contribution of this thesis aims to strengthen the collaboration between the SAT solver and the model checker. The improvements proposed mainly focus on increasing the interconnections of these two modules by exploiting the high-level structure of the problem.We have therefore defined several methods taking advantage of the symmetrical structure of the formulas. This structure emerges during the successive unfolding of the transition relation, and allows us to duplicate clauses or even unroll the transitions in different directions (i.e., forward or backward). We also established a communication between the solver and the model checker, which has for purpose to: (i) simplify the model checker representation using the information inferred by the solver, and (ii) assist the solver during resolution with simplifications performed on the high-level representation. Another important contribution of this thesis is the empirical evaluation of the proposed algorithms on well-established benchmarks. This is achieved concretely via the implementation of a model checker taking AIG (And-Inverter Graph) as input, from which we were able to evaluate the effectiveness of our algorithms.

Parmi les différentes formes de raisonnement étudiées dans le contexte de l'intelligence artificielle, le raisonnement qualitatif permet d'inférer de nouvelles connaissances dans le contexte d'informations imprécises, incomplètes et dépourvues de valeurs numériques. Il permet par exemple de déduire de nouvelles informations à partir d'un ensemble d'informations spatiales telles que « la France est frontalière de l'Allemagne », « la Suisse est à l'est de la France », « l'Italie est en Europe » et « le Luxembourg est proche de la France ». Il peut également être utilisé pour résoudre des abstractions de problèmes quantitatifs difficiles à résoudre, afin par exemple d'accélérer la résolution de ces problèmes.De nombreux formalismes de raisonnement qualitatif ont été proposés dans la littérature. Ils ne se focalisent cependant que sur un seul aspect du monde, alors que la majorité des applications requièrent la prise en compte d'informations hétérogènes. Afin de répondre à ces besoins, plusieurs combinaisons et extensions de formalismes qualitatifs, comme le raisonnement spatio-temporel et le raisonnement multi-échelle, ont récemment été proposées dans la littérature. Le raisonnement spatio-temporel permet de raisonner dans le contexte d'informations spatiales et temporelles interdépendantes. Le raisonnement multi-échelle permet de raisonner avec des informations de précisions différentes, et en particulier de lever des incohérences apparentes.Dans cette thèse, nous nous intéressons au raisonnement multi-échelle, au raisonnement spatio-temporel et aux combinaisons de formalismes qualitatifs.Nous proposons d'étendre le raisonnement qualitatif temporel multi-échelle pour prendre en compte le fait que les intervalles de temps peuvent être perçus comme des instants à certaines échelles de précision, de formaliser intégralement ce raisonnement et d'étudier la décision de la cohérence dans ce contexte ainsi que sa complexité. Nous montrons en particulier que ce formalisme permet de décider la cohérence et que le problème de décision de la cohérence est NP-complet, même dans le cas le plus simple.En outre, nous proposons un cadre général permettant de raisonner sur les séquences temporelles d'informations qualitatives, une forme de description spatio-temporelle. Ce cadre permet notamment de raisonner dans le contexte d'évolutions complexes. Par exemple, les entités considérées peuvent avoir des caractéristiques préservées au cours du temps, évoluer de manière dépendante les unes par rapport aux autres, tout en ayant un comportement potentiellement irréversible et différent selon leur nature. De plus, dans ce cadre, le raisonnement est plus performant computationnellement que les approches de l'état de l'art. Nous étudions en particulier la décision de la cohérence dans le contexte spécifique de régions mobiles de taille constante, et montrons que ce cadre permet effectivement de décider la cohérence.De surcroît, nous proposons un cadre formel unifiant plusieurs formes d'extensions et de combinaisons de formalismes qualitatifs, incluant le raisonnement multi-échelle et les séquences temporelles. Ce cadre permet de raisonner dans le contexte de chacune de ces combinaisons et extensions, mais également d'étudier de manière unifiée la décision de la cohérence et sa complexité. Nous établissons en particulier deux théorèmes complémentaires garantissant que la décision de la cohérence est polynomiale, et nous les utilisons pour prouver que plusieurs fragments de séquences temporelles sont traitables.Nous généralisons également la définition principale de formalisme qualitatif afin d'inclure des formalismes qualitatifs exclus des définitions de la littérature, importants dans le cadre des combinaisons. / In this thesis, we are interested in qualitative multi-scale reasoning, qualitative spatio-temporal reasoning and combinations of qualitative formalisms.We propose to extend the multiscale temporal reasoning to take into account the fact that time intervals can be perceived as instants at certain scales of precision, to fully formalize this reasoning and to study its consistency problem. We show in particular that this formalism decides consistency and that the consistency problem is NP-complete, even in the simplest case.In addition, we propose a general framework for reasoning on temporal sequences of qualitative information, a form of spatio-temporal description. This framework allows for reasoning in the context of complex evolutions. For example, the considered entities may have characteristics preserved over time, evolve in a dependent manner with respect to each other, while having a potentially irreversible and different behavior depending on their nature. Moreover, in this context, reasoning is computationally more efficient than state-of-the-art approaches. In particular, we study the consistency problem in the specific context of constant-size moving regions, and show that this framework actually decides consistency.Furthermore, we propose a formal framework unifying several forms of extensions and combinations of qualitative formalisms, including multi-scale reasoning and temporal sequences. This framework allows one to reason in the context of each of these combinations and extensions, but also to study in a unified way the consistency problem. In particular, we establish two complementary theorems guaranteeing that the consistency problem is polynomial, and we use them to prove that several fragments of temporal sequences are tractable.

Dans cette thèse, nous nous intéressons à la spécification et à la synthèse de contrôleurs des systèmes temps-réels. Les modèles pour ces systèmes sont des Event-recording Automata. Nous supposons que les contrôleurs observent tous les évènements se produisant dans le système et qu'ils peuvent interdirent uniquement des évènements contrôlables. Tous les évènements ne sont pas nécessairement contrôlables. Une première étude est faite sur la logique Event-recording Logic (ERL). Nous proposons des nouveaux algorithmes pour les problèmes de vérification et de satisfaisabilité. Ces algorithmes présentent les similitudes entre les problèmes de décision cité ci-dessus et les problèmes de décision similaires étudiés dans le cadre du $\mu$-calcul. Nos algorithmes corrigent aussi des algorithmes présents dans la littérature. Les similitudes relevées nous permettent de prouver l'équivalence entre les formules de ERL et les formules de ERL en forme normale disjonctive. La logique ERL n'étant pas suffisamment expressive pour décrire certaines propriétés des systèmes, en particulier des propriétés des contrôleurs, nous introduisons une nouvelle logique WT$_\mu$. La logique WT$_\mu$ est une extension temps-réel faible du $\mu$-calcul. Nous proposons des algorithmes pour la vérification des systèmes lorsque les propriétés sont écrites en WT$_\mu$. Nous identifions deux fragments de WT$_\mu$ appelés WT$_\mu$ bien guardé ($WG$-WT$_\mu$) et WT$_\mu$ pour le contrôle ($C$-WT$_\mu$). La logique $WG$-WT$_\mu$ est plus expressif que $C$-WT$_\mu$. Nous proposons un algorithme qui permet de vérifier si une formule de $WG$-WT$_\mu$ possède un modèle (éventuellement déterministe). Cet algorithme nécessite de connaître les ressources (horloges et constante maximale comparée avec les horloges) des modèles. Dans le cadre de $C$-WT$_\mu$ l'algorithme que nous proposons et qui permet de décider si une formule possède un modèle n'a pas besoin de connaître les ressources des modèles. En utilisant $C$-WT$_\mu$ comme langage de spécification des systèmes, nous proposons des algorithmes de décision pour le contrôle centralisé et le $\Delta$-contrôle centralisé. Ces algorithmes permettent aussi de construire des modèles de contr\^oleurs. Lorsque les objectifs de contrôle sont décrits à l'aide des formules de $WG$-WT$_\mu$, nous montrons également comment synthétiser des contrôleurs décentralisés avec des ressources fixées à l'avance et ceci, lorsqu'au plus un contrôleur est non déterministe. / In this dissertation, we consider the specification and the controller synthesis problem for real-time systems. Our models for systems are kinds of Event-recording automata. We assume that controllers observe all the events occurring in the system and can prevent occurrences of controllable events. We study Event-recording Logic (ERL). We propose new algorithms for the model-checking and the satisfiability problems of that logic. Our algorithms are similar to some algorithms proposed for the same problems in the setting of the standard $\mu$-calculus. They also correct earlier proposed algorithms. We define disjunctive normal form formulas and we show that every formula is equivalent to a formula in disjunctive normal form. Unfortunately, ERL is rather weak and can not describe some interesting real-time properties, in particular some important properties for controllers. We define a new logic that we call WT$_\mu$. The logic WT$_\mu$ is a weak real-time extension of the standard $\mu$-calculus. We present an algorithm for the model-checking problem of WT$_\mu$. We consider two fragments of WT$_\mu$ called well guarded WT$_\mu$ ($WG$-WT$_\mu$) and WT$_\mu$ for control ($C$-WT$_\mu$). We show that the satisfiability of $WG$-WT$_\mu$ is decidable if the maximal constants appearing in models are known a priori. Our algorithm allows to check whether a formula of $WG$-WT$_\mu$ has a deterministic model. The algorithm we propose to decide whether a formula of $C$-WT$_\mu$ has a model does not need to know the maximal constant used in models. All the algorithms for the satisfiability checking construct witness models. Using $C$-WT$_\mu$, we present algorithms for a centralised controller synthesis problem and a centralised $\Delta$-controller synthesis problems. The construction of witness controllers is effective. We also consider the decentralised controller synthesis problem with limited resources (the maximal constants used in controllers is known a priory) when the properties are described with $WG$-WT$_\mu$. We show that this problem is decidable and the computation of witness controllers is effective.

Ce mémoire est constitué de 3 parties.La NP-complétude de la satisfaction de combinaisons booléennes de contraintes de sous-arbres est démontrée dans l'article [Ven87] ; la partie I de ce mémoire étudie dans quelle mesure l'ajout de contraintes régulières laisse espérer conserver la complexité NP. Ce modèle étendu définit une nouvelle classe de langages dont l'expressivité est comparée à celle des Rigid Tree Automata [JKV11]. Puis un début de formalisation des t-dags est donné.Les patterns ont été étudiés, principalement du point de vue des contraintes sur les données qu'ils demandent. La partie II de ce mémoire les étudie plus finement, en mettant de côté les données. Les squelettes sont définis en tant qu'intermédiaire de calcul et le fait que leur syntaxe caractérise leur sémantique est démontré. Puis un lemme de pompage est donné dans un cas restreint, un autre dans le cas général est étudié et conjecturé. Ensuite des fragments de combinaisons booléennes de patterns sont comparés en expressivité pour terminer avec l'étude de la complexité des problèmes de model-checking, satisfaisabilité et DTD-satisfaisabilité sur les dits fragments.Le contenu de la partie III constitue l'article [FMS11], c'est la démonstration de la caractérisation des langages des automates fortement déterministes de niveau 2 par des systèmes d'équations récurrentes caténatives. Celle-ci utilise, entre autres, des techniques de réécriture, la notion d'inconnues non-réécrivables et les ordres noethériens. Cette caractérisation constitue le cas de base de la récurrence démontrée dans [Sén07]. / This thesis is in 3 parts.The NP-completeness of satisfiability of boolean combinations of subtree constraints is shown in the article [Ven87] ; in the part I of this thesis, we study whether adding regular contraints lets hope for keeping the same complexity. This extended model defines a new class of languages which is compared in expressivity to the Rigid Tree Automata [JKV11]. Then a begining of formalisation of the t-dags is developped.The patterns have been studied mainly from the point of view of the constraints they demand on the data. The part II of this thesis study them more finely, by putting aside the data. The skeletons are defined as calculus intermediate and the characterisation holding between their syntax and their semantics is shown. Then a pumping lemma is prooved in a restreict case, another one is conjectured in the most general case. Then fragments of boolean combinations of patterns are compared in expressivity, this parts ends with the study of complexity of model-checking, satisfiability and DTD-satisfiability on these fragments.The content of part III constitutes the article [FMS11], it is the demonstration of the characterisation of strongly-deterministic 2-level pushdown automata by recurrent catenative equation systems. This proof uses in particular, some rewriting techniques, unrewritable unknowns and noetherian orders. This characterisation provides the base case of the recurrence shown in [Sén07].