Séminaires LIRICA

- Le 17/10/2022 à 14h à St Charles, FRUMAM, 2ème étage

Orateur : Van-Giang Trinh (LIRICA)

Titre : Minimal trap spaces of Boolean models are maximal siphons of their Petri net encoding

Résumé : Boolean modelling of gene regulation but also of other biological systems has had great successes over the last ~20 years. Besides simulation, the analysis of such models is mostly based on attractor computation, since those correspond roughly to observable biological phenotypes. The recent use of trap spaces made a real breakthrough in that field allowing to consider medium-sized models that used to be out of reach. However, with the continuing increase in model-size, the state-of-the-art computation of minimal trap spaces based on prime-implicants shows its limits as there can be a huge number of implicants.
In this research, we present an alternative method to compute minimal trap spaces, and hence complex attractors, of a Boolean model. It replaces the need for prime-implicants with a completely different technique, namely the enumeration of maximal siphons in the Petri net encoding of the original model. After some technical preliminaries, we expose the concrete need for such a method and detail its implementation using Answer Set Programming. We then demonstrate its efficiency and compare it to implicant-based methods on several large Boolean models from the literature.

- Le 03/10/2022 à 14h à St Charles, FRUMAM, 2ème étage

Orateur : Nicola Olivetti (LIRICA)

Titre : A Journey in intuitionistic Modal Logic: normal and non-normal modalities

Résumé : Modal extensions of intuitionistic logic have a long history going back to the work by Fitch in the 40’ [6]. Two traditions are now consolidated, called respectively Intuitionistic Modal Logic and Constructive Modal logic. Each of the two has its own motivation and is more natural than the other from some standpoint. In the former tradition originated by Fischer- Servi [5] and systematized by Simpson [9], the basic system is IK, whereas in the tradition of constructive modal logics the two basic systems are Wijesekera’ systems WK [10] and the system CK by Bellin et als. [1]. Constructive modal logic are non-normal modal logics. In the classical setting, non-normal modal logics have been studied for a long time for several purposes (see [2], [8]). The observation that constructive modal logics are non-normal and the interest in non-normal modalities in itself leads to the question: which are the intuitionistic analog of classical non-normal modal logic?
It turns out that the framework of intuitionistic non-normal modal logic is richer than the classical one. In particular different interactions between the two modalities 2 and 3 give rise to distinct systems; some of them do not have a counterpart in the classical case. The resulting picture is a lattice of 24 non-normal modal logics with an intuitionistic base each of them determined by a cut-free sequent calculus.
Similarly to classical non-normal modal logics, all systems of non-normal intuitionistic modal logic are characterized by a simple neighbourhood semantics. Moreover the neighbourhood semantics helps to understand also Constructive modal logics CK and WK, as it covers also these systems.
The interest of the neighbourhood semantics for constructive modal logic can also be justified from a proof-theoretical perspective, as it witnessed by some recently introduced unprovability calculi for these logics. In these calculi, each derivation precisely corresponds to one neighbour- hood countermodel, whereas there is no direct correspondence with relational models. This fact confirms the usefulness and the naturalness of neighbourhood semantics for analysing in- tuitionistic modal logics.
[Joint work with Tiziano Dalmonte and Charles Grellois.]

- Le 19/09/2022 à 14h à St Charles, FRUMAM, 2ème étage

Orateur : Giulio Guerrierri (LIRICA)

Titre : Understanding the lambda-calculus via (non-)linearity and rewriting

