General information
I am a researcher in the Infrastructure Protection Security Research Team at the Cyber Physical Security Research Center of the National Institute of Advanced Industrial Science and Technology, in Tokyo.
I am also involved with the JapaneseFrench Laboratory for Informatics.
Previously, I was a Project Researcher (postdoc) and then a Project Assistant Professor in Prof. Ichiro Hasuo's ERATO Metamathematics for Systems Design Project at the National Institute of Informatics in Tokyo. I am still involved in the project as a Visiting Researcher.
Before that, I was a PhD student at LSV, ENS ParisSaclay, under the supervision of Jean GoubaultLarrecq and Eric Goubault.
Email: jeremy[dot]dubut[at]aist[dot]go[dot]jp
Upcoming events and news
 I received the best paper award for my paper AczelMendler Bisimulations in a Regular Category at CALCO (see [0]).
 Our paper Formal Verification of Intersection Safety for Automated Driving (with James Haydon, Martin Bondu, Clovis Eberhart, and Ichiro Hasuo) has been accepted for presentation at ITSC, in Bilbao (Spain) in September (see [0]).
 Please, consider attending JSSST2023. Some of the talks are related to [0] and [0].
 I am in childcare leave from September 2023 to March 2024. I am still answering emails, but expect some delays.
 I just released the newest version of this page, mostly untested. If there is anything wrong, please let me know :)
Research interests
 categorical aspects of computer science
 (true) concurrency
 (directed) algebraic topology
 formal methods for CPS
 proof assistants
