Model-checking, relationally
Séminaire MeFoSyLoMa
in Créteil,
June 2026
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).
Related talks | ||
|
RAMiCS
in Będlewo,
April 2026.
|
More | |
|
RAMiCS
in Będlewo,
April 2026.
|
More | |
|
Séminaire du LACL
in Créteil,
September 2025
(in French)
.
|
More | |
|
Séminaire Plume
in Lyon,
June 2025.
|
More | |
|
Séminaire 68nqrt
in Rennes,
May 2025.
|
More | |
Related papers | ||
| A 2-adjunction between representations and preorder morphisms (2026) | More | |
| Representations (in RAMiCS 2026) | More | |
| On preorders (2025) | More | |