Résumé : The lambda-calculus is the model of computation underlying functional programming languages and proof assistants. Actually, there are many lambda-calculi, depending on the evaluation mechanism (e.g., call-by-name, call-by-value, call-by-need) and computational features that the calculus aims to model (e.g., plain functional, non-deterministic, probabilistic, infinitary).
The existence of different paradigms is troubling because one apparently needs to study the theory and semantics of each one separately.
We propose a unifying and uniform meta-theory of lambda-calculi, where the study is rooted on a unique core language, the bang calculus, a variant of the lambda-calculus inspired by Girard's linear logic and Levy's Call-by-Push-Value: a bang operator marks which resources can be duplicated or discarded.
The bang calculus subsumes both call-by-name and call-by-value. A property studied in the bang calculus is automatically translated in the corresponding property for the call-by-name lambda-calculus and the call-by-value lambda-calculus, thanks to two different embeddings of the lambda-calculus in the bang calculus. These embeddings are grounded on proof theory, via Curry-Howard: they are an adaptation of Girard's two translations of intuitionistic logic into linear logic.
Advanced computational features are usually obtained by adding new operators to a core language. Instead of studying the operational properties of the extended language from scratch, we propose a simple method to study them modularly: if an operational property holds in the core language and in the new operators separately, then a simple test of good interaction between core language and new operators guarantees that the property lifts to the whole extended language. This approach is first developed in abstract rewriting systems.

- Le 13/07/2022 à 10h à St Charles, FRUMAM, 2ème étage

Orateur : Trinh Van Giang (LIRICA)

Titre : Minimal trap spaces of Boolean models are maximal siphons of their Petri net encoding

- Le 13/06/2022 à 14h en visio et à St Charles, FRUMAM, 2ème étage

Orateur : Marianna Girlando (University of Birmingham, UK)

Titre : Cyclic proofs, hypersequents and Transitive Closure Logic

Résumé : Transitive Closure Logic (TCL) enriches the language of first order logic with a recursive operator, expressing the transitive closure of a binary relation. Cyclic sequent calculi proofs for this logic have been introduced in the literature. In this talk, I will present a new cyclic proof system for TCL, which employs hypersequents. The main motivation behind this work is that, differently from sequent TCL proofs, hypersequent proofs for TCL successfully simulate cyclic proofs in the transitive fragment of Propositional Dynamic Logic (PDL+), without using the non-analytic rule of cut.
After introducing the cyclic hypersequent calculus for TCL, I will present two main results. First, I will sketch a proof of soundness for the calculus, which requires a more involved argument than the one used in traditional cyclic proofs. Second, I will show how PDL+ cyclic proofs can be translated into TCL hypersequent proofs. This result allows to lift the completeness result for cyclic PDL+ to the hypersequent calculus.
This talk is based on joint work with Anupam Das.

- Le 30/05/2022 à 14h en visio

Orateur : Raphaëlle Crubillé (LIRICA)

Titre : Sémantique dénotationelle pour les langages de programmation probabilistes

Résumé : La sémantique dénotationelle est un champs de recherche centré sur la construction de modèles mathématiques des langages de programmation, visant à produire des techniques de preuve pour l'équivalence de programmes. Dans les dix dernières années, l'usage des probabilités pour la programmation a été transformé par les développements en programmation statistique et en apprentissage, ce qui a stimulé un intérêt renouvelé pour les méthodes formelles pour des langages probabilistes. Cet exposé présente un bref panorama de la sémantique dénotationelle des langages de programmation probabilistes, en tentant d'expliciter à la fois ses enjeux, ses outils et ses perspectives.

- Le 09/05/2022 à 14h en visio

Orateur : José-Luis Vilchis-Medina (Ecole navale, Brest)

Titre : Autonomous Decision-Making with Incomplete Information and Safety Rules based on Non-Monotonic Reasoning

Résumé : In this seminar, we will present a decision process integrating Non-Monotonic Reasoning (NMR), embedded in a deliberative architecture. The NMR process uses Default Logic to implement goal reasoning, managing partially observable or incomplete information, allowing the design of default behaviours completed by the handling of specific situations, in order to manage the current mission objective as well as safety rules. We illustrate our approach through an application of an underwater robot performing a marine biology mission.

- Le 25/04/2022 à 14h en visio et à St Charles, FRUMAM, 2ème étage

Orateur : Tarek Khaled (LIRICA)

Titre : De la conception d'un système ASP au traitement des données biologiques

