The work of the LILaC research group aims to model intelligent systems based on theories and techniques from knowledge representation, logic, game theory, argumentation, and verification techniques. The LILaC team conducts projects and research in the following areas:
An important aspect of interaction is the dynamics of the environment, caused by the execution of events and actions that affect the mental states of agents (through their observations or perceptions). In this aspect, the LILaC team is interested in:
- logics of action such as dynamic logic, whose formal properties are studied such as completeness, decidability, complexity);
- revision and updating, to take into account new information, especially in the multiagent case;
- algorithms for reasoning on actions, in particular the study of the formal properties (consistency, modularity) of theories of action and events and their evolution.
In an open environment, the interaction between agents needs to be protected.
This protection can be declined in the form of three properties: availability, integrity, confidentiality. Starting from the formal specification of a system, the LILaC team is interested, on the one hand, to provide proof that this system verifies the three properties above, and, on the other hand, to obtain automatically an implementation which corresponds to the specification and whose correction is proven by construction.
- At the level of access control, the challenge is to extend the model of the access control matrix and to draw the limit between decidability and undecidability of the problem of security in extended models;
- At the level of protocol checking, the challenge is to define algorithms to automatically check protocols that will allow agents to guarantee the confidentiality or integrity of the information they exchange.
The protection of a system is also studied by modeling (in terms of roles and relations between users) the organization in which a computer system is inserted:
- It is then necessary to characterize both the predicative aspects of the notion of role and its deontic aspects, which make use of the concepts of permission and obligation, which are also the basis of other notions such as trust, responsibility, or delegation.
The LILaC team is interested in the social mechanisms that govern the interactions between agents (artificial or human). In particular:
- voting theory, which provides an important model of interaction, particularly for multi-agent systems, and where the use of logic makes it possible to specify and verify these systems;
- the theory of epistemic games and the logic for games;
- the theory of the diffusion of opinion and the phenomenon of social influence.
While most of the above research is theoretical, simulations are often implemented to test the different mechanisms developed in a variety of situations.
While the goal of the LILaC team is to develop a general model of interaction based on logic, its work also aim at integrating those models coming from the previous axes into a unified formalism. In particular, this challenge has been attacked with the use of BDI logics and logics of action, by constructing logics that speak to both the beliefs, desires, and intentions of agents, as well as the actions they can produce (also focusing on the evolution of agents’ beliefs). This high-level endeavor also considers argumentation as a model of reasoning based on interactions between arguments – the evaluation of the interactions makes it possible to determine collectively acceptable sets of arguments (extensions), or an order of acceptability between the arguments. The dynamics of argumentation systems, the definition of different modes of evaluation (argumentative semantics), and the links between argumentation and logic, are at the heart of the team’s current research.
Models of interaction among autonomous agents pose computational challenges and require the development of algorithms that able to answer to questions of the form “is a given formula a consequence of a given logical theory”? As specialists of non-classical logic, the LILaC team substantially renewed the tableaux method (completeness and complexity of logics admitting a Kripke semantic). On the practical side, this work has been implemented in the platform LoTREC, which offers a high-level programming language for the rapid definition of provers for all normal modal logics.
- we developed the TouIST platform, which constitutes an interface between a high-level propositional language and several solvers (SAT, SMTP, and more recently QBF);
- we translated (fragments) of given languages in a language usable by TouIST to automate proving procedures for which we do not have a dedicated prover;
- we implemented games for the search of a winning strategy;
- we studied epistemic planning of actions (cognitive robotics).
- Predictive police: a framework and a necessary transparencyLaurent Perrussel in the spotlight for his work on the predictive police. … Read more
- UT1C/LILaC members honored!Several members of the team are honored in the UT1C journal (in … Read more
- SCONE kick off meetingThe SCONE kick off meeting will take place on November 12th at … Read more
- Arianna’s PhD DefenseNote the date: November, 12 in the Arsenal (UT1C). Her webpage for … Read more
- Arrival of Rachael ColleyRachael Colley will join the team on October 1st for a duration … Read more
- IJCAI-19 Tutorial: Game Description Languages and LogicsThis tutorial gives an overview of Game Description Logics, a family of … Read more
- Arrival of Carlos Areces (Guest Researcher)Carlos Areces will be visiting researcher in the team from July 07 … Read more