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: TBA