Résumé : La programmation par ensemble réponse (Answer Set Programming, ASP) est un paradigme de programmation déclaratif basé sur la sémantique des modèles stables. L'idée derrière ASP est de coder un problème donné comme un ensemble de règles logiques, les modèles stables obtenus à partir du programme logique constituent les solutions du problème initial. La grande expressivité de l'ASP, combinée au nombre croissant d'applications, ont fait de l’ASP un sujet de recherche majeur.
Dans cet exposé, nous présentons la manière dont nous avons exploité une nouvelle sémantique de programme logique pour la conception d'un nouveau système ASP. Cette sémantique nous a donné la possibilité de calculer tous les modèles stables d'un programme logique ainsi que les modèles extra-stables. Ces modèles extra-stables correspondent aux extra-extensions de la nouvelle sémantique qui ne sont pas capturées par la sémantique des modèles stables. La méthode que nous proposons effectue un processus énumératif booléen adapté à l’ ASP et à la nouvelle sémantique. Elle a l’avantage de travailler sur une représentation sous forme de clauses de Horn ayant la même taille que le programme logique d’entrée et travaille à espace constant. En plus, l’énumération est effectuée sur un ensemble restreint de littéraux du programme logique représentant son "strong backdoor".Dans la suite de cet exposé, nous aborderons l'utilisation de programmes logiques et d'ASP pour exprimer et traiter des réseaux de régulation génique considérés comme des réseaux booléens, et nous présenterons des méthodes permettant de détecter tous les attracteurs dans ces réseaux. Les attracteurs sont essentiels dans l'analyse de la dynamique d'un réseau booléen. Ils expliquent pourquoi une cellule particulière peut acquérir des phénotypes spécifiques qui peuvent être transmis sur plusieurs générations. Nous présentons d'abord comment représenter et traiter les réseaux booléens généraux pour les modes de mise à jour synchrone et asynchrone. Ensuite, nous faisons une présentation du cas particulier des réseaux circulaires. Ce dernier cas spécifique joue un rôle essentiel dans les systèmes vivants. Nous avons montré plusieurs propriétés théoriques; en particulier, les attracteurs simples des réseaux de gènes sont représentés par les modèles stables des programmes logiques correspondants et les attracteurs cycliques par leurs modèles extra-stables.

- Le 04/04/2022 à 14h en visio et à St Charles, FRUMAM, 2ème étage

Orateur : Federico Olimpieri (Leeds, UK)

Titre : A categorical approach to resource approximation

Résumé : In recent years, the semantics of linear logic has lead to the development of powerful tools for the analysis of quantitative and qualitative aspects of computation. The notion of resource approximation arose in this context and it consists in the study of the computational behavior of programs via an appropriate kind of approximations. An important example of this is given by linear approximations of lambda-terms. These approximations are resource-sensitive programs, that use exactly once their input during computation. I will present some relevant results in this field from my general perspective rooted in the categorical semantics of programming languages.

- Le 21/03/2022 à 14h en visio

Orateur : Sophie Paillocher (IBISC, Evry)

Titre : Complétion de modèles partiellement étiquetés pour la logique LTL

Résumé : Un problème important dans le processus de conception et réalisation d’un système informatique critique est de tester automatiquement si un modèle abstrait donné du système vérifie ou non une spécification donnée, exprimée dans un langage logique. Ce problème, connu sous le nom de « Model Checking » est usuellement étudié dans le cadre où le modèle abstrait est entièrement construit.
Toutefois des scénarios existent où l’information dont l’on dispose à propos du système est partielle. En effet, le système peut être seulement partiellement construit, ou bien la possibilité d’observation du système peut être limitée.
Dans ce contexte deux problèmes émergent :
• Peut-on compléter le modèle partiel de façon à obtenir un modèle entièrement construit respectant une spécification donnée ?
• Peut-on s’assurer que le modèle respectera une spécification donnée, peut importe l’information manquante?
Ici nous considérerons les modèles comme étant des systèmes de transitions dont les états sont étiquetés par des informations sur les propositions atomiques. Le cadre logique sera quant-à lui celui de la logique LTL. De plus nous restreindrons l’information manquante aux seules étiquettes. La structure du modèle partiel (états et transitions) donné en entrée restera donc inchangée lors de la complétion.
Nous commencerons par analyser les problèmes de complétion, et en particulier par énoncer des résultats de complexité. Puis nous présenterons une méthode générale, inspirée de la méthode des tableaux, afin de les résoudre.

