Events

Séminaire LoCaL

Systems that interact synchronously with an unpredictable environment are usually captured by zero-sum concurrent games. In such games, randomised strategies are in general more powerful than deterministic ones. Such systems, however, do not capture faithfully decentralised systems that cannot resort to a common private source of randomness. In this talk, I will introduce dicey games, a model for games played by teams, where the structure of randomness sources accessible to each player is explicitly specified.

Abstract: Event-B provides a rigorous method for ensuring functional safety of cyber-physical systems. However, it lacks native support for temporal aspects. Therefore, we propose a novel methodology using Parametric Timed Automata (PTA) as a formalism to systematically generate Event-B models with integrated temporal constraints. This generated model captures the temporal aspects and a partial functional specification, which is then improved with the remaining functional requirements. This approach significantly reduces manual effort in developing formally verified cyber-physical systems while ensuring both functional correctness and temporal safety properties through automated constraint synthesis and formal proof obligations.

Historiquement, l'approche franco-italo-japonais de la logique linéaire accorde beaucoup d'importance à la notion de réseaux de preuve. Celle-ci est, à son tour, basée sur un ensemble d'objets de nature calculatoire (des espèces de programmes non-typés) que l'on peut appeler des "structure de preuve non-typées". Dans l'exposé, je considérerai par parti pris les processus du pi-calcul comme des structures de preuve non-typées et non-déterministes, et je montrerai comment arriver aux réseaux de preuve d'une version de la logique linéaire avec cocontraction (mais sans coaffaiblissement ou codéreliction). S'il y a le temps, je parlerai de comment libéraliser cela pour obtenir un système de types pour le pi-calcul garnatissant l'absence de deadlock tout en permettant des processus "cycliques", habituellement exclus des systèmes de type à base de logique linéaire. Ceci est un travail en collaboration avec Juan Jaramillo et Jorge Perez (Université de Groeningen).

Interval graphs arise as intersection graphs of intervals on the real line and form a natural meeting point between discrete geometry and graph theory. Their rich structure yields efficient algorithms and applications in scheduling and resource allocation. Representing graphs as intersection graphs of axis-aligned boxes in R^d extends this idea to higher dimensions; the minimum dimension required is the boxicity of the graph, introduced by Roberts in 1969. Boxicity models competition for shared resources in ecology and operations research. It also matters algorithmically: graphs of bounded boxicity inherit some of the tractability of interval graphs (for example, Maximum Clique remains polynomial-time solvable). Exploiting this, however, typically requires a box representation, and finding one is NP-hard in general. Only a few graph classes are known for which boxicity can be computed in polynomial time. To extend this list and to develop new techniques for the problem, we follow the approach of Cozzens and Roberts (1983) and study the boxicity of a graph's complement, which we call its co-boxicity. This change of perspective trades d-dimensional boxes for one-dimensional objects: the co-boxicity of a graph is the minimum number of co-interval subgraphs needed to cover its edges. We show that co-boxicity can be computed block by block from a small amount of local information. As corollaries, we obtain a fixed-parameter tractable algorithm parameterized by the size of the largest block, and polynomial-time algorithms for block graphs and cactus graphs. This talk presents joint work with Will Evans and Tao Gaede.

Réunion de plannification