Publications
Click on to unfold more information.Journals

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 discretetime 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 infinitedimensional 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 finitedimensional linear system, and use it for moment approximation by iteratively propagating the moments along the finitedimensional 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 
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.
GoalAware RSS for Complex Scenarios Via Program Logic.Transactions on Intelligent Vehicles, IEEE, 2022.Abstract:We introduce a goalaware extension of responsibilitysensitive safety (RSS), a recent methodology for rulebased 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 dFHLbased workflow for deriving goalaware RSS rules; we discuss its software support, too. We conducted experimental evaluation using RSS rules in a safety architecture. Its results show that goalaware RSS is indeed effective in realising both collision avoidance and goal achievement.
Key words:automated driving, safety, rulebased safety, responsibilitysensitive safety (RSS), program logic, FloydHoare logic, differential dynamics, simplex architecture
Links: 
J. Dubut and
A. Yamada.
Fixed Point Theorems for NonTransitive Relations.Logical Methods in Computer Science, 18(1), 30:130:24, Episciences, 2022.Extended version of [0].Abstract:In this paper, we develop an Isabelle/HOL library of ordertheoretic fixedpoint theorems. We keep our formalization as general as possible: we reprove several wellknown 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 quasifixed 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 KnasterTarski, BourbakiWitt, Kleene, Markowsky, Pataraia, Mashburn, BhattaGeorge, and StoutiMaaden.
Key words:order theory, lattice theory, fixedpoints, Isabelle/HOL
Links: 
D. Sprunger,
S. Katsumata,
J. Dubut, and
I. Hasuo.
Fibrational Bisimulations and Quantitative Reasoning: Extended Version.Journal of Logic and Computation, 31(6), 15261559, Oxford University Press, 2021.Extended verion of [0].Abstract:Bisimulation and bisimilarity are fundamental notions in comparing statebased 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 predicateforming 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: 
T. Wißmann,
S. Milius,
S. Katsumata, and
J. Dubut.
A Coalgebraic View on Reachability.Commentationes Mathematicae Universitatis Carolinae, 60(4), 605638, Charles University, 2019.Abstract:Coalgebras for an endofunctor provide a categorytheoretic framework for modeling a wide range of statebased 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 breadthfirst 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, breadthfirst search, reachability
Links: 
J. Dubut,
É. Goubault, and
J. GoubaultLarrecq.
Directed homology theories and EilenbergSteenrod axioms.Applied Categorical Structures, 25(5), 775807, 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 EilenbergSteenrod 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

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 responsibilitysensitive 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, rulebased safety, responsibilitysensitive safety (RSS), program logic, FloydHoare logic, differential dynamics, simplex architecture 
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 blackbox ADV controllers, and for graceful degradation from one ODD to another. Building on our previous work on the formalization of responsibilitysensitive safety (RSS), we introduce a novel program logic that accommodates assume guarantee reasoning and fallbacklike 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, rulebased safety, responsibilitysensitive safety (RSS), program logic, FloydHoare logic, differential dynamics, simplex architecture 
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 structurepreserving 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 structurepreserving 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 valuebased 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 
J. Dubut.
AczelMendler Bisimulations in a Regular Category.In CALCO'23, LIPICS, LeibnizZentrum für Informatik, 2023.Best paper award.Abstract:AczelMendler 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 powerobject monad, and extend the formalism to simulations. Finally, we describe several examples in Stone spaces, toposes for namepassing, and modules over a ring.
Key words:regular categories, toposes, bisimulations, coalgebra
Links: 
A. Yamada and
J. Dubut.
Formalizing Results on Directed Sets in Isabelle/HOL.In ITP'23, LIPICS, LeibnizZentrum 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 penandpaper 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: 
J. Dubut and
T. Wißmann.
Weighted and Branching Bisimulations from Generalized Open Maps.In FoSSaCS'23, LNCS, 13992, 308327, Springer, 2023.Abstract:In the open map approach to bisimilarity, the paths and their runs in a given statebased system are the firstclass citizens, and bisimilarity becomes a derived notion. While open maps were successfully used to model bisimilarity in nondeterministic 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: 
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 spatiotemporal logic with fixed points and firstorder 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:spatiotemporal logic, network of agents, monitoring, netwrok topology, resilient consensus
Links: 
S. Pruekprasert,
C. Eberhart, and
J. Dubut.
Fast Synthesis for Symbolic Selftriggered Control under Rightrecursive LTL Specifications.In CDC'21, IEEE, 2021.Abstract:We extend previous work on symbolic selftriggered control for nondeterministic continuoustime nonlinear 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 rightrecursive 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 meanpayoff 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:selftriggered control, symbolic model, meanpayoff parity games, LTL specifications
Links: 
S. Pruekprasert,
C. Eberhart, and
J. Dubut.
Symbolic Selftriggered Control of Continuoustime Nondeterministic Systems without Stability Assumptions for 2LTL Specifications.In ICARCV'20, IEEE, 2020.Best paper award finalist.Abstract:We propose a symbolic selftriggered controller synthesis procedure for nondeterministic continuoustime 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 2LTL. 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:selftriggered control, symbolic model, meanpayoff parity games, LTL specifications
Links: 
S. Pruekprasert,
T. Takisaka,
C. Eberhart,
A. Cetinkaya, and
J. Dubut.
Moment Propagation of DiscreteTime Stochastic Polynomial Systems using Truncated Carleman Linearization.In IFAC'20, IFACPapersOnLine, 53(2), 1446214469, Elsevier, 2020.Abstract:We propose a method to compute an approximation of the moments of a discretetime stochastic polynomial system. We use the Carleman linearization technique to transform this finitedimensional polynomial system into an infinitedimensional linear one. After taking expectation and truncating the induced deterministic dynamics, we obtain a finitedimensional 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: 
J. Dubut.
Bisimilarity of diagrams.In RAMiCS'20, LNCS, 12062, 6581, 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 bisimulationlike 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: 
J. Kolčák,
J. Dubut,
I. Hasuo,
S. Katsumata,
D. Sprunger, and
A. Yamada.
Relational Differential Dynamic Logic.In TACAS'20, LNCS, 12078, 191208, 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, cyberphysical system, formal verification, theorem proving, dynamic logic
Links: 
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 nonmalicious 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: 
A. Yamada and
J. Dubut.
Complete NonOrders and Fixed Points.In ITP'19, LIPICS, 141, 30:130:16, LeibnizZentrum für Informatik, 2019.Abstract:In this paper, we develop an Isabelle/HOL library of ordertheoretic concepts, such as various completeness conditions and fixedpoint theorems. We keep our formalization as general as possible: we reprove several wellknown results about complete orders, often without any property of ordering, thus complete nonorders. In particular, we generalize the Knaster–Tarski theorem so that we ensure the existence of a quasifixed point of monotone maps over complete nonorders, and show that the set of quasifixed 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 fixedpoint theorem for omegacomplete nonorders, again using attractivity to prove that Kleene's fixed points are least quasifixed points.
Key words:order theory, lattice theory, fixedpoints, Isabelle/HOL
Links: 
J. Dubut.
Trees in partial Higher Dimensional Automata.In FoSSaCS'19, LNCS, 11425, 224241, 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: 
T. Wißmann,
J. Dubut,
S. Katsumata, and
I. Hasuo.
Path Category For Free: Open Morphisms From Coalgebras With NonDeterministic Branching.In FoSSaCS'19, LNCS, 11425, 523540, 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 Gcoalgebra 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 pathcategory for pointed Gcoalgebras and lax homomorphisms, such that the open morphisms turn out to be precisely the Gcoalgebra homomorphisms. The above construction provides pathcategories and trace semantics for free for different flavours of transition systems: (1) nondeterministic 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: 
D. Sprunger,
S. Katsumata,
J. Dubut, and
I. Hasuo.
Fibrational Bisimulations and Quantitative Reasoning.In CMCS'18, LNCS, 11202, 190213, Springer, 2018.Abstract:Bisimulation and bisimilarity are fundamental notions in comparing statebased 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: 
J. Dubut,
É. Goubault, and
J. GoubaultLarrecq.
The Directed Homotopy Hypothesis.In CSL'16, LIPICS, 62, 9:19:16, LeibnizZentrum 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: 
J. Dubut,
É. Goubault, and
J. GoubaultLarrecq.
Bisimulations and unfolding in Paccessible categorical models.In CONCUR'16, LIPICS, 59, 25:125:14, LeibnizZentrum 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: 
J. Dubut,
É. Goubault, and
J. GoubaultLarrecq.
Natural Homology.In ICALP'15, LNCS, 9135, 171183, Springer, 2015.Abstract:We propose a notion of homology for directed algebraic topology, based on socalled 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