- Le 07/03/2022 à 14h en visio et à St Charles, FRUMAM, 2ème étage

Orateur : Ezgi Iraz SU

Titre : Recent Epistemic Extensions of Equilibrium Logic

Résumé : Answer set programming (ASP) is a well-established paradigm for declarative logic programming and nonmonotonic reasoning. Thanks to its efficient solvers, ASP performs as a successful logic-based problem-solving technique and is especially useful for difficult combinatorial search problems with optimisation.
Here-and-there logic (HT) is a nonclassical (three-valued) monotonic logic which is intermediate between classical logic and intuitionistic logic, and it is closely aligned with ASP:
(i) First, Pearce’s equilibrium logic provides a purely logical framework for ASP. Its semantics, via equilibrium models, is based on a truth-minimisation criterion over HT models. The way of choosing such minimal models among HT models of a formula turns equilibrium logic into a nonmonotonic reasoning formalism.
(ii) Second, HT characterises an important notion of ASP. To spell it out, strong equivalence of ASP programs can be captured by logical equivalence of corresponding HT theories (i.e., sets of HT formulas).
In this talk, we first make a short introduction to the above-mentioned formalisms with a focus on equilibrium logic. Then, we discuss the recent epistemic extensions of equilibrium logic. Among these, the main approach is to integrate (reflexive) autoepistemic logic and equilibrium logic in order to insert the introspective reasoning of the former to the latter. Autoepistemic logic is an important form of nonmonotonic reasoning, allowing a rational agent to reason about her own knowledge. It extends classical propositional logic by an epistemic modal operator. Autoepistemic logic and its reflexive extension are respectively identical to the nonmonotonic variants of the modal logics KD45 and SW5. Their minimal models reflect minimisation of knowledge. Thus, equilibrium models of (reflexive) autoepistemic equilibrium logics respect both knowledge and truth minimality. Today, they are considered the most successful approach among the existing semantics for epistemic ASP; yet the definition of a rigorous and understandable semantics for epistemic operators in the language of ASP is still subject of ongoing research.

- Le 11/02/2022 à 10h en visio (séminaire commun DALGO-LIRICA)

Orateur : Jérémy Ledent

Titre : Simplicial Models for Multi-Agent Epistemic Logic

Résumé : Epistemic Logic is the modal logic of knowledge. It allows to reason about a finite set of agents who can know facts about the world, and about what the other agents know. The traditional Kripke-style semantics for epistemic logic is based on graphs whose vertices represent the possible worlds, and whose edges indicate the agents that cannot distinguish between two worlds. In this talk, I will present an alternative semantics for epistemic logic, based on combinatorial topology. The idea is to replace the Kripke graph by a simplicial complex, allowing for higher-dimensional connectivity between the possible worlds. In fact, every Kripke model can be turned into an equivalent simplicial model, thus uncovering its underlying geometric structure. Our notion of simplicial model is inspired from the "protocol complex" approach to distributed computing. I will show how our framework can be used to analyse distributed computing, where the agents are the processes, and the possible worlds are all the possible executions of the system. In order to prove impossibility results, one must find an epistemic logic formula representing the knowledge that the processes should acquire in order to solve a task; and argue that such knowledge cannot be achieved. This is joint work with Éric Goubault and Sergio Rajsbaum

- Le 10/01/2022 à 14h en visio et à St Charles, FRUMAM, 3ème étage

Orateur : Pierre Clairambault (LIRICA)

Titre : Games with no Winner: an Introduction to Game Semantics

