16 citations · 40 across the 20 of their papers we have counts for
22 papers
Monitoring Diameters of Causal Communication Graph with Spatio-Temporal Logic
Lydia Bakiri, Jérémy Dubut, Sergio Mover
Verification of multi-agent systems requires the ability to check meticulous topological properties when it comes to agents that can move through space in continuous time. This dem…
Homological Algebra in Abelian Framed Bicategories: Exact Sequences and Embedding Theorems
Augustin Albert, Jérémy Dubut, Eric Goubault
We introduce abelian framed bicategories, which are particular framed bicategories that are locally abelian, and show that they are suitable for developing homology and cohomology…
Variants of Higher-Dimensional Automata
Hugo Bazille, Jérémy Dubut, Uli Fahrenberg +1
The theory of higher-dimensional automata (HDAs) has seen rapid progress in recent years, and first applications, notably to Petri net analysis, are starting to show. It has, howev…
A Categorical Framework for Program Semantics and Semantic Abstraction
Shin-ya Katsumata, Xavier Rival, Jérémy Dubut
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…
Formal Verification of Safety Architectures for Automated Driving
Clovis Eberhart, Jérémy Dubut, James Haydon +1
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 gr…
Formal Verification of Intersection Safety for Automated Driving
James Haydon, Martin Bondu, Clovis Eberhart +2
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 contr…
Aczel-Mendler Bisimulations in a Regular Category
Jeremy Dubut
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 f…
Weighted and Branching Bisimilarities from Generalized Open Maps
Jérémy Dubut, Thorsten Wißmann
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…
Goal-Aware RSS for Complex Scenarios via Program Logic
Ichiro Hasuo, Clovis Eberhart, James Haydon +12
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 r…
Moment Propagation of Polynomial Systems Through Carleman Linearization for Probabilistic Safety Analysis
Sasinee Pruekprasert, Jérémy Dubut, Toru Takisaka +2
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 ta…
Fast Synthesis for Symbolic Self-triggered Control under Right-recursive LTL Specifications
Sasinee Pruekprasert, Clovis Eberhart, Jérémy Dubut
We extend previous work on symbolic self-triggered control for non-deterministic continuous-time nonlinear systems without stability assumptions to a larger class of specifications…
Symbolic Self-triggered Control of Continuous-time Non-deterministic Systems without Stability Assumptions for 2-LTL Specifications
Sasinee Pruekprasert, Clovis Eberhart, Jérémy Dubut
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…
Fixed Points Theorems for Non-Transitive Relations
Jérémy Dubut, Akihisa Yamada
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 a…
Moment Propagation of Discrete-Time Stochastic Polynomial Systems using Truncated Carleman Linearization
Sasinee Pruekprasert, Toru Takisaka, Clovis Eberhart +2
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…
Decision Making for Autonomous Vehicles at Unsignalized Intersection in Presence of Malicious Vehicles
Sasinee Pruekprasert, Xiaoyi Zhang, Jérémy Dubut +2
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 t…
A Game-Theoretic Approach to Decision Making for Multiple Vehicles at Roundabout
Sasinee Pruekprasert, Jérémy Dubut, Xiaoyi Zhang +2
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…
Relational Differential Dynamic Logic
Juraj Kolčák, Ichiro Hasuo, Jérémy Dubut +3
In the field of quality assurance of hybrid systems (that combine continuous physical dynamics and discrete digital control), Platzer's differential dynamic logic (dL) is widely re…
A Coalgebraic View on Reachability
Thorsten Wißmann, Stefan Milius, Shin-ya Katsumata +1
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…
Path category for free - Open morphisms from coalgebras with non-deterministic branching
Thorsten Wißmann, Jérémy Dubut, Shin-ya Katsumata +1
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…
Quantitative bisimulations using coreflections and open morphisms
Jérémy Dubut, Ichiro Hasuo, Shin-ya Katsumata +1
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,…
Trees in Partial Higher Dimensional Automata
Jérémy Dubut
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 a…
Bisimilarity of diagrams
Jérémy Dubut
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 o…