TBA
On monday, at 2pm - UPEC CMC - Room P2-131
May 19, 2025
Containment for Guarded Monotone Strict NP
Guarded Monotone Strict NP (GMSNP) extends Monotone Monadic Strict NP (MMSNP) by guarded existentially quantified predicates of arbitrary arities. The talk will be about the meta-problem of containment for the former logic. While being undecidable for many classes of problems (e.g., Datalog, SNP, first-order) it remains to be decidable for GMSNP. The complexity of the problem is 2NEXPTIME-complete — the same as for MMSNP. In my talk, I will show some examples of GMSNP problems and discuss the methods arising from model and Ramsey theories that are used in order to characterise the containment.
May 12, 2025
TBA
TBA
May 5, 2025
TBA
TBA
April 28, 2025
Formal modeling and analysis of social-ecogical systems
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.
April 14, 2025
Analyse calculable sur l’espace des groupes marqués
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.
April 7, 2025
Extending Timed Automata with Clock Derivatives
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.
April 7, 2025
A framework for locally structured spaces
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.
March 31, 2025
CrewAI for State Representation Optimization in Model Checking: A LLM-Based Framework for State Space Analysis with UPPAAL
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.
March 24, 2025
An algebraic approach for union bound reasoning about probabilistic programs
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.