Welcome to LILaC team

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.

More recently:

  • 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).

Distinction | UPS | UT1C

4 accepted papers and a demo paper at IJCAI-ECAI22 from LILaC

ByUmberto Grandi

Congratulations to all authors of 4 accepted papers, a demo paper, and an invitation to an early career spotlight talk at IJCAI-ECAI 2022 (the main generalistic international conference in AI) which will be hosted in Vienna in July: Axiomatic Foundations of Explainability by Leila Amgoud and Jonathan Ben-Naim Preserving Consistency in Multi-Issue Liquid Democracy by Rachael Colley and Umberto Grandi

Read More

Seminar

LILAC PhD seminar

ByUmberto Grandi

Here is the calendar of the upcoming seminars by PhD students of the research group: Friday 26 February, 14:00 Saul Fernandez Gonzalez. Indexed Frames and Social Epistemic Logics.Jorge Luis Fernandez Davila. CoPains – An integrated framework for cognitive planning Friday 12 March, 14:00 Munyque Mittelmann. Strategic Reasoning in Automated Mechanism DesignRachael Colley. Judgment Aggregation with Weighted Issues Friday 2 April, 14:00Elise Perrotin.

Read More