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) and axiomatisability (can we reason about models using specifications). I will also investigate notions of reductions between problems. This is ongoing work, building on my RAMICS 2026 paper as well as joint work with Uli Fahrenberg (LMF).