LACL, bâtiment P4 niveau 4, salle 423 (P4-423)comment aller au LACL, comment trouver la salle.
Abstract: In this talk I will show how techniques from relation algebra can be used to discuss various properties of model-checking problems. Such problems will be viewed as arbitrary binary relations, between an abstract set of models, and one of specifications. In particular I will discuss expressivity (are there enough specifications to describe each model), axiomatisability (can we reason about models using specifications), and adequacy (is behavioural equivalence captured by logical equivalence). If time allows I will also investigate notions of reductions and translations between problems. This is ongoing work, building on my RAMICS 2026 paper as well as joint work with Uli Fahrenberg (LMF).
Abstract: Hybrid games provide a natural framework for modeling systems that combine discrete decisions with continuous dynamics. In such games, Player~1 typically represents the controller trying to enforce a desired objective, while Player~2 models the environment or adversarial behaviors. Verification and strategy synthesis problems for hybrid games are often highly complex or undecidable in the general case. In this talk, I will present a framework based on alternating bisimulation relations for the formal abstraction of classes of hybrid turn-based games into timed turn-based games. The main objective is to preserve the existence of winning strategies while reducing the analysis to simpler and decidable timed models. This approach makes it possible to benefit from existing algorithms and verification tools developed for timed games. In particular, I will discuss abstractions from singular hybrid games to timed games and the preservation of strategic properties through these abstractions. Finally, I will present a temporal logical framework adapted to hybrid games, allowing strategic, timing, and variable-valuation objectives to be expressed. I will also introduce an alternating simulation relation preserving the existence of winning strategies for objectives specified in this logic.
