En informatique, la notion de ressource est une notion centrale. Nous considérons comme ressource toute entité pouvant être composée ou décomposée en sous-entités. Plusieurs logiques ont été proposées afin de modéliser et d’exprimer des propriétés sur celles-ci, comme la logique BI exprimant des propriétés de partage et de séparation. Puisque les systèmes informatiques manipulent des ressources, la proposition de nouveaux modèles capturant la dynamique de ces ressources, ainsi que la vérification et la preuve de propriétés sur ces modèles, sont des enjeux cruciaux. Dans ce contexte, nous définissons de nouvelles logiques permettant la modélisation logique de la dynamique des ressources, proposant de nouveaux modèles et permettant l’expression de nouvelles propriétés sur cette dynamique. De plus, pour ces logiques, nous proposons des méthodes des tableaux et d’extraction de contre-modèles. Dans un premier temps, nous définissons de nouveaux réseaux de Petri, nommés ß-PN, et proposons une nouvelle sémantique à base de ß-PN pour BI. Puis nous proposons une première extension modale de BI, nommée DBI, permettant la modélisation de ressources ayant des propriétés dynamiques, c’est-à-dire évoluant en fonction de l’état courant d’un système. Ensuite, nous proposons une logique, nommée DMBI, modélisant des systèmes manipulant/produisant/consommant des ressources. Par ailleurs, nous proposons une nouvelle logique (LSM) possédant de nouvelles modalités multiplicatives (en lien avec les ressources). Pour finir, nous introduisons la séparation au sein des logiques épistémiques, obtenant ainsi une nouvelle logique ESL, exprimant de nouvelles propriétés épistémiques / In computer science, the notion of resource is a central concern. We consider as a resource, any entity that can be composed or decomposed into sub-entities. Many logics were proposed to model and express properties on these resources, like BI logic, a logic about sharing and separation of resources. As the computer systems manipulate resources, a crucial issue consists in providing new models that capture the dynamics of resources, and also in verifying and proving properties on these models. In this context, we define new logics with new models and new languages allowing to respectively capture and express new properties on the dynamics of resources. Moreover, for all these logics, we also study the foundations of proof search and provide tableau methods and counter-model extraction methods. After defining new Petri nets, called ß-PN, we propose a new semantics based on ß-PN for BI logic, that allows us to show that BI is able to capture a kind of dynamics of resources. After observing that it is necessary to introduce new modalities in BI logic, we study successively different modal extensions of BI. We define a logic, called DBI, that allows us to model resources having dynamic properties, meaning that they evolve during the iterations of a system. Then, we define a logic, called DMBI, that allows us to model systems that manipulate/produce/consume resources. Moreover, we define a new modal logic, called LSM, having new multiplicative modalities, that deals with resources. Finally, we introduce the notion of separation in Epistemic Logic, obtaining a new logic, called ESL, that models and expresses new properties on agent knowledge

Cette thèse a pour objectif d’étudier les mécanismes par lesquels des expertises judiciaires sont conduites dans lecadre d’un procès afin d’assurer une recherche d’information préalable à la prise de décision du juge. Nous analysonsl’efficacité du recours à des mesures d’expertise en nous basant sur deux critères : le coût que les expertises font pesersur le système judiciaire et l’impact des expertises sur la qualité de la prise de décision du juge. Les travaux réalisésse divisent en quatre grands thèmes.Premièrement, nous étudions les incitations de l’expert judiciaire et nous mettons en évidence l’existence de problèmesd’aléa moral et de sélection adverse dans la relation qu’entretiennent le juge et l’expert. Deuxièmement, nous offronsune vue comparative de deux grandes catégories de procédures dans le contexte desquelles une expertise peut êtredemandée : la procédure inquisitoire et la procédure accusatoire. Notre objectif est de déterminer quelle procédureest préférable, compte tenu des deux critères d’évaluation de l’expertise judiciaire que nous avons précédemmentcités. Troisièmement, nous étudions spécifiquement le problème d’aléa moral existant dans la relation qui lie l’expertau juge, cette relation s’articulant autour du travail de recherche réalisé par le premier et du contrôle exercé par lesecond. Quatrièmement, nous mettons en évidence que des conflits d’intérêts de la part de l’expert, ou l’utilisationd’une méthodologie biaisée dans la conduite de ses travaux d’expertise, peuvent entraîner des erreurs dans la prise dedécision. Dans ce contexte, nous tentons de déterminer dans quelle mesure la présence d’un mécanisme d’appel peutpermettre de réduire les effets pervers d’un potentiel biais dans les résultats de l’expertise. / The objective of this thesis is to study the mechanisms by which an expert, who is appointed by the judge or by aparty to search evidence, may contribute to increase the quality of the judicial decision-making. We use two criteriato study how the use of experts may benefit to the judicial decision-making : the cost of expertise and the cost oferrors due to incorrect decisions by the judge. Our work is divided into four chapters.Firstly, we study the judicial expert’s incentives and we highlight the existence of moral hazard and adverse selectionproblems in the relationship between the judge and the expert. Secondly, we offer a comparative view of two differentcategories of procedure in which experts may be appointed : the inquisitorial procedure and the adversarial procedure.Thirdly, we study more specifically the relationship between the judge and the expert, when the judge exerts a controleffort and the expert exerts a research effort. Finally, we highlight the consequences of potential conflicts of interestsfrom the expert, or the consequences of a bias in the methodology used to conduct the expertise. Such conflicts ofinterests or bias may create some errors in the decision-making. In this context, we investigate how the presence ofan appeal mechanism may reduce the adverse effects of a potential bias in the results of the expertise.