TBA

TBA

TBA

We present the EDEN framework that provides tools for the formal modelling and analysis of social-ecological systems and their dynamics. In particular, EDEN features modelling languages that allow defining systems as discrete variables and guarded actions to update them. An implementation called ecco allows analysing the dynamics of such modelled systems in an interactive and incremental way, leveraging classical techniques from the field of model-checking. EDEN has been used for years for both theoretical and practical studies.

L’approche classique de l’étude de la calculabilité en théorie des groupes repose sur l’usage des présentations finies, qui encodent de manière compacte la table de multiplication d’un groupe engendré par un nombre fini d’éléments.
Un théorème de Groves et Wilton de 2009 montre que des phénomènes très intéressants apparaissent si l’on s’intéresse à des descriptions plus complexes. Pour donner un cadre formel à cette nouvelle approche, on se tournera vers l’analyse calculable.

The demand for large-scale, complex distributed applications is growing with the expansion of distributed computing and networking. Distributed Real-Time Applications are essential for controlling and monitoring Distributed Real-Time Systems (DRTS) in domains like aerospace, robotics, and nuclear plants. DRTS often operate on heterogeneous networks with multiple interconnected components, each equipped with independent, unsynchronized clocks. While Timed Automata (TA) and Distributed Timed Automata (DTA) are standard formalisms for modeling DRTS, they have limitations: TA assumes synchronized clocks, and DTA may fail to fully capture indirect interactions or dependencies between clocks. This paper introduces idTA, a novel, more expressive variant of TA and DTA that controls clock drift. We also present DLν, an extension of Lν logic incorporating our idTA semantics, with semantics defined over Multi-Timed Labeled Transition Systems (MLTS). We prove that model checking for DLν is EXPTIME-complete and introduce MIMETIC, a model checking tool tailored for verifying DRTS.

For the analysis of concurrent programs, higher-dimensional automata (HDA) are models that help to limit the combinatorial explosion that can be observed with interleaving models. Such an automaton has a fundamentally geometric interpretation: it can be seen as a construction plan indicating how to glue together elementary topological spaces such as segments, squares, cubes, etc. In order to retrieve the semantics of the program in the topological space previously constructed, the latter must have a notion of local direction. To axiomatize this idea of local direction, several non-equivalent approaches have been proposed in the literature, such as d-spaces, streams, locally ordered spaces and so on.

In this talk, we present a unified framework, inspired by topological spaces, which can contain and compare these different approaches, and, more generally, in which it is possible to define all kinds of locally structured spaces. We show that many topological notions generalize to this framework, and that streams have a natural place in it.

CrewAI is a framework for orchestrating role-playing AI agents, collaborating to solve complex tasks. Here we introduce an innovative approach to formal verification that addresses the state explosion problem through a multi-agent AI framework, currently in early development stages. Our system deploys four specialized agents (State Representation Specialist, Abstraction Engineer, UPPAAL Interface Specialist, and Evaluation Specialist) that collaborate to analyze, optimize, and verify state spaces in formal models. This work represents a first step toward making formal verification more practical for complex systems through AI-assisted state space optimization.

Kleene Algebra with Tests (KAT) provides a framework for algebraic equational reasoning about imperative programs. The recent variant Guarded KAT (GKAT) allows to reason on non-probabilistic properties of probabilistic programs. Here we introduce an extension of this framework called approximate GKAT (aGKAT), which equips GKAT with a partially ordered monoid (real numbers) enabling to express satisfaction of (deterministic) properties except with a probability up to a certain bound. This allows to represent in equational reasoning ‘à la KAT’ proofs of probabilistic programs based on the union bound, a technique from basic probability theory. We show how a propositional variant of approximate Hoare Logic (aHL), a program logic for union bound, can be soundly encoded in our system aGKAT. We then illustrate the use of aGKAT with an example of accuracy analysis from the field of differential privacy.

For concurrent programs, Higher Dimensional Automata (HDA) are a very expressive model of non-interleaving concurrency. In this talk, I explain my recent works regarding these models and its timed version.

Temporal logics are a powerful tool to specify properties of computational systems.
HDA recognize languages of partially ordered multisets, or pomsets. Recent work has shown that Monadic Second Order (MSO) logic is as expressive as HDA for pomset languages.
In recent work, we investigate the class of pomset languages that are definable in First Order (FO) logic. In the case of words, Kamp’s theorem states that FO is as expressive as Linear Temporal Logic (LTL). Our aim is to prove a variant of Kamp’s theorem for pomset languages. Thus, we define a temporal logic called Sparse Pomset Temporal Logic (SPTL), and show that it is equivalent to FO, when there is no auto-concurrency.
In previous work, we worked on lifting decidability and undecidability results from Timed Automata to a timed version of HDA, Higher Dimensional Timed Automata.