S. Pruekprasert,
J. Dubut,
X. Zhang,
C. Huang, and
M. Kishida.
A Game Theoretic Approach to Decision Making for Multiple Vehicles at Roundabout.arXiv, 2019.Abstract:In this paper, we study the decision making of multiple autonomous vehicles at a roundabout. The behaviours of the vehicles depend on their aggressiveness, which indicates how much they value speed over safety. We propose a distributed decisionmaking process that balances safety and speed of the vehicles. In the proposed process, each vehicle estimates other vehicles' aggressiveness and formulates the interactions among the vehicles as a finite sequential game. Based on the Nash equilibrium of this game, the vehicle predicts other vehicles' behaviours and makes decisions. We perform numerical simulations to illustrate the effectiveness of the proposed process, both for safety (absence of collisions), and speed (time spent within the roundabout).
Key words:decision making, autonomous vehicles, games, acceleration, safety, roads
Links: 
J. Dubut,
S. Katsumata,
I. Hasuo, and
D. Sprunger.
Quantitative bisimulations using coreflections and open morphisms.arXiv, 2018.Abstract:We investigate a canonical way of defining bisimilarity of systems when their semantics is given by a coreflection, typically in a category of transition systems. We use the fact, from Joyal et al., that coreflections preserve open morphisms situations in the sense that a coreflection induces a path subcategory in the category of systems in such a way that open bisimilarity with respect to the induced path category coincides with usual bisimilarity of their semantics. We prove that this method is particularly wellsuited for systems with quantitative information: we canonically recover the path category of probabilistic systems from Cheng et al., and of timed systems from Nielsen et al., and, finally, we propose a new canonical path category for hybrid systems.
Key words:open maps bisimilarity, coreflections, hybrid systems
Links:
Theses

