Jérémy Dubut-Kross (デュブ黒須・ジェレミー)

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 Japanese-French 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 Paris-Saclay, under the supervision of Jean Goubault-Larrecq and Eric Goubault.

Email: jeremy[dot]dubut[at]aist[dot]go[dot]jp

dblp, research map, Google scholar, orcid

Upcoming events and news

Research interests

Publications

Journals

  1. 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. 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

  3. 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

  4. 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

  5. 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

  6. 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

Conferences

  1. 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

  2. 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

  3. 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

  4. 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

  5. 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

  6. 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

  7. 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

  8. 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

  9. 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

  10. 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

  11. 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

  12. 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

  13. Abstract:
    The homotopy hypothesis was originally stated by Grothendieck [13]: 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

  14. 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

  15. 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

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.