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
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
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
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
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
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
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
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
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
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/HO
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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 decision-making 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
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 well-suited 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
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 n-cube, 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
Abstract:
See my PhD thesis, which is a better and more complete version of this report.
Key words:
directed algebraic topology, directed homology, Eilenberg-Steenrod axioms
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 right-angled Artin associated with the grpah of holes, and that actually
the trace space is a Eilenberg-MacLane 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
Abstract:
to be written
Key words:
Decidable equational theory, static equivalence, homomorphic encryption
Abstract:
Key words:
flocking models, differential equations, simulations, cinetic model, Monte-Carlo method