Responsable : Giuseppe Di Molfetta / Shantanu Das
« Reachability in Vector Addition Systems is Not Elementary » par J. Leroux (LABRI)
« Locally definable vertex set properties are efficiently enumerable » par N. Creignou (LIS)
« Determinisation of Finitely-Ambiguous Copyless Cost Register Automata » par T. Lopez (LIS)
Orateur : J. Leroux (LABRI)
Titre : Reachability in Vector Addition Systems is Not Elementary
Orateur : N. Creignou (LIS)
Titre : Locally definable vertex set properties are efficiently enumerable
Orateur : T. Lopez (LIS)
Titre : Determinisation of Finitely-Ambiguous Copyless Cost Register Automata
« Dynamic epistemic logic for distributed computing – asynchrony and concurrency » par H. van Ditmarsch (LORIA)
« Non-normal modal logics: from models to proofs » par T. Dalmonte (LIS)
« Consistency Measures, Inconsistency Measures, and Mix Measures » par V. Risch (LIS)
Orateur : Tiziano Dalmonte, LIS
Titre : Non-normal modal logics: from models to proofs
Résumé : Modal logics are applied in many different contexts, such as epistemic, deontic or temporal reasoning, and many others. In some of these contexts, the minimal normal modal logic K leads to counter-intuitive conclusions, such as the problem of logical omniscience or the problem of conflicting obligations, and gives rise to several paradoxes (Ross paradox, the paradox of gentle murder, …). For this reason, weaker modal logics — called non-normal – are considered. Non-normal modal logics are traditionally characterised by a possible world semantics with a neighbourhood function. In this talk I present an alternative semantics which is more natural for systems lacking monotonicity. I also present some new proof systems which have ‘good’ properties, moreover they provide a decision procedure of optimal complexity and allow one to construct countermodels for non-valid formulas. In the final part I present some open problems.
Orateur : Vincent Risch (LIS)
Titre : Consistency Measures, Inconsistency Measures, and Mix Measures (Preliminary Report)
Résumé : En collaboration avec Philippe Besnard Abstract: We give some insight into a preliminary attempt at investigating a notion of consistency measures. These would provide a consistency degree for any finite collection of logical formulas, on a par with the well-known notion of inconsistency measures, that aim at assigning degrees of inconsistency to finite sets of logical formulas. We first propose a basic set of postulates for consistency measures. We look at a couple of relationships with inconsistency measures. We even lay grounds for a formal duality between these two domains. Lastly, we have a look at what would be a mix measure, that is, a measure that gives a degree, on the same scale, for consistency (positive values) and inconsistency (negative values). We also mention supermodels, as defined by Ginsberg et al., as well as a theory that can be regarded as a generalization of super-models, namely morpho-logics.
Orateur : Hans van Ditmarsch (LORIA)
Titre : Dynamic epistemic logic for distributed computing – asynchrony and concurrency
Résumé : We will present some recent work on asynchrony and concurrency in dynamic epistemic logics (DEL), building on foundations in distributed computing and temporal epistemic logics. Asynchrony can be modelled by reasoning over histories of actions of different length. How to do this in DEL was proposed by [Dégremont, Löwe, Witzel: TARK 2011]. By equivalence relations on protocol-generated forests along different depths of trees, they can identify action histories of different length. More or less strongly related to DEL this was also considered for: gossip protocols [Apt, Grossi, vd Hoek, TARK 2015], logic puzzles [vD, van Eijck, Wu: KR 2010], and for the immediate snapshot algorithm in distributed computing [Goubault, Ledent, Rajsbaum: GandALF 2018]. We will present the last in some detail: Kripke models and action models can be represented as simplicial complexes. Dynamic epistemic logic can then be interpreted on such complexes. From the perspective of dynamic epistemic logic, a further departure towards distributed computing and asynchrony is to distinguish the sending and receiving of messages, such as the making versus hearing of announcements. Recent proposals are [Knight, Maubert, Schwarzentruber; MSCS 2019] and [Balbiani, vD, Fernandez Gonzalez; ArXiV 2019] (SR 2017). From the latter we will present asynchronous announcement logic. Its axiomatization resembles that of public announcement logic, and the dynamic modalities can also be eliminated. Further research is on (what is known as) concurrent common knowledge. Finally, how do we model concurrency in DEL? Both true concurrency and intersection concurrency are conceivable. We recall some older work in the area: [vD, vd Hoek, Kooi: AAMAS 2003] and [van Eijck, Sietsma, Wang: JANCL 2011]. The Muddy Children Problem is a joy forever: the action of three muddy children not stepping forward because none of them know whether they are muddy, is always modelled as the public announcement of a conjunction with three conjuncts. Should this not be a concurrent action with three components?
« Distributed labeling schemes on metrically defined graphs » par S. Ratel (LIS)
« Fast Algorithms for Unit Disk Graphs » par G. Dias da Fonseca (LIS)
« Two open problems of Digital Geometry with convex lattice sets » par Y. Gérard (LIS)
Orateur : Sébastien Ratel (LIS)
Titre : Distributed labeling schemes on metrically defined graphs
Orateur : Guilherme Dias da Fonseca (MCF, LIS)
Titre : Fast Algorithms for Unit Disk Graphs
Résumé : Unit-disk graphs are graphs whose $n$ vertices correspond to unit disks in the plane and whose $m$ edges correspond to pairs of intersecting disks. \emph{Graph-based} algorithms receive as input solely the adjacency representation of the graph while geometric algorithms receive the coordinates of the disks. In this talk, we consider approximation algorithms to two classic hard optimization problems: maximum independent set and minimum dominating set. We are particularly interested in algorithms whose running times are close to linear in the input size, i.e. close to $O(n+m)$ for graph-based algorithms and close to $O(n)$ for geometric algorithms. We will discuss four different approaches to obtain such algorithms: greedy, local search, strip decomposition, and shifting coresets, comparing their performance for different problems and graph classes. This work is based on multiple papers co-written by the author with Celina M. H. de Figueiredo, Vinicius G. Pereira de Sá, Raphael Machado, Gautam K. Das, and Ramesh K. Jallu.
Orateur : Yan Gerard (PR, UCA)
Titre : Two open problems of Digital Geometry with convex lattice sets
Résumé : A lattice set of $Z^d$ is digital convex if its real convex hull does not contain any other integer point than the ones of S. Problem 1: recognition of digital polyhedra. A n-digital polyhedron is the intersection of the lattice $Z^d$ with a polyhedron of $R^d$ with at most $n$ faces. Given $n$ and a convex lattice set $S$, we want to determine whether $S$ is a $n$-digital polyhedron. In dimension $d=2$, with $n=3$, the question is to determine whether there exists a triangle $T$ whose intersection with the lattice is $S$. Whatever the value of $n$, it is a very natural question related to polyhedral separability but it is still undetermined whether it is decidable in the cases where $d>3$ and $S$ is hollow (hollow means that the interior of its convex hull does not contain any integer point). Problem 2: Discrete Tomography We consider the problem of reconstruction of convex lattice sets (or HV-convex polyominoes) from their horizontal and vertical X-rays or projections. In other words, we know the number of points of a convex lattice set $S$ on each row and column, and we want to reconver $S$. It’s not known whether it can be done in polynomial time. The usual approach to tackle the problem is based on some combinatorial objects called the switching components. We present some recent results abour their structures.
« Back to the Coordinated Attack Problem » par E. Godard (LIS)
« Analyse et reconstruction de modèles 3D » par A. Bac (LIS)
« Faster computation on simple topologies » par C. Maria (INRIA)
Orateur : Emmanuel Godard, LIS
Titre : Back to the Coordinated Attack Problem
Résumé : We consider the well known Coordinated Attack Problem, where two gener- als have to decide on a common attack, when their messengers can be captured by the enemy. Informally, this problem represents the difficulties to agree in the present of communication faults. We consider here only omission faults (loss of message), but contrary to previous studies, we do not to restrict the way mes- sages can be lost, i.e. we make no specific assumption, we use no specific failure metric. In the large subclass of message adversaries where the double simulta- neous omission can never happen, we characterize which ones are obstructions for the Coordinated Attack Problem. We give two proofs of this result. One is combinatorial and uses the classical bivalency technique for the necessary con- dition. The second is topological and uses simplicial complexes to prove the necessary condition. We also present two different Consensus algorithms that are combinatorial (resp. topological) in essence. Finally, we analyze the two proofs and illustrate the relationship between the combinatorial approach and the topological approach in the very general case of message adversaries. We show that the topological characterization gives a clearer explanation of why some message adversaries are obstructions or not. This result is a convincing illustration of the power of topological tools for distributed computability.
Joint work with Eloi Perdereau
Orateur : Alexandra Bac (MCF), LIS
Titre : Analyse et reconstruction de modèles 3D : approches géométriques et topologiques
Résumé : Avec la généralisation de l’outil informatique dans tous les domaines de la société civile, la modélisaton géométrique est devenue une plaque tournante incontournable. Pour expliquer son essor, commençons peut-être par une tentative de définition :
« La modélisation géométrique, à la croisée des Mathématiques et de l’Informatique Graphique, a pour but de construire et analyser des modèles virtuels d’objets réels ou virtuels. »
Différents facteurs ont contribué à élargir le statut de la modélisation géométrique pour le faire passer de discipline relativement académique à celui d’outil applicatif indispensable :
Orateur : Clement Maria, INRIA
Titre : Faster computation on simple topologies
Résumé : The complexity of solving topological problems on surfaces often depends on the topology of the input surface. For example, deciding whether a graph can be embedded on a surface is NP-hard in general, but becomes only linear time on the size of the graph if the genus of the surface is considered constant. In this talk, we focus on a powerful topological invariant of 3-manifolds satisfying a similar property. Specifically, we introduce a fixed parameter tractable algorithm for computing the Turaev-Viro invariant at the fourth root of unity, using the dimension of the first homology group of the manifold as parameter. This invariant is #P-hard to compute in general. This is joint work with Jonathan Spreer.
« Synthesizing robust controllers for Büchi conditions in timed systems » par D. Busatto-Gaston (LIS)
« Programmation logique au sens ASP » par B. Benhamou (LIS)
« Assume Admissible Synthesis » par J.F. Raskin (ULB)
Orateur : Damien Busatto-Gaston (PhD) , LIS
Titre : Synthesizing robust controllers for Büchi conditions in timed systems.
Résumé : We solve the robust controller synthesis problem in timed automata with Büchi acceptance conditions. The goal of the controller is to play according to an accepting lasso of the automaton, while resisting to timing perturbations chosen by a competing environment. The talk will introduce classical notions for studying timed automata (regions, zones, constraint graphs) and explain how these can be extended to compute strategies that are resilient to arbitrarily small perturbations. We will also introduce a way to compute the largest perturbation allowed by a given controller. Our techniques are illustrated by the regulation of a train network.
Orateur : Belaid Benhamou (MCF), LIS
Titre : Programmation logique au sens ASP (Answer Set Programming) : une nouvelle sémantique capturant et étendant celle des modèles stables.
Résumé : Plusieurs travaux ont été faits pour définir des sémantiques pour les programmes logiques normaux. La plupart de ces sémantiques sont en fait des sémantiques de points fixes. L’idée principale est le calcul de modèles canoniques du programme logique considéré, appelés modèles stables (Gelfond et al. 1988).
Dans cette exposé, nous décrivons une nouvelle sémantique pour les programmes logiques normaux. Cette dernière est basée sur une notion d’extensions de formules propositionnelles classiques. Un programme logique est alors codé par un ensemble de clauses de Horn propositionnelles. On prouve que chaque formule consistante (ou programme logique) admet au moins une extension et que, pour chaque modèle stable d’un programme logique, il existe une extension de son codage logique qui l’implique. Certaines extensions (extra-extensions) ne correspondent pas à des modèles stables du programme logique, mais sont intéressantes car elles représentent ici, une extension pour la sémantique des modèles stables. Nous donnons une condition discriminante simple qui permet de reconnaître les extensions « normales » et les distinguer des extra-extensions.
Basé sur cette sémantique, nous proposons une nouvelle méthode de recherche de modèles stables pour les programmes logiques. Elle a l’avantage d’utiliser un ensemble de clauses de Horn et travaille à espace constant. Elle évite ainsi, la lourdeur induite par la gestion des boucles, dont souffrent la plupart des solveurs ASP utilisant la complétion de Clark et qui ont des complexités spatiales exponentielles dans le pire des cas. De plus, l’énumération est effectuée sur un ensemble restreint de variables du programme logique. Ce qui réduit en général, la complexité temporelle de l’algorithme. En plus de la recherche de modèles stables, cette méthode pourrait générer une sorte d’extra-modèles stables exprimant ainsi l’extension portée à la sémantique des modèles stables.
Orateur : Raskin Jean-Francois, ULB
Titre : Assume Admissible Synthesis.
Résumé : In this talk, I will show how the notion of admissibility can be used to provide an elegant solution to the synthesis problem for reactive system where the environment is not completely adversarial or when the system is composed of several components. In particular, I will introduce a novel rule for synthesis of reactive systems, applicable to systems made of n components which have each their own objectives. Contrary to previous proposals in the literature, the rule « assume admissible » defines sets of solutions which are rectangular. This property leads to solutions which are robust and resilient, and allows one to synthesize strategies separately for each component.
« Décompositions et résolution de modèles graphiques » par C. Terrioux (LIS)
« Argument-based logics » par L. Amgoud (IRIT)
« Au coeur des démonstrateurs SAT » par G. Audemard (CRIL)
Orateur : Cyril Terrioux , LIS
Titre : Décompositions et résolution de modèles graphiques
Résumé : La notion de décomposition arborescente est, de nos jours, un sujet majeur pour l’étude théorique et la résolution pratique de problèmes NP-complets et au-delà. En intelligence artificielle, son utilisation est des plus prometteuses notamment dans le cadre des modèles graphiques (réseaux de contraintes, réseaux bayésiens, logique propositionnelle, …).
Dans cet exposé, nous illustrerons d’abord comment la décomposition arborescente peut être exploitée, d’un point de vue théorique, pour définir des classes polynomiales. Ensuite, nous nous intéresserons aux méthodes de calcul de décompositions arborescentes. Enfin, nous verrons quel peut-être l’apport de la décomposition arborescente pour la résolution pratique des instances.
Orateur : Leila Amgoud, IRIT
Titre : Argument-based logics
Résumé : Argumentation is a reasoning process based on the justification of claims by arguments. Due to its explanatory power, it has become a hot topic in Artificial Intelligence, and has been used for solving different problems including decision making under uncertainty, learning rules, modelling different types of dialogs, and more importantly reasoning about inconsistent information.
In this talk, I will focus on argument-based paraconsistent logics. Starting from a knowledge base encoded in a logical language, an argument-based logic defines arguments (supporting conclusions) and identifies conflicts between them. Then, it evaluates the strength of each arguments using what is called semantics in the argumentation literature. Finally, it infers conclusions that are supported by strong arguments. I will present two families of such logics: the family that uses extension semantics and the one that uses ranking ones for the evaluation of arguments. I discuss the outcomes of both families and compare them. I also compare the argumentation approach with other well-known paraconsistent logics.
Orateur : Gilles Audemard, CRIL
Titre : Au coeur des démonstrateurs SAT
Résumé : Aujourd’hui, les solveurs SAT se trouvent au coeur de nombreux domaines de recherche. Nous commencerons par une présentation des ingrédients essentiels des solveurs SAT. Ensuite, nous présenterons l’utilisation incrémentale des démonstrateurs SAT, c’est à dire l’appel multiple de solveurs sur des instances proches les unes des autres. Nous introduirons quelques exemples d’utilisation incrémentale de SAT. Enfin, nous ferons une petite analyse des compétitions SAT qui ont lieu tous les ans.
« Quantum control flow » par B. Valiron (LRI)
« Natural computing models of unusual complexity » par A.E. Porreca (LIS)
« Computability in closure spaces » par E. Jeandel (LORIA)
Orateur : Benoit Valiron (http://www.monoidal.net), CentralSupelec, LRI
Titre : Quantum control flow
Résumé : One perspective on quantum algorithms is that they are classical algorithms having access to a special kind of memory with exotic properties. This perspective suggests that, even in the case of quantum algorithms, the control flow notions of sequencing, conditionals, loops, and recursion are entirely classical. There is however, another notion of control flow, that is itself quantum. The notion of quantum conditional expression is reasonably well-understood: the execution of the two expressions becomes itself a superposition of executions. The quantum counterpart of loops and recursion is however not believed to be meaningful in its most general form. In this talk, using a detour through reversible computing we discuss how a reasonable notion of quantum loops and recursion is indeed possible.
Orateur : A.E. Porreca, LIS
Titre : Natural computing models of unusual complexity
Orateur : E. Jeandel, LORIA
Titre : Computability in closure spaces
« Hybrid tractable classes » par M. Cooper (IRIT)
« On Rationality of Nonnegative Matrix Factorization » par M. Shirmohammadi (LIS)
« Tout réseau hyperbolique a un coeur » par V. Chepoi (LIS)
Orateur : Martin Cooper, l’IRIT
Titre : Hybrid tractable classes
Résumé : The CSP (constraint satisfaction problem) is a generic problem over finite domains in which each constraint is a relation and a list of variables (its scope). Given the NP-completeness of the CSP, it is natural is to look for restrictions of the problem that allow polynomial-time solving. The two classical approaches consist in studying restrictions either on the language of relations or on the hypergraph defined by the constraint scopes. After 30 years of effort, dichotomies have been established for these two approaches. A third avenue consists in defining classes of CSP instances by forbidding patterns (generic sub-problems). This hybrid approach has led to the discovery of several new polynomial classes. I will present the state of the art in the characterization of forbidden patterns that define polynomial classes.
Orateur : Mahsa Shirmohammadi (LIS AMU, new MCF)
Titre : On Rationality of Nonnegative Matrix Factorization
Résumé : Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative n×m matrix M into a product of a nonnegative n×d matrix W and a nonnegative d×m matrix H. A longstanding open question, posed by Cohen and Rothblum in 1993, is whether a rational matrix M always has an NMF of minimal inner dimension d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix for which W and H require irrational entries.
In this talk, we further exhibit a connection between Cohen and Rothblum’s question with a question posed by Paz, in his seminal 1971 textbook. The latter question asks, given a probabilistic automaton (PA) with rational transition probabilities, does there always exist a minimal equivalent PA that also has rational transition probabilities? The PA and its minimal equivalent PA accept all finite words with equal probabilities. We use the established connection to answer Paz’s question negatively, thus falsifying a positive answer claimed in 1974.
(This talk is based on two papers in ICALP 2016 and SODA 2017.)
Orateur : Victor Chepoi (LIS AMU)
Titre : Tout réseau hyperbolique a un coeur (ou « hyperbolicité pour tous »)
Résumé : In the first part of the talk, we will introduce Gromov hyperbolicity and recall several characterizations of delta-hyperbolic geodesic metric spaces and graphs.
In the second part, we investigate the impact the negative curvature has on the traffic congestion in large-scale networks. We prove that every Gromov hyperbolic network G admits a core, thus answering in the positive a conjecture by Jonckheere, Lou, Bonahon, and Baryshnikov, Internet Mathematics, 7 (2011) which is based on the experimental observation by Narayan and Saniee, Physical Review E, 84 (2011) that real-world networks with small hyperbolicity have a core congestion. Namely, we prove that for every subset X of n vertices of a graph G with delta-thin geodesic triangles there exists a vertex m of G such that the ball B(m,4delta) of radius 4delta centered at m intercepts at least one half of the total flow between all pairs of vertices of X, where the flow between two vertices x,y of X is carried by geodesic (or quasi-geodesic) (x,y)-paths. We show that the point m can be constructed in the following way: take a median point m* of X (a point minimizing the sum of distances to the points of X) in the injective hull of G and then a closest to m* point in G. In the third part of the talk, (and if the time will permit), we will describe a simple factor 8 approximation algorithm for optimal hyperbolicity of an n-vertex graph in optimal O(n^2) time (assuming that the input is the distance matrix of the graph).
The talk is based on the papers
[1] V. Chepoi, F. Dragan, and Y. Vaxès, Core congestion is inherent in hyperbolic networks, SODA 2017, <http://arxiv.org/abs/1605.03059> .
[2] J. Chalopin, V. Chepoi, F. Dragan, G. Ducoffe, A. Mohammed, and Y. Vaxès, <https://arxiv.org/abs/1803.06324> Fast approximation and exact computation of negative curvature parameters of graphs, SoCG 2018, <https://arxiv.org/abs/1803.06324>.
« Homologie algorithmique pour les objets discrets » par A. Gonzales-Lorenzo (LIRIS)
« Topological and algorithmic tools for computability in distributed computing » par D. Imbs (LIS)
« Un contre-exemple à la conjecture de Thiagarajan sur les structures d’évènements régulières » par J. Chalopin (LIS)
Orateur : Aldo Gonzales-Lorenzo (post-doc LIRIS)
Titre : Homologie algorithmique pour les objets discrets
Résumé : La théorie de l’homologie formalise la notion de trou dans un espace. Pour un sous-ensemble de l’espace Euclidien, on définit une séquence de groupes d’homologie, dont leurs rangs sont interprétés comme le nombre de trous de chaque dimension. Ainsi, β0 (le rang du groupe d’homologie de dimension zéro) est le nombre de composantes connexes, β1 est le nombre de tunnels ou anses et β2 est le nombre de cavités. Ces groupes sont calculables quand l’espace est décrit d’une façon combinatoire, comme c’est le cas pour les complexes simpliciaux ou cubiques. À partir d’un objet discret (un ensemble de pixels, voxels ou leur analogue en dimension supérieure) nous pouvons construire un complexe cubique et donc calculer ses groupes d’homologie.
Dans cette présentation je parlerai de deux approches relatives au calcul de l’homologie sur des objets discrets. Primo, je présenterai le champ de vecteurs discret homologique, une structure combinatoire qui permet de calculer les groupes d’homologie. Secundo, je présenterai deux mesures (l’épaisseur et la largeur) associées aux trous d’un objet discret, ce qui permet d’obtenir une signature topologique et géométrique plus intéressante que les simples nombres de Betti.
Orateur : Damien Imbs (LIS AMU, new MCF)
Titre : Topological and algorithmic tools for computability in distributed computing
Résumé : One of the major breakthroughs in distributed computing was the discovery of its links with algebraic topology. This result earned its authors the Gödel prize in 2004. Topological tools are especially useful to prove impossibility results.
In this talk, I will present such topological tools and how to use them to prove the impossibility of distributed problems. In particular, I will show how to use Sperner’s Lemma to prove the impossibility of Set Agreement, a fundamental distributed problem, in a specific model. I will then present algorithmic techniques to extend this result to various distributed models of computation.
Orateur : Jeremie Chalopin (LIS AMU)
Titre : Un contre-exemple à la conjecture de Thiagarajan sur les structures d’évènements régulières
Résumé : On présente un contre-exemple à la conjecture de Thiagarajan (1996 et 2002) affirmant que les structures d’évènements régulières correspondent exactement à celles obtenues comme dépliages des réseaux de Petri 1-safe finis. Les structures d’évènements, les automates de trace sont des modèles fondamentaux pour la théorie de la concurrence. Il existe des interprétations élégantes de ces structures comme des objets combinatoires et géométriques, et on peut reformuler la conjecture dans ce cadre. Plus précisément, les domaines des structures d’évènements correspondent exactement aux graphes médians pointés et aux complexes cubiques CAT(0) pointés. Une condition nécessaire pour que la conjecture de Thiagarajan soit vérifiée est que les domaines des structures d’évènements régulières admettent un joli étiquetage régulier (regular nice labelling). Pour réfuter cette conjecture, on décrit le domaine d’une structure d’évènement régulière qui n’admet pas de tel étiquetage. Notre contre-exemple est basé sur une construction de Wise (1996 et 2007) d’un complexe de carrés de courbure non-positive dont le revêtement universel est un complexe de carrés CAT(0) contenant un plan muni d’un pavage apériodique.
« When type theory meets model-checking » par C. Grellois (LIS)
« Programs as formulas » par M. Cristia (U. N. Rosario)
« On The Complexity of Resource-Bounded Logics » par S. Demri (LSV)
Orateur : Charles Grellois (LIS)
Titre : When type theory meets model-checking
Résumé : Type theory and model-checking are two formal methods, aiming at ensuring the correctness of programs. In type theory, the idea is to annotate the instructions of the program with the properties they satisfy, so as to statically control how they will evolve during the computation, and to conclude that the program is correct — or not. In model-checking, one typically abstracts the program as a mathematical model, as a graph for instance, representing an approximation of its behavior. Then, an appropriate logical formula is devised over this program, and an algorithm checks automatically whether the abstract model satisfies the requirement. In the analysis of functional programs, higher-order constructions are possible: one can define functions that themselves take functions as inputs. Type theory is particularly useful to analyze such situations, as I will explain during the talk. I will first give a brief idea of what model-checking is, then explain what are the basics of type theory, and in a third time show how they where combined by Kobayashi in 2009 to perform model-checking of functional programs. If time allows, I will spend the last minutes giving an overview of the research I did in the last years building up on Kobayashi’s work and its extension by Kobayashi and Ong.
Orateur : Maximiliano Cristia (U. N. Rosario)
Titre : Programs as formulas (not as proofs)
Résumé : After the Curry-Howard correspondence and the type theories developed in the past decades, it emerged the idea of programs as proofs (of their properties). That is, if we have a proof P of a theorem T, we can make P a program whose type is T. This theory was a major breakthrough in programming language design and software verification. However, in this talk, I’ll show you an alternative and, in some sense, previous view: programs as formulas. In other words, let’s make the very formula to be a program; that is, we don’t need to make a proof to have a program. In particular I’m going to show {log} (setlog), which is a programming language but also an automated theorem prover. In {log} formulas are programs, and programs are formulas. We can use the same tool and the same language to specify programs, to simulate these specifications, to generate test cases and to prove properties of them. {log} works with formulas over the theory of finite sets, which allows for the specification of large classes of programs.
Orateur : Stephane Demri (LSV)
Titre : On The Complexity of Resource-Bounded Logics
Résumé : We characterise the complexity of model-checking problems for resource-bounded logics by taking advantage of recent results on decision problems for alternating VASS. For instance, we show that the model-checking problem for the logic RBATL is 2EXPTIME-complete and we establish that for RBATL* the problem remains decidable. A parameterised version of the logics is also discussed. This is a joint work with Natasha Alechina, Nils Bulling and Brian Logan.