General information

I am a Professeur Assistant Monge at École Polytechnique. I am part of the DIX, of the Cosynus team, of the LIX lab, and of the chaire Architecture des Systèmes Complexes of IP Paris.

Before that,
Apr. 22—Aug. 24 Researcher at Infrastructure Protection Security Research Team, Cyber Physical Security Research Center, National Institute of Advanced Industrial Science and Technology, Tokyo, Japan.
Nov. 17—Mar. 22 Project researcher→Project assistant professor at ERATO HASUO Metamathematics for Systems Design Project, National Institute of Informatics, Tokyo, Japan.
Nov. 17—Mar. 24 Member of Japanese-French Laboratory for Informatics.
Sep. 14—Sep. 17 PhD student and teaching assistant at ENS Paris-Saclay, under the supervision of Jean Goubault-Larrecq and Eric Goubault, Cachan, France.

Email: jeremy[dot]dubut[at]polytechnique[dot]edu

Office: Room 2152, LIX - UMR 7161
Ecole Polytechnique
1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing
91128 Palaiseau

Upcoming events and news

Research interests

Publications

Click on to unfold more information.

Journals

  1. S. Pruekprasert, J. Dubut, T. Takisaka, C. Eberhart, and A. Cetinkaya.
    Moment Propragation Through Carleman Linearization with Application to Probabilistic Safety Analysis.
    Automatica, Elsevier, To appear.
    Extended version of [0].
    Abstract:
    We develop a method to approximate the moments of a discrete-time stochastic polynomial system. Our method is built upon Carleman linearization with truncation. Specifically, we take a stochastic polynomial system with finitely many states and transform it into an infinite-dimensional system with linear deterministic dynamics, which describe the exact evolution of the moments of the original polynomial system. We then truncate this deterministic system to obtain a finite-dimensional linear system, and use it for moment approximation by iteratively propagating the moments along the finite-dimensional linear dynamics across time. We provide efficient online computation methods for this propagation scheme with several error bounds for the approximation. Our result also shows that precise values of certain moments can be obtained when the truncated system is sufficiently large. Furthermore, we investigate techniques to reduce the offline computation load using reduced Kronecker power. Based on the obtained approximate moments and their errors, we also provide probability bounds for the state to be outside of given hyperellipsoidal regions. Those bounds allow us to conduct probabilistic safety analysis online through convex optimization. We demonstrate our results on a logistic map with stochastic dynamics and a vehicle dynamics subject to stochastic disturbance.

    Key words:
    stochastic systems, nonlinear systems, probabilistic safety analysis, moment computation, Carleman linearization
  2. I. Hasuo, C. Eberhart, J. Haydon, J. Dubut, R. Bohrer, T. Kobayashi, S. Pruekprasert, X. Zhang, E. Pallas, A. Yamada, K. Suenaga, F. Ishikawa, K. Kamijo, Y. Shinya, and T. Suetomi.
    Goal-Aware RSS for Complex Scenarios Via Program Logic.
    Transactions on Intelligent Vehicles, IEEE, 2022.
    Abstract:
    We introduce a goal-aware extension of responsibility-sensitive safety (RSS), a recent methodology for rule-based safety guarantee for automated driving systems (ADS). Making RSS rules guarantee goal achievement - in addition to collision avoidance as in the original RSS — requires complex planning over long sequences of manoeuvres. To deal with the complexity, we introduce a compositional reasoning framework based on program logic, in which one can systematically develop RSS rules for smaller subscenarios and combine them to obtain RSS rules for bigger scenarios. As the basis of the framework, we introduce a program logic dFHL that accommodates continuous dynamics and safety conditions. Our framework presents a dFHL-based workflow for deriving goal-aware RSS rules; we discuss its software support, too. We conducted experimental evaluation using RSS rules in a safety architecture. Its results show that goal-aware RSS is indeed effective in realising both collision avoidance and goal achievement.

    Key words:
    automated driving, safety, rule-based safety, responsibility-sensitive safety (RSS), program logic, Floyd-Hoare logic, differential dynamics, simplex architecture

    Links:
  3. J. Dubut and A. Yamada.
    Fixed Point Theorems for Non-Transitive Relations.
    Logical Methods in Computer Science, 18(1), 30:1-30:24, Episciences, 2022.
    Extended version of [0].
    Abstract:
    In this paper, we develop an Isabelle/HOL library of order-theoretic fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often with only antisymmetry or attractivity, a mild condition implied by either antisymmetry or transitivity. In particular, we generalize various theorems ensuring the existence of a quasi-fixed point of monotone maps over complete relations, and show that the set of (quasi-)fixed points is itself complete. This result generalizes and strengthens theorems of Knaster-Tarski, Bourbaki-Witt, Kleene, Markowsky, Pataraia, Mashburn, Bhatta-George, and Stouti-Maaden.

    Key words:
    order theory, lattice theory, fixed-points, Isabelle/HOL

    Links:
  4. D. Sprunger, S. Katsumata, J. Dubut, and I. Hasuo.
    Fibrational Bisimulations and Quantitative Reasoning: Extended Version.
    Journal of Logic and Computation, 31(6), 1526-1559, Oxford University Press, 2021.
    Extended verion of [0].
    Abstract:
    Bisimulation and bisimilarity are fundamental notions in comparing state-based systems. Their extensions to a variety of systems have been actively pursued in recent years, a notable direction being quantitative extensions. In this paper we enhance a categorical framework for such extended (bi)simulation notions. We use coalgebras as system models and fibrations for organizing predicates—following the seminal work by Hermida and Jacobs. Endofunctor liftings are crucial predicate-forming ingredients; the first contribution of this work is to extend several extant lifting techniques from particular fibrations to CLat∧-fibrations over Set. The second contribution of this work is to introduce endolifting morphisms as a mechanism for comparing predicates between fibrations. We apply these techniques by deriving some known properties of the Hausdorff pseudometric and approximate bisimulation in control theory.

    Key words:
    fibration, approximate bisimulation, behavioural metric, functor lifting

    Links:
  5. T. Wißmann, S. Milius, S. Katsumata, and J. Dubut.
    A Coalgebraic View on Reachability.
    Commentationes Mathematicae Universitatis Carolinae, 60(4), 605-638, Charles University, 2019.
    Abstract:
    Coalgebras for an endofunctor provide a category-theoretic framework for modeling a wide range of state-based systems of various types. We provide an iterative construction of the reachable part of a given pointed coalgebra that is inspired by and resembles the standard breadth-first search procedure to compute the reachable part of a graph. We also study coalgebras in Kleisli categories: for a functor extending a functor on the base category, we show that the reachable part of a given pointed coalgebra can be computed in that base category.

    Key words:
    coalgebra, breadth-first search, reachability

    Links:
  6. J. Dubut, É. Goubault, and J. Goubault-Larrecq.
    Directed homology theories and Eilenberg-Steenrod axioms.
    Applied Categorical Structures, 25(5), 775-807, Springer, 2017.
    Extended version of [0].
    Abstract:
    In this paper, we define and study a homology theory, that we call “natural homology”, which associates a natural system of abelian groups to every space in a large class of directed spaces and precubical sets. We show that this homology theory enjoys many important properties, as an invariant for directed homotopy. Among its properties, we show that subdivided precubical sets have the same homology type as the original ones; similarly, the natural homology of a precubical set is of the same type as the natural homology of its geometric realization. By same type we mean equivalent up to some form of bisimulation, that we define using the notion of open map. Last but not least, natural homology, for the class of spaces we consider, exhibits very important properties such as Hurewicz theorems, and most of Eilenberg-Steenrod axioms, in particular the dimension, homotopy, additivity and exactness axioms. This last axiom is studied in a general framework of (generalized) exact sequences.

    Key words:
    algebraic topology, directed topology, homology theory, exact sequences

    Links:

Conferences

  1. A. Yamada, J. Dubut, and T. Tsukada.
    Hedge automata revisited: Transforming texts to and from XML.
    In ATVA'24, Springer, 2024.
    Abstract:
    We develop automata-theoretic concepts for hedges, a mathematical model for XML documents. First, we define context-free grammars on hedges, and connect our formulation with existing definitions of regular hedge languages and hedge automata. We also extend regular automata, push-down automata, and push-down transducers to hedges, and verify that the well-known correspondences with language classes in the string case carry over to the hedge setting. Based on the theory, we introduce a tool TXtruct, which serves as a grammar validator and transformer for XML and text files.

    Key words:
    hedge automata, XML, transducers, grammars
  2. J. Haydon, M. Bondu, C. Eberhart, J. Dubut, and I. Hasuo.
    Formal Verification of Intersection Safety for Automated Driving.
    In ITSC'23, IEEE, 2023.
    Abstract:
    We build on our recent work on formalization of responsibility-sensitive safety (RSS) and present the first formal framework that enables mathematical proofs of the safety of control strategies in intersection scenarios. Intersection scenarios are challenging due to the complex interaction between vehicles; to cope with it, we extend the program logic dFHL in the previous work and introduce a novel formalism of hybrid control flow graphs on which our algorithm can automatically discover an RSS condition that ensures safety. An RSS condition thus discovered is experimentally evaluated; we observe that it is safe (as our safety proof says) and is not overly conservative.

    Key words:
    automated driving, safety, rule-based safety, responsibility-sensitive safety (RSS), program logic, Floyd-Hoare logic, differential dynamics, simplex architecture
  3. C. Eberhart, J. Dubut, J. Haydon, and I. Hasuo.
    Formal Verification of Safety Architectures for Automated Driving.
    In IV'23, IEEE, 2023.
    Abstract:
    Safety architectures play a crucial role in the safety assurance of automated driving vehicles (ADVs). They can be used as safety envelopes of black-box ADV controllers, and for graceful degradation from one ODD to another. Building on our previous work on the formalization of responsibility-sensitive safety (RSS), we introduce a novel program logic that accommodates assume- guarantee reasoning and fallback-like constructs. This allows us to formally define and prove the safety of existing and novel safety architectures. We apply the logic to a pull over scenario and experimentally evaluate the resulting safety architecture.

    Key words:
    automated driving, safety, rule-based safety, responsibility-sensitive safety (RSS), program logic, Floyd-Hoare logic, differential dynamics, simplex architecture
  4. S. Katsumata, X. Rival, and J. Dubut.
    A Categorical Framework for Program Semantics and Semantic Abstraction.
    In MFPS'23, ENTICS, Episciences, 2023.
    Abstract:
    Categorical semantics of type theories are often characterized as structure-preserving functors. This is because in category theory both the syntax and the domain of interpretation are uniformly treated as structured categories, so that we can express interpretations as structure-preserving functors between them. This mathematical characterization of semantics makes it convenient to manipulate and to reason about relationships between interpretations. Motivated by this success of functorial semantics, we address the question of finding a functorial analogue in abstract interpretation, a general framework for comparing semantics, so that we can bring similar benefits of functorial semantics to semantic abstractions used in abstract interpretation. Major differences concern the notion of interpretation that is being considered. Indeed, conventional semantics are value-based whereas abstract interpretation typically deals with more complex properties. In this paper, we propose a functorial approach to abstract interpretation and study associated fundamental concepts therein. In our approach, interpretations are expressed as oplax functors in the category of posets, and abstraction relations between interpretations are expressed as lax natural transformations representing concretizations. We present examples of these formal concepts from monadic semantics of programming languages and discuss soundness.

    Key words:
    semantics, abstract interpretation, oplax functors, monads
  5. J. Dubut.
    Aczel-Mendler Bisimulations in a Regular Category.
    In CALCO'23, LIPICS, Leibniz-Zentrum für Informatik, 2023.
    Best paper award.
    Abstract:
    Aczel-Mendler bisimulations are a coalgebraic extension of a variety of computational relations between systems. It is usual to assume that the underlying category satisfies some form of axiom of choice, so that the theory enjoys desirable properties, such as closure under composition. In this paper, we accommodate the definition in a general regular category -- which does not necessarily satisfy any form of axiom of choice. We show that this general definition 1) is closed under composition without using the axiom of choice, 2) coincide with other types of coalgebraic formulations under milder conditions, 3) coincide with the usual definition when the category has the regular axiom of choice. We then develop the particular case of toposes, where the formulation becomes nicer thanks to the power-object monad, and extend the formalism to simulations. Finally, we describe several examples in Stone spaces, toposes for name-passing, and modules over a ring.

    Key words:
    regular categories, toposes, bisimulations, coalgebra

    Links:
  6. A. Yamada and J. Dubut.
    Formalizing Results on Directed Sets in Isabelle/HOL.
    In ITP'23, LIPICS, Leibniz-Zentrum für Informatik, 2023.
    Abstract:
    Directed sets are of fundamental interest in domain theory and topology. In this paper, we formalize some results on directed sets in Isabelle/HOL, most notably: under the axiom of choice, a poset has a supremum for every directed set if and only if it does so for every chain; and a function between such posets preserves suprema of directed sets if and only if it preserves suprema of chains. The known pen-and-paper proofs of these results crucially use uncountable transfinite sequences, which are not directly implementable in Isabelle/HOL. We show how to emulate such proofs by utilizing Isabelle/HOL's ordinal and cardinal library. Thanks to the formalization, we relax some conditions for the above results.

    Key words:
    directed sets, completeness, scott continuous functions, ordinals, Isabelle/HOL

    Links:
  7. J. Dubut and T. Wißmann.
    Weighted and Branching Bisimulations from Generalized Open Maps.
    In FoSSaCS'23, LNCS, 13992, 308-327, Springer, 2023.
    Abstract:
    In the open map approach to bisimilarity, the paths and their runs in a given state-based system are the first-class citizens, and bisimilarity becomes a derived notion. While open maps were successfully used to model bisimilarity in non-deterministic systems, the approach fails to describe quantitative system equivalences such as probabilistic bisimilarity. In the present work, we see that this is indeed impossible and we thus generalize the notion of open maps to also accommodate weighted and probabilistic bisimilarity. Also, extending the notions of strong path and path bisimulations into this new framework, we show that branching bisimilarity can be captured by this extended theory and that it can be viewed as the history preserving restriction of weak bisimilarity.

    Key words:
    open maps, weighted bisimilarity, probabilistic bisimilarity, branching bisimilarity, weak bisimilarity

    Links:
  8. C. Eberhart, J. Haydon, J. Dubut, A. Cetinkaya, and S. Pruekprasert.
    Logic for Timed Agent Network Topologies.
    In CDC'22, IEEE, 2022.
    Abstract:
    We define μTGL, a spatio-temporal logic with fixed points and first-order agent quantification whose expressive power allows the definition of topological properties of networks of communicating agents. The existence of temporal operators and fixed points requires particular care when defining its semantics. We also give a streaming monitoring algorithm for μTGL formulas. Finally, we demonstrate the logic's usefulness on an example, where we monitor a complex property that ensures resilient consensus.

    Key words:
    spatio-temporal logic, network of agents, monitoring, netwrok topology, resilient consensus

    Links:
  9. S. Pruekprasert, C. Eberhart, and J. Dubut.
    Fast Synthesis for Symbolic Self-triggered Control under Right-recursive LTL Specifications.
    In CDC'21, IEEE, 2021.
    Abstract:
    We extend previous work on symbolic self-triggered control for non-deterministic continuous-time non-linear systems without stability assumptions to a larger class of specifications. Our goal is to synthesise a controller for two objectives: the first one is modelled as a right-recursive LTL formula, and the second one is to ensure that the average communication rate between the controller and the system stays below a given threshold. We translate the control problem to solving a mean-payoff parity game played on a discrete graph. Apart from extending the class of specifications, we propose a heuristic method to shorten the computation time. Finally, we illustrate our results on the example of a navigating nonholonomic robot with several specifications.

    Key words:
    self-triggered control, symbolic model, mean-payoff parity games, LTL specifications

    Links:
  10. S. Pruekprasert, C. Eberhart, and J. Dubut.
    Symbolic Self-triggered Control of Continuous-time Non-deterministic Systems without Stability Assumptions for 2-LTL Specifications.
    In ICARCV'20, IEEE, 2020.
    Best paper award finalist.
    Abstract:
    We propose a symbolic self-triggered controller synthesis procedure for non-deterministic continuous-time nonlinear systems without stability assumptions. The goal is to compute a controller that satisfies two objectives. The first objective is represented as a specification in a fragment of LTL, which we call 2-LTL. The second one is an energy objective, in the sense that control inputs are issued only when necessary, which saves energy. To this end, we first quantise the state and input spaces, and then translate the controller synthesis problem to the computation of a winning strategy in a mean- payoff parity game. We illustrate the feasibility of our method on the example of a navigating nonholonomic robot.

    Key words:
    self-triggered control, symbolic model, mean-payoff parity games, LTL specifications

    Links:
  11. S. Pruekprasert, T. Takisaka, C. Eberhart, A. Cetinkaya, and J. Dubut.
    Moment Propagation of Discrete-Time Stochastic Polynomial Systems using Truncated Carleman Linearization.
    In IFAC'20, IFAC-PapersOnLine, 53(2), 14462-14469, Elsevier, 2020.
    Abstract:
    We propose a method to compute an approximation of the moments of a discrete-time stochastic polynomial system. We use the Carleman linearization technique to transform this finite-dimensional polynomial system into an infinite-dimensional linear one. After taking expectation and truncating the induced deterministic dynamics, we obtain a finite-dimensional linear deterministic system, which we then use to iteratively compute approximations of the moments of the original polynomial system at different time steps. We provide upper bounds on the approximation error for each moment and show that, for large enough truncation limits, the proposed method precisely computes moments for sufficiently small degrees and numbers of time steps. We use our proposed method for safety analysis to compute bounds on the probability of the system state being outside a given safety region. Finally, we illustrate our results on two concrete examples, a stochastic logistic map and a vehicle dynamics under stochastic disturbance.

    Key words:
    stochastic systems, nonlinear systems, probabilistic safety analysis, moment computation, Carleman linearization

    Links:
  12. J. Dubut.
    Bisimilarity of diagrams.
    In RAMiCS'20, LNCS, 12062, 65-81, Springer, 2020.
    Abstract:
    In this paper, we investigate diagrams, namely functors from any small category to a fixed category, and more particularly, their bisimilarity. Initially defined using the theory of open maps of Joyal et al., we prove two characterisations of this bisimilarity: it is equivalent to the existence of a bisimulation-like relation and has a logical characterisation à la Hennessy and Milner. We then prove that we capture both path bisimilarity and strong path bisimilarity of any small open maps situation. We then look at the particular case of finitary diagrams with values in real or rational vector spaces. We prove that checking bisimilarity and satisfiability of a positive formula by a diagram are both decidable by reducing to a problem of existence of invertible matrices with linear conditions, which in turn reduces to the existential theory of the reals.

    Key words:
    open maps, diagrams, path logic, existential theories

    Links:
  13. J. Kolčák, J. Dubut, I. Hasuo, S. Katsumata, D. Sprunger, and A. Yamada.
    Relational Differential Dynamic Logic.
    In TACAS'20, LNCS, 12078, 191-208, Springer, 2020.
    Abstract:
    In the field of quality assurance of hybrid systems, Platzer's differential dynamic logic (dL) is widely recognized as a deductive verification method with solid mathematical foundations and sophisticated tool support. Motivated by case studies provided by our industry partner, we study a relational extension of dL, aiming to formally prove statements such as “an earlier engagement of the emergency brake yields a smaller collision speed.” A main technical challenge is to combine two dynamics, so that the powerful inference rules of dL (such as the differential invariant rules) can be applied to such relational reasoning, yet in such a way that we relate two different time points. Our contributions are a semantical theory of time stretching, and the resulting synchronization rule that expresses time stretching by the syntactic operation of Lie derivative. We implemented this rule as an extension of KeYmaera X, by which we successfully verified relational properties of a few models taken from the automotive domain.

    Key words:
    hybrid system, cyber-physical system, formal verification, theorem proving, dynamic logic

    Links:
  14. S. Pruekprasert, X. Zhang, J. Dubut, C. Huang, and M. Kishida.
    Decision Making for Autonomous Vehicle at Unsignalized Intersection in Presence of Malicious Vehicles.
    In ITSC'19, IEEE, 2019.
    Abstract:
    In this paper, we investigate the decision making of autonomous vehicles in an unsignalized intersection in presence of malicious vehicles, which are vehicles that do not respect the law by not using the proper rules of the right of way. Each vehicle computes its control input as a Nash equilibrium of a game determined by the priority order based on its own belief: each of non-malicious vehicle bases its order on the law, while a malicious one considers itself as having priority. To illustrate the effectiveness of our method, we provide numerical simulations, with different scenarios given by different cases of malicious vehicles.

    Key words:
    decision making, autonomous vehicles, games, acceleration, safety, roads

    Links:
  15. A. Yamada and J. Dubut.
    Complete Non-Orders and Fixed Points.
    In ITP'19, LIPICS, 141, 30:1-30:16, Leibniz-Zentrum für Informatik, 2019.
    Abstract:
    In this paper, we develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any property of ordering, thus complete non-orders. In particular, we generalize the Knaster–Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition—attractivity—which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene's fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene's fixed points are least quasi-fixed points.

    Key words:
    order theory, lattice theory, fixed-points, Isabelle/HOL

    Links:
  16. J. Dubut.
    Trees in partial Higher Dimensional Automata.
    In FoSSaCS'19, LNCS, 11425, 224-241, Springer, 2019.
    EATCS best paper award.
    Abstract:
    In this paper, we give a new definition of partial Higher Dimension Automata using lax functors. This definition is simpler and more natural from a categorical point of view, but also matches more clearly the intuition that pHDA are Higher Dimensional Automata with some missing faces. We then focus on trees. Originally, for example in transition systems, trees are defined as those systems that have a unique path property. To understand what kind of unique property is needed in pHDA, we start by looking at trees as colimits of paths. This definition tells us that trees are exactly the pHDA with the unique path property modulo a notion of homotopy, and without any shortcuts. This property allows us to prove two interesting characterisations of trees: trees are exactly those pHDA that are an unfolding of another pHDA; and trees are exactly the cofibrant objects, much as in the language of Quillen's model structure. In particular, this last characterisation gives the premisses of a new understanding of concurrency theory using homotopy theory.

    Key words:
    Higher Dimensional Automata, trees, homotopy theories

    Links:
  17. T. Wißmann, J. Dubut, S. Katsumata, and I. Hasuo.
    Path Category For Free: Open Morphisms From Coalgebras With Non-Deterministic Branching.
    In FoSSaCS'19, LNCS, 11425, 523-540, Springer, 2019.
    Abstract:
    There are different categorical approaches to variations of transition systems and their bisimulations. One is coalgebra for a functor G, where a bisimulation is defined as a span of G-coalgebra homomorphism. Another one is in terms of path categories and open morphisms, where a bisimulation is defined as a span of open morphisms. This similarity is no coincidence: given a functor G, fulfilling certain conditions, we derive a path-category for pointed G-coalgebras and lax homomorphisms, such that the open morphisms turn out to be precisely the G-coalgebra homomorphisms. The above construction provides path-categories and trace semantics for free for different flavours of transition systems: (1) non-deterministic tree automata (2) regular nondeterministic nominal automata (RNNA), an expressive automata notion living in nominal sets (3) multisorted transition systems. This last instance relates to Lasota's construction, which is in the converse direction.

    Key words:
    coalgebra, open maps, categories, nominal sets

    Links:
  18. D. Sprunger, S. Katsumata, J. Dubut, and I. Hasuo.
    Fibrational Bisimulations and Quantitative Reasoning.
    In CMCS'18, LNCS, 11202, 190-213, Springer, 2018.
    Abstract:
    Bisimulation and bisimilarity are fundamental notions in comparing state-based systems. Their extensions to a variety of systems have been actively pursued in recent years, a notable direction being quantitative extensions. In this paper we present an abstract categorical framework for such extended (bi)simulation notions. We use coalgebras as system models and fibrations for organizing predicates — following the seminal work by Hermida and Jacobs — but our focus is on the structural aspect of fibrational frameworks. Specifically we use morphisms of fi- brations as well as canonical liftings of functors via Kan extensions. We apply this categorical framework by deriving some known properties of the Hausdorff pseudometric and approximate bisimulation in control theory.

    Key words:
    fibration, approximate bisimulation, behavioural metric, functor lifting

    Links:
  19. J. Dubut, É. Goubault, and J. Goubault-Larrecq.
    The Directed Homotopy Hypothesis.
    In CSL'16, LIPICS, 62, 9:1-9:16, Leibniz-Zentrum für Informatik, 2016.
    Abstract:
    The homotopy hypothesis was originally stated by Grothendieck: topological spaces should be “equivalent” to (weak) ∞-groupoids, which give algebraic representatives of homotopy types. Much later, several authors developed geometrizations of computational models, e.g. for rewriting, distributed systems, (homotopy) type theory etc. But an essential feature in the work set up in concurrency theory, is that time should be considered irreversible, giving rise to the field of directed algebraic topology. Following the path proposed by Porter, we state here a directed homotopy hypothesis: Grandis' directed topological spaces should be “equivalent” to a weak form of topologically enriched categories, still very close to (∞,1)-categories. We develop, as in ordinary algebraic topology, a directed homotopy equivalence and a weak equivalence, and show invariance of a form of directed homology.

    Key words:
    directed algebraic topology, partially enriched categories, homotopy hypothesis, geometric models for concurrency, higher category theory

    Links:
  20. J. Dubut, É. Goubault, and J. Goubault-Larrecq.
    Bisimulations and unfolding in P-accessible categorical models.
    In CONCUR'16, LIPICS, 59, 25:1-25:14, Leibniz-Zentrum für Informatik, 2016.
    Abstract:
    We propose a categorical framework for bisimulations and unfoldings that unifies the classical approach from Joyal and al. via open maps and unfoldings. This is based on a notion of categories accessible with respect to a subcategory of path shapes, i.e., for which one can define a nice notion of trees as glueings of paths. We show that transition systems and presheaf models are instances of our framework. We also prove that in our framework, several notions of bisimulation coincide, in particular an “operational one” akin to the standard definition in transition systems. Also, our notion of accessibility is preserved by coreflections. This also leads us to a notion of unfolding that behaves well in the accessible case: it is a right adjoint and is a universal covering, i.e., it is initial among the morphisms that have the unique lifting property with respect to path shapes. As an application, we prove that the universal covering of a groupoid, a standard construction in algebraic topology, is an unfolding, when the category of path shapes is well chosen.

    Key words:
    categorical models, bisimulation, coreflections, unfolding, universal covering

    Links:
  21. J. Dubut, É. Goubault, and J. Goubault-Larrecq.
    Natural Homology.
    In ICALP'15, LNCS, 9135, 171-183, Springer, 2015.
    Abstract:
    We propose a notion of homology for directed algebraic topology, based on so-called natural systems of abelian groups, and which we call natural homology. As we show, natural homology has many desirable properties: it is invariant under isomorphisms of directed spaces, it is invariant under refinement (subdivision), and it is computable on cubical complexes.

    Key words:
    directed algebraic topology, homology, path space, geometric semantics, persistent homology, natural system

    Links:

Preprints

Theses

Some presentations

Teachings

SOKENDAI (2019)

I did a guest lecture for the Formal Methods for Cyber-Physical Systems course for SOKENDAI students on Deductive verification of hybrid systems
slides, KeYmaera model, Keymaera proof, home assignment

ENS Paris-Saclay (2014-2017)

This section contains archives for the exercise sessions I monitored at the CS department at the École Normale Supérieure Paris-Saclay (ex ENS Cachan). Most of them are in English, some in French. Some have a correction. There might be duplicates. Those exercises are usally taken from books, lecture notes, or papers, but any typo or mistake is my own.

Rewriting systems

Those sessions were for students in first year of master, and were made in collaboration with Hubert Comon and Frédéric Blanqui.
archive of exercises, archive of rewriting systems for kbcv.

Tree automata

Those sessions were for students in first year of master, and were made in collaboration with Hubert Comon and Sylvain Schmitz.
archive of exercises.

Logic

Those sessions were undergraduates, and were made in collaboration with Lucca Hirschi, Hubert Comon, Gilles Dowek, and Étienne Lozes.
archive of exercises.