Dialectica is a proof transformation acting of intuitionnistic logic, allowing
the realization of several semi-classical axioms such as Markov’s principle. By
taking the viewpoint of differential lambda-calculus and recent developments in
differentiable programming, we will show how Dialectica computes higher-order
backward differentiation. We will illustrate this through the lens of
categories, types and lambda-terms.
Dynamical systems are frequently used for modeling in the sciences. Building a detailed model often requires taking into account a large number of factors and, as a result, a model may become quite large. High-dimensional models with dozens or hundreds of state variables are not only challenging computationally but it is also hard to use them to derive mechanistic insights. Exact model reduction is a way to address this issue by finding a self-consistent lower dimensional projection of the corresponding dynamical system. I will describe recent algorithms for computing such reductions and demonstrate them on the models from literature.
The tableaux method is an automated proof search technics initially dealing with first-order logics. Many extensions have been proposed to accommodate different logics and additional theories. Toward the hope to extend this method with guaranteed simulation to prove properties on hybrid systems dynamics described by ODEs, we start with a more modest targe. We present the integration of tableaux to standard arithmetic equations. We show how an oracle can be used to deal with formula involving membership to constant intervals.
I will discuss joint work with Paul-André Melliès in which we analyze context-free grammars as certain kinds of functors of operads, and parsing as a lifting problem . One advantage of this perspective is that it naturally generalizes to enable one to define context-free languages of arrows in any category. Another advantage is that it allows one to study context-free grammars in a common setting with finite state automata, the latter seen as certain kinds of functors of categories. Relying on this (as well as on a surprising adjunction!) we give a categorical reconstruction of (a generalization of) the Chomsky-Schützenberger Representation Theorem, whose classical statement says that any context-free language may be represented as the homomorphic image of the intersection of a Dyck language of balanced parentheses with a regular language.
 Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem. MFPS 2022.
In the last few years, learning-based techniques have shown a great success to control complex cyber-physical systems (CPS), where learning-based tools are used either to provide mathematical models of a system, based on which one can synthesize a controller, or to learn directly the controller. However, the use of learning-based techniques in the context of safety critical CPS is particularly problematic, since learning-based components are typically viewed as black box-type systems, lacking formal guarantees. In this talk, we first recall how symbolic control techniques can be used in the context of the control of CPS. In the second part of the talk, we focus on how to provide guarantees when learning is used at the model’s level, namely we show how to learn a symbolic model from data, while providing formal guarantees. This symbolic model will be then used to construct the controller for complex specifications, such as linear temporal logics, based on existing tools in the formal methods community. In the last part of the talk, we focus on the use of learning at the controller’s level. We first use tools from viability theory to develop a general framework for the computation of interval controlled invariants for nonlinear systems. We then show how this framework makes it possible to provide safety guarantees when using neural networks to the control of dynamical systems.
Les diagrammes états-transitions algébriques (Algebraic State-Transition Diagrams (ASTD)) permettent de combiner des machines à états hiérarchiques avec des opérateurs inspirés des algèbres de processus (séquence, choix, garde, fermeture de Kleene, synchronisation, flow, et versions quantifiés de ces opérateurs). Un état d’une machine peut être un ASTD quelconque, ce qui donne une approche entièrement compositionnelle pour la spécifications de systèmes complexes. Des actions pouvant modifier des attributs, d’un type quelconque, déclarés localement dans les ASTD permettent de modéliser les données complexes de manière modulaire.
Nous présenterons une extension temporisée des ASTD, qui permet de spécifier des contraintes temporelles sur le comportement des ASTD. Les nouveaux opérateurs temporels sont: Delay, Persistent Delay, Timeout, Persistent Timeout et Timed Interrupt. Ils sont définis avec deux nouveaux opérateurs ASTD (Persistent Guard et Interruption). Ils peuvent être arbitrairement combinés avec les opérateurs existants. L’extension est basée sur une horloge globale qui fait partie de l’état et qui représente l’horloge système. Un évènement particulièr appelé « step » (inspiré de Stateflow) permet de spécifier des transitions dans les machines à états qui sont déclenchées par l’écoulement du temps. L’évènement step est soumis par l’environnement à un ASTD, typiquement à intervalles réguliers suffisamment petits pour respecter la granularité des contraintes de temps visées.
TASTD est supporté par un éditeur graphique eASTD et un compilateur cASTD qui permet de générer un programme C++ implémentant le comportement spécifié dans un TASTD. Le mode simulation permet d’exécuter le programme généré en contrôlant l’écoulement du temps.
Les preuves avec point-fixes (circulaires et non-bienfondées) permettent d’étudier des logiques exprimant des propriétés co·inductives. Le calcul des séquents présente des difficultés pour exprimer des propriétés indispensables pour la productivité. On présente donc des structures de preuve plus générales.
Joint avec Alexis Saurin et Abhishek De
In this talk, we consider the online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS), a method known to be scalable to large state spaces. We will present their theoretical guarantees. Formal analysis of MCTS is notably challenging, and we will discuss recent results in that area. Moreover, we augment the MCTS algorithm with a notion of symbolic advice, and show that its theoretical guarantees are maintained. Symbolic advice are used to bias the selection and simulation strategies of MCTS. We illustrate our techniques using a scheduling problem and the popular game Pac-Man.
Cooperative rational synthesis is the problem of computing a Nash equilibrium that satisfies the objective of a designated player, the “controller”. In this paper, we tackle this problem in the presence of several resources, where each action may increase or decrease some of the resources. We investigate the problem of synthesizing the controller strategy such that there exists an individually rational behavior of all the agents that satisfies the controller’s objective and does not deplete any of the resources.
We consider two types of agents: careless and careful. Careless agents only care for their temporal objective, while careful agents also pay attention not to deplete the system’s resource. We show that the problem is undecidable with at least two resources, and decidable for either a single resource or in the presence of a fixed upper bound on all the resources, and study the complexity for the decidable cases.
Controlling the Access of Data in Database management systems is a classical problem and it has been solved through different mechanisms. One of the most common implemented in most Databases management systems is the mechanism of views, i.e defining the accessible data of a user as the result of a query. This mechanism is also used in principle in other systems such as in social networks.
Unfortunately, this approach has some defaults. Even though it does not leak any secret information, the user seeing the data can infer some of these secret data by using different knowledge such as the logical definition of the query used to define the accessible data and different property of the database.
In this talk, I will present a formalism allowing to check when a set of views do not leak any information even through this kind of attacks.