Directed homotopy and homology theories for geometric models of true concurrency.PhD, Laboratoire Spécification et vérification, ENS ParisSaclay, Université ParisSaclay, 2017.Under the supervision of É. Goubault and J. GoubaultLarrecq.Abstract:Studying a system that evolves with time through its geometry is the main purpose of directed algebraic topology. This topic emerged in computer science, more particularly in true concurrency, where Pratt introduced the higher dimensional automata (HDA) in 1991 (actually, the idea of geometry of concurrency can be tracked down Dijkstra in 1965). Those automata are geometric by nature: every set of n processes executing independent actions can be modeled by a ncube, and such an automaton then gives rise to a topological space, obtained by glueing such cubes together. This space naturally has a specific direction of time coming from the execution flow. It then seems natural to use tools from algebraic topology to study those spaces: paths model executions, homotopies of paths, that is continuous deformations of paths, model equivalence of executions modulo scheduling of independent actions, and so on, but all those notions must preserve the direction. This brings many complications and the theory must be done again. In this thesis, we develop homotopy and homology theories for those spaces with a direction. First, my directed homotopy theory is based on deformation retracts, that is continuous deformation of a big space on a smaller space, following directed paths that are inessential, meaning that they do not change the homotopy type of spaces of executions. This theory is related to categories of components and higher categories. Secondly, my directed homology theory follows the idea that we must look at the spaces of executions and those evolves with time. This evolution of time is handled by defining such homology as a diagram of spaces of executions and comparing such diagrams using a notion of bisimulation. This homology theory has many nice properties: it is computable on simple spaces, it is an invariant of our homotopy theory, it is invariant under simple action refinements and it has a theory of exactness.
Key words:directed algebraic topology, true concurrency, homology, homotopy
Links: 
Homologie dirigée.M2 internship, École Polytechnique, Palaiseau, 2014.Under the supervision of É. Goubault and J. GoubaultLarrecq.Abstract:See my PhD thesis, which is a better and more complete version of this report.
Key words:directed algebraic topology, directed homology, EilenbergSteenrod axioms
Links: 
Application de la topologie algébrique en informatique théorique.M1 internship, École Polytechnique Fédérale de Lausanne, 2012.Under the supervision of K. HessBellwald.Abstract:The purpose of this report is to describe some constructions by Raussen to represent the homotopy type of trace spaces of cubical complexes in directed algebraic topology. We then investigate methods to compute the homotopy and homology groups of those spaces. The first method uses homotopy colimits. The second is by describing the homotopy type as a generalized moment angle complex of a graphs generated by the holes of the complex and their relationship with respect to the order. We then formulated a conjecture that this is effectively the case, implying that the number of generators of homology is the number of chains of holes. In the case of domension 3, this would also imply that the fundamental group is isomorphic to the rightangled Artin associated with the grpah of holes, and that actually the trace space is a EilenbergMacLane space for this group. Finally, we proved this statement in some easy cases such as dimension 2, chains of holes, or incomparable holes.
Key words:directed algebraic topology, trace spaces, homology and homotopy groups, Salvetti complexes
Links: 
Décidabilité de la déduction et de l'équivalence statique pour le chiffrement homomorphique.L3 internship, Laboratoire Lorrain de Recherche en Informatique et ses Applications, Nancy, 2011.Under the supervision of V. Cortier.Abstract:To be added
Key words:decidable equational theory, static equivalence, homomorphic encryption
Links: 
Le modèle de CuckerSmale: Émergence et formation de structures et de motifs dans les groupes (troupeaux, bancs, colonies, nuées).L3 internship, Centre de Mathématiques et Leurs Applications, 2011.With C. Eberhart, under the supervision of F. Pascal.Abstract:To be added
Key words:flocking models, differential equations, simulations, cinetic model, MonteCarlo method
Links:
Some presentations
 slides for the 54th TRS meeting
 slides for a seminar at Igarashi lab, Kyoto University
 slides for DHS 2019
 poster (made by Juraj) for the ERATO MMSD Symposium on Automated Driving Safety
 slides for the PPS seminar, Paris 7
 slides and poster for the Young Mathematicians' Challenge in Tokyo
 slides (in French) for a flash talk at the Journée Francophone de la Recherche in Tokyo
 slides for DHS 2018
 slides and poster for NII's Winter Festa
 slides for the Shonan meeting on Enhanced coinduction
 slides for Young Researcher CONCUR17
 slides and YouTube video for the conference of the program Applied and Computational Algebraic Topology at Hausdorff Research Institute for Mathematics
 slides for the Prix Doctorants ED STIC 2016 ceremony at the journée de rentrée at ENSTA ParisTech
 slides for ACCAPT16
 poster for the Journées nationales 2016 of GdR IM
 slides for HCR
 poster for GETCO15
Teachings
SOKENDAI (2019)
I did a guest lecture for the Formal Methods for CyberPhysical Systems course for SOKENDAI students on Deductive verification of hybrid systemsslides, KeYmaera model, Keymaera proof, home assignment
ENS ParisSaclay (20142017)
This section contains archives for the exercise sessions I monitored at the CS department at the École Normale Supérieure ParisSaclay (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.