Details of the Researcher

PHOTO

Eberhart Clovis
Section
Research Institute of Electrical Communication
Job title
Assistant Professor
e-Rad No.
80867987

Papers 41

  1. AP-Observation Automata for Abstraction-Based Verification of Continuous-Time Systems

    Sasinee Pruekprasert, Clovis Eberhart

    2026

    DOI： 10.1007/978-3-032-11176-0_20 　

  2. Compositional Solution of Mean Payoff Games by String Diagrams.

    Kazuki Watanabe 0003, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo

    Principles of Verification (3)　423-445　2025

    DOI： 10.1007/978-3-031-75778-5_20 　

  3. Moment propagation of polynomial systems through Carleman linearization for probabilistic safety analysis

    Sasinee Pruekprasert, Jeremy Dubut, Toru Takisaka, Clovis Eberhart, Ahmet Cetinkaya

    Automatica　160　111441-111441　2024/02

    Publisher: Elsevier BV

    DOI： 10.1016/j.automatica.2023.111441 　

    ISSN： 0005-1098

  4. A Compositional Framework for Petri Nets.

    Serge Lechenne, Clovis Eberhart, Ichiro Hasuo

    Coalgebraic Methods in Computer Science - 17th IFIP WG 1.3 International Workshop(CMCS)　174-193　2024

    Publisher: Springer

    DOI： 10.1007/978-3-031-66438-0_9 　

  5. Goal-Aware RSS for Complex Scenarios via Program Logic.

    Ichiro Hasuo, Clovis Eberhart, James Haydon, Jérémy Dubut, Rose Bohrer, Tsutomu Kobayashi, Sasinee Pruekprasert, Xiao-Yi Zhang 0005, Erik André Pallas, Akihisa Yamada 0002, Kohei Suenaga, Fuyuki Ishikawa, Kenji Kamijo, Yoshiyuki Shinya, Takamasa Suetomi

    IEEE Transactions on Intelligent Vehicles　8　(4)　3040-3072　2023/04

    DOI： 10.1109/TIV.2022.3169762 　

  6. Formal Verification of Safety Architectures for Automated Driving.

    Clovis Eberhart, Jérémy Dubut, James Haydon, Ichiro Hasuo

    CoRR　abs/2308.10365　2023

    DOI： 10.48550/arXiv.2308.10365 　

  7. Formal Verification of Intersection Safety for Automated Driving.

    James Haydon, Martin Bondu, Clovis Eberhart, Jérémy Dubut, Ichiro Hasuo

    CoRR　abs/2308.06785　2023

    DOI： 10.48550/arXiv.2308.06785 　

  8. Compositional Probabilistic Model Checking with String Diagrams of MDPs.

    Kazuki Watanabe 0003, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo

    CoRR　abs/2307.08765　2023

    DOI： 10.48550/arXiv.2307.08765 　

  9. Compositional Solution of Mean Payoff Games by String Diagrams.

    Kazuki Watanabe 0003, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo

    CoRR　abs/2307.08034　2023

    DOI： 10.48550/arXiv.2307.08034 　

  10. Formal Verification of Safety Architectures for Automated Driving.

    Clovis Eberhart, Jérémy Dubut, James Haydon, Ichiro Hasuo

    IV　1-8　2023

    DOI： 10.1109/IV55152.2023.10186763 　

  11. Compositional Probabilistic Model Checking with String Diagrams of MDPs.

    Kazuki Watanabe 0003, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo

    CAV (3)　40-61　2023

    DOI： 10.1007/978-3-031-37709-9_3 　

  12. Goal-Aware RSS for Complex Scenarios via Program Logic.

    Ichiro Hasuo, Clovis Eberhart, James Haydon, Jérémy Dubut, Rose Bohrer, Tsutomu Kobayashi, Sasinee Pruekprasert, Xiao-Yi Zhang 0005, Erik André Pallas, Akihisa Yamada 0002, Kohei Suenaga, Fuyuki Ishikawa, Kenji Kamijo, Yoshiyuki Shinya, Takamasa Suetomi

    CoRR　abs/2207.02387　2022

    DOI： 10.48550/arXiv.2207.02387 　

  13. Moment Propagation Through Carleman Linearization with Application to Probabilistic Safety Analysis.

    Sasinee Pruekprasert, Jérémy Dubut, Toru Takisaka, Clovis Eberhart, Ahmet Cetinkaya

    CoRR　abs/2201.08648　2022

  14. Logic for Timed Agent Network Topologies.

    Clovis Eberhart, James Haydon, Jérémy Dubut, Ahmet Cetinkaya, Sasinee Pruekprasert

    CDC　2870-2877　2022

    DOI： 10.1109/CDC51059.2022.9992550 　

  15. Codensity Games for Bisimilarity.

    Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, Samuel Humeau, Clovis Eberhart, Ichiro Hasuo

    New Generation Computing　40　(2)　403-465　2022

    DOI： 10.1007/s00354-022-00186-y 　

  16. Architecture-Guided Test Resource Allocation Via Logic.

    Clovis Eberhart, Akihisa Yamada 0002, Stefan Klikovits, Shin-ya Katsumata, Tsutomu Kobayashi, Ichiro Hasuo, Fuyuki Ishikawa

    CoRR　abs/2107.10948　2021

  17. Fast Synthesis for Symbolic Self-triggered Control under Right-recursive LTL Specifications.

    Sasinee Pruekprasert, Clovis Eberhart, Jérémy Dubut

    CoRR　abs/2103.16122　2021

  18. Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs.

    Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart, Kohei Suenaga, Kenta Cho 0002, Shin-ya Katsumata

    CoRR　abs/2101.01502　2021

  19. A Compositional Approach to Parity Games.

    Kazuki Watanabe 0003, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo

    Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online(MFPS)　278-295　2021

    DOI： 10.4204/EPTCS.351.17 　

  20. Architecture-Guided Test Resource Allocation via Logic.

    Clovis Eberhart, Akihisa Yamada 0002, Stefan Klikovits, Shin-ya Katsumata, Tsutomu Kobayashi, Ichiro Hasuo, Fuyuki Ishikawa

    Tests and Proofs - 15th International Conference(TAP@STAF)　22-38　2021

    Publisher: Springer

    DOI： 10.1007/978-3-030-79379-1_2 　

  21. Fast Synthesis for Symbolic Self-triggered Control under Right-recursive LTL Specifications.

    Sasinee Pruekprasert, Clovis Eberhart, Jérémy Dubut

    2021 60th IEEE Conference on Decision and Control (CDC)(CDC)　1321-1328　2021

    Publisher: IEEE

    DOI： 10.1109/CDC45484.2021.9683328 　

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

    CoRR　abs/2010.11663　2020

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

    16th International Conference on Control, Automation, Robotics and Vision(ICARCV)　548-554　2020

    Publisher: IEEE

    DOI： 10.1109/ICARCV50220.2020.9305387 　

  24. Fibred pseudo double categories for game semantics

    Clovis Eberhart, Tom Hirschowitz

    Theory and Applications of Categories　34　514-572　2019

    Publisher: Mount Allison University

    ISSN： 1201-561X

  25. Moment Propagation of Discrete-Time Stochastic Polynomial Systems using Truncated Carleman Linearization.

    Sasinee Pruekprasert, Toru Takisaka, Clovis Eberhart, Ahmet Cetinkaya, Jérémy Dubut

    CoRR　abs/1911.12683　2019

  26. Template Games, Simple Games, and Day Convolution.

    Clovis Eberhart, Tom Hirschowitz, Alexis Laouar

    4th International Conference on Formal Structures for Computation and Deduction(FSCD)　16-19　2019

    Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik

    DOI： 10.4230/LIPIcs.FSCD.2019.16 　

  27. History-Dependent Nominal μ-Calculus.

    Clovis Eberhart, Bartek Klin

    34th Annual ACM/IEEE Symposium on Logic in Computer Science(LICS)　1-13　2019

    Publisher: IEEE

    DOI： 10.1109/LICS.2019.8785736 　

  28. Scenario Sampling for Cyber Physical Systems using Combinatorial Testing.

    Akihisa Yamada 0002, Clovis Eberhart, Fuyuki Ishikawa, Nian-Ze Lee

    2019 IEEE International Conference on Software Testing, Verification and Validation Workshops　198-199　2019

    Publisher: IEEE

    DOI： 10.1109/ICSTW.2019.00053 　

  29. Categories and String Diagrams for Game Semantics

    Clovis Eberhart

    2018/06/22

    DOI： 10.70675/77200150z215az474az87efz14656ede0998 　

  30. Categories and String Diagrams for Game Semantics

    Clovis Eberhart

    2018/06/22

    More details Close

    Game semantics is a class of models of programming languages in which types are interpreted as games and programs as strategies. Such game models have successfully covered diverse features, such as functional and imperative programming, or control operators. They have recently been extended to non-deterministic and concurrent languages, which generated an in-depth recasting of the standard approach: plays are now organised into a category, on which strategies are presheaves. The fundamental notion of innocence has also been recast as a sheaf condition. This thesis is a study of various constructions appearing in this new approach to game semantics.We first consider a pattern common to several game models of concurrent languages, in which games and plays are first organised into a double category, from which strategies are then derived. We provide an abstract construction of such a double category from more basic data, and prove that, under suitable hypotheses, the result allows the construction of strategies.Our second contribution is to relate two established techniques for defining plays: the standard one, based on justified sequences, and a more recent one, based on string diagrams. We (fully) embed the former into the latter and prove that they induce essentially the same model.Finally, we propose an axiomatisation of the notions of game and play, from which we formally derive a category of games and strategies. We also refine the axioms to deal with innocence, and prove that, under suitable hypotheses, innocent strategies are stable under composition.

  31. Simple game semantics and Day convolution.

    Clovis Eberhart, Tom Hirschowitz, Alexis Laouar

    CoRR　abs/1810.06991　2018

  32. What's in a game?: A theory of game models.

    Clovis Eberhart, Tom Hirschowitz

    Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science(LICS)　374-383　2018

    Publisher: ACM

    DOI： 10.1145/3209108.3209114 　

  33. Categories and String Diagrams for Game Semantics. (Catégories et diagrammes de cordes pour les jeux concurrents).

    Clovis Eberhart

    2018

  34. Game semantics as a singular functor, and definability as geometric realisation

    Clovis Eberhart, Tom Hirschowitz

    2017

    More details Close

    Game semantics is a class of models of programming languages in which types are interpreted as games and programs as strategies. Though originally designed for sequential languages, its scope has recently been extended to concurrent ones. A salient feature of game semantics is the notion of innocence, which requires strategies to be determined by their values on a certain class of plays, called views. In previous work, we have obtained a representation theorem for Tsukada and Ong's categories of views and plays, in particular by constructing an embedding V of views into a coslice of a certain presheaf category. We here exploit this result to exhibit an efficient categorical account of two crucial constructions of game semantics. First, we recover the interpretation of normal forms into innocent strategies as the singular functor associated to V. Second, the corresponding geometric realisation functor yields the standard definability result saying that any innocent strategy is (isomorphic to) the interpretation of a normal form.

  35. What's in a game? A theory of game models.

    Clovis Eberhart, Tom Hirschowitz

    CoRR　abs/1711.10860　2017

  36. An intensionally fully-abstract sheaf model for π (expanded version).

    Clovis Eberhart, Tom Hirschowitz, Thomas Seiller

    CoRR　abs/1710.06744　2017

  37. Justified Sequences in String Diagrams: a Comparison Between Two Approaches to Concurrent Game Semantics.

    Clovis Eberhart, Tom Hirschowitz

    7th Conference on Algebra and Coalgebra in Computer Science(CALCO)　10-16　2017

    Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik

    DOI： 10.4230/LIPIcs.CALCO.2017.10 　

  38. An intensionally fully-abstract sheaf model for π (expanded version).

    Clovis Eberhart, Tom Hirschowitz, Thomas Seiller

    Logical Methods in Computer Science　13　(4)　2017

    DOI： 10.23638/LMCS-13(4:9)2017 　

  39. Justified sequences in string diagrams

    Clovis Eberhart, Tom Hirschowitz

    2016

    More details Close

    We compare two approaches to concurrent game semantics, one by Tsukada and Ong for a simply-typed λ-calculus and the other by the authors and collaborators for CCS and the π-calculus. The two approaches are obviously related, as they both define strategies as sheaves for the Grothendieck topology induced by embedding ‘views’ into ‘plays’. However, despite this superficial similarity, the notions of views and plays differ significantly: the former is based on standard justified sequences, the latter uses string diagrams. In this paper, we relate both approaches at the level of plays. Specifically, we design a notion of play (resp. view) for the simply-typed λ-calculus, based on string diagrams as in our previous work, into which we fully embed Tsukada and Ong's plays (resp. views). We further provide a categorical explanation of why both notions yield essentially the same model, thus demonstrating that the difference is a matter of presentation. In passing, we introduce an abstract framework for producing sheaf models based on string diagrams, which unifies our present and previous models.

  40. An Intensionally Fully-abstract Sheaf Model for pi.

    Clovis Eberhart, Tom Hirschowitz, Thomas Seiller

    6th Conference on Algebra and Coalgebra in Computer Science(CALCO)　86-100　2015

    Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik

    DOI： 10.4230/LIPIcs.CALCO.2015.86 　

  41. Fully-abstract concurrent games for pi.

    Clovis Eberhart, Tom Hirschowitz, Thomas Seiller

    CoRR　abs/1310.4306　2013

Show all ︎Show first 5