Centre de Recherche en Informatique de Lens

PRISM - Platform for Reasoning with Inconsistency Shapley Measure

Stéphanie Roussel — 2013-04-19T07:26:49Z

PRISM stands for Platform for Reasoning with Inconsistency Shapley Measure.

Overview

PRISM is a java-based evolutive platform that allows to perform different reasoning tasks such as inference, belief revision or conciliation using MI Shapley inconsistency value. It can for instance be sued for academic purposes.

The idea is to use an inconsistency value for evaluating how much each formula of the belief base is responsible of the inconsistency of the base. Then this evaluation allows us to obtain a stratification (total pre-order) of the base, that can be used as the preferential input for different reasoning tasks, such as inference, belief revision, or conciliation. Obtained operators are interesting and have good logical properties. Several inference, revision and conciliation operators are already implemented in the platform but one can develop its own implementation and add it dynamically.

Downloads

The platform is available through the following jar : prism.jar.

Note that this jar also includes Sat4j core library (http://www.sat4j.org)

How to execute PRISM

JRE is required.

download prism.jar

execute the jar with the following command line "java -jar prism.jar"

License

PRISM is developed under the GNU GPL license. See LICENSE

How to

have access to the platform sources ?

Go to or create a repository that will be the one where the platform is deployed. Copy prism.jar to this repository and use the command line "jar xf prism.jar".

add its own implementation of an operator ?

First, deploy the platform sources as it is explained in the previous paragraph. Depending on the operation one wants to write, one needs to extend a specific abstract class. These classes and their respective packages are given in the following table.

Abstract classes to extend in order to implement its own operator
Tab	Abstract Class	Package
Shapley	ShapleyValueSet	model.computation.shapleyValue
Inference	InferenceOperator	model.inference.fromListFormulae
Revision	MssScoreAggregator	model.computation.mssScore
Revision	MssSelectionOperator	model.mssSelection
Revision	InferenceFromMSSOperator	model.inference.fromMSS
Conciliation	ChoiceOperator	model.conciliation.choice
Conciliation	WeakOperator	model.conciliation.weakening

The new operator should be in the same class as the abstract class it extends. This means that the package of the new class must be the same and that the java file should be moved to the repository corresponding to the package. Once the class is created, it has to be compiled with javac command : "javac /pathtotheclass/NewClass.java". Be careful to import all needed classes in order to compile... If the compilation is successful, the repository should contain a new file NewClass.class. In order to launch the platform and take into account the new classes, from the base repository, execute "java gui.TestGUI".

get the whole documentation

Javadoc for PRISM is available here and here. .

Contacts

Stéphanie Roussel, Research engineer at CRIL

stephanie.roussel@cril.fr

Please, let us know if you find any bug in the platform or if have suggestions to improve it.

Gestion de l'incertitude et codage des politiques de sécurités dans les systèmes de contrôle d'accès — PhD of Khalid Bouriche (in French)

Fabien Delorme — 2013-03-14T14:48:35Z

Le travail de cette thèse se situe à l'intersection du domaine de l'intelligence artificielle et du domaine de la sécurité informatique. Cette thèse a deux objectifs principaux : le premier est de confirmer la puissance expressive du modèle OTBAC, en particulier par rapport aux politiques de sécurité par défaut utilisées dans SELinux. Le deuxième objectif est d'étendre ce modèle OTBAC, en intégrant le concept de priorité qui sera représenté dans le cadre de la théorie des possibilités. Dans la première partie de la thèse, nous passons en revue et analysons les différents modèles du contrôle d'accès existants, y compris ceux utilisés dans les systèmes SELinux. En particulier, nous présentons le modèle OrBAC qui offre une représentation compacte et flexible des politiques de sécurité.

Dans la deuxième partie de la thèse, nous proposons une modélisation des politiques de sécurité par défaut, utilisées par SELinux, dans le modèle OTBAC. Nous montrons que chaque concept utilisé dans la politique de sécurité SELinux (type, rôle, etc.) possède une contrepartie naturelle dans le modèle OTBAC. Cette modélisation, illustré sur la distribution Selinux tedora74, confirme la puissance expressive du modèle de contrôle d'accès OTBAC. Nous proposons également la représentation et la gestion des règles de transition des politiques de sécurité SELinux dans le modèle OTBAC.

Dans la troisième et dernière partie de la thèse, nous nous intéressons à la gestion de l'incertitude dans les modèles de contrôle d'accès. Nous avons utilisé la théorie des possibilités qui offre un cadre naturel, qualitatif et ordinal pour représenter et raisonner avec les règles incertaines. Nous proposons une extension du modèle OrBAC en y introduisant une entité appelée priorité au niveau de chaque relation. L'entité priorité quantifie la certitude qu'une relation, entre une entité concrète et une entité abstraite, soit réalisée. Plusieurs modes de combinaison (pessimiste, optimiste et avancé) sont proposés pour déterminer la valeur de la priorité de chaque relation concrète à partir des priorités des relations abstraites correspondantes.

Apprentissage artificiel de règles de jeux de stratégie

Fabien Delorme — 2013-03-14T11:49:19Z

Début de la thèse : septembre 2013

Encadrants
Fred Koriche (koriche _AT_ cril.fr)
Sylvain Lagrue (lagrue _AT_ cril.fr)
Sébastien Tabary (tabary _AT_ cril.fr)

Rendre une machine capable de jouer et surtout de gagner à des jeux de société, apanage de l'intelligence humaine, a toujours été un challenge fascinant dans le domaine de l'Intelligence Artificielle (IA). En particulier, le General Game Playing (GGP) est la capacité́ pour un agent intelligent de bien jouer non pas à un jeu spécifique, comme Deep Blue aux échecs [5], mais à n'importe quel jeu. Les règles sont représentées de manière déclarative dans un langage de représentation des connaissances issu de la programmation logique, GDL (General Description Language) [1]. Cependant, les règles du jeu sont données au départ à l'agent qui ne peut rien faire sans elles : un défi actuel de l'IA est ainsi de permettre à un agent artificiel d'apprendre à jouer.

L'objectif central de ce sujet de thèse est de concevoir des algorithmes d'apprentissage, basés sur la programmation logique inductive [1,2], permettant d'assimiler les règles d'un jeu de stratégie à partir d'un ensemble de parties observées. Différents contextes d'apprentissages peuvent être envisagés. Dans un premier temps, l'agent possède une bibliothèque de règles de jeux et doit être capable d'apprendre les règles d'un nouveau jeu en révisant les règles d'un jeu similaire qu'il connaitrait déjà [3]. Dans un deuxième temps, l'agent pourrait poser différentes questions afin d'accélérer le processus d'apprentissage. Enfin, il pourrait apprendre non seulement à jouer, mais à « bien jouer ». Il sera judicieux pour cela d'étudier le lien avec la programmation par contraintes [4], en étudiant notamment l'identification et la prise en compte incrémentale de nouvelles contraintes (ou la modification de contraintes existantes) au sein d'un réseau de contraintes modélisant les règles du jeu

Ce sujet est à la frontière de grands champs de l'intelligence artificielle (jeux, apprentissage, représentation des connaissances, programmation par contraintes) et est de ce fait transversal aux différentes thématiques du laboratoire.

Liste des publications portant directement sur le sujet

[1] M. Genesereth, N. Love, B. Pell : General game playing, AI magazine 26(2), 2006

[2] L. De Raedt : Logical and Relational Learning, Springer, 2008.

[3] H. Katsuno and A. O. Mendelzon. Propositional knowledge base revision and minimal change. Artificial Intelligence,52:263 - 294, 1991.

[4] Francesca Rossi ; Peter Van Beek ; Toby Walsh (2006). Handbook of constraint programming. Elsevier

[5] Murray Campbell, A. Joseph Hoane Jr., and Feng-hsiung Hsu. Deep Blue. Artificial Intelligence, 134(1-2) :57–83, 2002. pages 9

Développement de cadres formels pour le raisonnement spatio-temporel

Fabien Delorme — 2013-03-14T07:16:00Z

Début de la thèse : septembre 2013

Clôture des candidatures le 10 mai 2013

Encadrants :

Jean-François Condotta (MCF-HDR, CRIL, condotta@cril.fr)

Bertrand Mazure (Professeur des universités, CRIL, mazure@cril.fr)

Yakoub Salhi (MCF, CRIL, salhi@cril.fr)

Sujet :

La représentation et le raisonnement sur le temps et l'espace est une tâche importante dans de nombreux domaines et applications de l'Intelligence Artificielle et plus généralement de l'Informatique. Parmi ces domaines et applications, nous pouvons citer la compréhension du langage naturel, les systèmes d'informations géographiques, les base de données spatio-temporelles, la navigation assistée, le contrôle du trafic aérien.

Dans la littérature, différentes approches ont été proposées afin de permettre de raisonner à la fois sur des informations temporelles et sur des informations spatiales. Parmi ces formalismes, des logiques combinant la logique temporelle PLTL [1] et des contraintes spatiales qualitatives issues de calculs tels que RCC8 [2] ou l'algèbre des directions cardinales [3] ont été proposées et étudiées [4,5]. Grâce à ces langages, nous pouvons par exemple représenter le fait qu'une région géographique a été, à un moment donné au cours du temps contenue par une autre région géographique ou bien encore qu'une entité ponctuelle en mouvement se déplace toujours vers sa droite dans le plan. Des études concernant le problème de la satisfiabilité d'une formule de ces logiques spatio-temporelles ont été réalisées et ont montré que ce problème est plus ou moins difficile en fonction des contraintes spatiales et des modalités temporelles considérées. Par exemple, en considérant un langage basé sur des contraintes du calcul des relations cardinales, ce problème est PSPACE-complet [5] tandis qu'en utilisant des contraintes issues de RCC8, nous pouvons avoir des fragments pour lesquels il est EXSPACE-complet [3]. Des fragments au pouvoir expressif intéressant ont été également caractérisés avec un problème de satisfiabilité NP-complet.

Le sujet de thèse proposé s'inscrit dans ce cadre et consiste au traitement des différents points suivants :
Définition et étude d'algorithmes permettant la résolution du problème de la satisfiabilité de certains fragments des logiques spatio-temporelles proposées dans la littérature.
Définition et étude de nouveaux formalismes spatio-temporelles. Ces formali-smes seront basés sur des langages de représentation définis à partir d'un langage logique et/ou de contraintes.

Références :

[1] A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32 :733–749, 1985.

[2] David A. Randell, Zhan Cui, and Anthony G. Cohn. A spatial logic based on regions and connection. Proceedings of the 3rd international conference on knowledge representation and reasoning (KR'92), pages 165–176. Morgan Kaufmann, 1992.

[3] Gérard Ligozat. Reasoning about cardinal directions. Journal of Visual Languages and Computing, 1(9) :23–44, 1998.

[4] F. Wolter and M. Zakharysachev. Spatio-temporel representation and reasoning based on RCC-8. Proc. of the 7th International Conference on the Principles of Knowledge Representation and Reasoning (KR), Breckenridge, USA, 2000.

[5] P. Balbiani and J.-F. Condotta. Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In Alessandro Armando, editor, Proceedings of the 4th InternationalWorkshop on Frontiers of Combining

Systems (FroCoS'02), volume 2309 of Lecture Notes in Computer Science, p 162–176. 2002.

Contributions aux problèmes SAT

Fabien Delorme — 2013-02-06T09:43:08Z

Titre : Contributions aux problèmes SAT.

Doctorant : MOHAMMAD SALEH BALASIM Al-Saedi.

Directeurs : Éric Grégoire, Bertrand Mazure et Lakhdar Saïs.

Compilation de connaissances : des formules logiques aux réseaux bayésiens

Fabien Delorme — 2013-02-06T09:33:03Z

Titre : Compilation de connaissances : des formules logiques aux réseaux bayésiens

Doctorant : Samuel Thomas

Directeur : Pierre Marquis et Fred Koriche

Co-encadrant : Jean-Marie Lagniez

Autour de la décision possibiliste qualitative

Fabien Delorme — 2013-02-06T09:31:41Z

Titre : Autour de la décision possibiliste qualitative

Doctorante : Ismahane Sid-Amar

Directeur : Salem Benferhat

Dynamique des Systèmes d'Argumentation

Fabien Delorme — 2013-02-06T09:28:25Z

Titre : Dynamique des Systèmes d'Argumentation

Doctorant : Jean-Guy Mailly

Directeurs : Sébastien Konieczny et Pierre Marquis

Co-encadrante : Sylvie Coste-Marquis

Parallélisation de systèmes de contraintes complexes

Fabien Delorme — 2013-02-06T09:26:53Z

Titre : Parallélisation de systèmes de contraintes complexes

Doctorante : Nebras Gharbi

Directeur : Christophe Lecoutre

Co-encadrants : Olivier Roussel et Fred Hemery

Changement de croyances et logiques modales

Fabien Delorme — 2013-02-06T09:25:19Z

Titre : Changement de croyances et logiques modales

Doctorant : Thomas Caridroit

Directeurs : Pierre Marquis et Sébastien Konieczny

Co-encadrant : Tiago de Lima

Centre de Recherche en Informatique de Lens

PRISM - Platform for Reasoning with Inconsistency Shapley Measure

Overview

Downloads

How to execute PRISM

License

How to

Contacts

Gestion de l'incertitude et codage des politiques de sécurités dans les systèmes de contrôle d'accès — PhD of Khalid Bouriche (in French)

Apprentissage artificiel de règles de jeux de stratégie

Début de la thèse : septembre 2013

Développement de cadres formels pour le raisonnement spatio-­temporel

Début de la thèse : septembre 2013

Encadrants :

Sujet :

Références :

Contributions aux problèmes SAT

Compilation de connaissances : des formules logiques aux réseaux bayésiens

Autour de la décision possibiliste qualitative

Dynamique des Systèmes d'Argumentation

Parallélisation de systèmes de contraintes complexes

Changement de croyances et logiques modales

Développement de cadres formels pour le raisonnement spatio-temporel