TBA

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.

Most models of quantum computing do not allow to represent efficiently “quantum control flow” : the possibility to have a quantum superposition between two different executions.
For instance, the quantum program “if x then P1 else P2” can be understood as a superposition of both P1 and P2 being executed at the same time.
In this talk, we explore how the additive structure of linear logic can be used to model quantum control flow. To this end, we introduce the “Many-Worlds Calculus”, a graphical language based on the Multiplicative Additive Proof Nets of Linear Logic for quantum computing. The graphical language comes equipped with a denotational semantics based on linear maps, and an equational theory. We prove the language to be universal, and the equational theory to be complete with respect to this semantics.

Les Macro Transducteurs d’Arbre (ou MTT) sont un modèle de fonctions entre langages d’arbre qui généralise les transducteurs d’arbre top-down classiques. Ils furent introduits en 1980 pour étudier les grammaires à attributs, un modèle utilisé en traitement du langage naturel et en compilation pour assigner une sémantique aux mots d’un langage context-free. Nous présenterons ici, après avoir introduits les modèles en question, une classe spéciale de MTTs dite “depth-proper”, toute aussi expressive que les MTT classique, et dans laquelle il est possible de décider si la fonction réalisée a une croissance linéaire en hauteur (LHI) ou non.

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.