Résumé : How to define rigorously the behaviour of programs under execution? Program semantics is a necessary first step in order to prove that a program or program transformation is correct, and is of course a preliminary to any theoretical question on programming languages. Game semantics is one of many approaches to program semantics. It represents a program by recording the exchange of observable computational events with its execution environment, phrased as a play in a two-player game that the program plays with its context. In game semantics there is no winner: it is about the journey, not the destination!
Most of my talk will be an introduction to game semantics. I will first focus on some old (but nice) results, namely the so-called « semantic cube » following which game semantics exactly captures the observable behaviour of programs with various computational effects (notably, mutable state and non-local control). I will show how this allows one to prove results about computational effects and their interferences.
Time permitting, I will then talk about some of my own recent work on a game semantics for concurrent programs. The semantics builds on so-called « true concurrency » models such as event structures, and provides a causal description of the behaviour of concurrent programs with rich computational features.

- Le 22/11/2021 à 14h à St Charles, FRUMAM, 3ème étage

Orateur : Erkko Lehtonen (Universidade Nova de Lisboa)

Titre : Clonoids of Boolean functions

Résumé : A clonoid is a class of functions of several arguments that is stable under right and left compositions with fixed clones. In this talk, we discuss first steps towards Post-like complete descriptions of clonoids of Boolean functions. We provide a brief introduction to the topic and present some motivations for studying clonoids.

- Le 28/06/2021 à 11h en visio

Orateur : Van-Giang TRINH (Tokyo, Japan)

Titre : An FVS-based Approach to Attractor Detection in Asynchronous Boolean Networks

Résumé : Boolean Networks (BNs) play a crucial role in modeling and analyzing biological systems. One of the central issues in the analysis of BNs is attractor detection, i.e., identification of all possible attractors. This problem becomes more challenging for large Asynchronous Boolean networks (ABNs) because of the asynchronous and non-deterministic updating scheme. In this research, we formally state and prove several relations between Feedback Vertex Sets (FVSs) and dynamics of BNs. From these relations, we propose an FVS-based method for detecting attractors in ABNs. Our approach relies on the principle of removing arcs in the state transition graph to get a candidate set and the reachability property to filter the candidate set. We formally prove the correctness of the proposed method, and then show its efficiency by conducting experiments on real biological networks and randomly generated N-K networks. The obtained results are very promising, since our method can handle large networks whose sizes are up to 101 without using any network reduction technique. This advanced computation capability can enable biologists to conduct more accurate analysis on large networks, then discover more biological insights.

- Le 31/05/2021 à 14h en visio

Orateur : Ezgi Iraz SU

Titre : Recent Epistemic Extensions of Answer Set Programming

Résumé : Answer set programming (ASP) is a well-established paradigm for declarative programming and nonmonotonic reasoning. Accordingly, it serves as a successful method of problem-solving in knowledge representation and reasoning. However, today it is widely accepted by the logic programming community that ASP requires a more powerful introspective reasoning with the use of epistemic modalities. Although there has been a long-lasting debate among researchers about how to correctly extend ASP with epistemic modal operators, there is still no agreement on a fully satisfactory semantics that is able to offer intuitive results for epistemic logic programs (ELPs). To carry this discussion on a more formal level, Cabalar et al. have recently proposed some candidate structural criteria that successful semantics approaches for ELPs are supposed to satisfy. These are mainly the epistemic extensions of ASP’s well-known principles of constraint monotonicity, splitting, and foundedness.
In this talk, we first give a brief survey of ASP’s recent epistemic extensions, and if time permits, then we also shortly discuss these formal properties.

- Le 26/04/2021 à 14h en visio

Orateur : Wesley Fussner

Titre : Ortholattices résiduels comme nouvelle approche de la logique quantique

Résumé : Cet exposé passe en revue nos récentes tentatives d'étudier le raisonnement quantique à l'aide des outils des logiques sous-structurelles. Nous introduisons les ortholattices résiduels comme des modèles algébriques généralisant les modèles habituels de la logique quantique, et illustrons qu'ils donnent une version `intuitioniste' de la logique quantique dans laquelle la logique quantique classique peut être interprétée par une traduction à double négation.