Some results in dynamic model theory

First-order structures over a fixed signature Σ give rise to a family of trace-based and relational Kleene algebras with tests defined in terms of Tarskian frames. A Tarskian frame is a Kripke frame whose states are valuations of program variables and whose atomic actions are state changes effected by variable assignments x≔e, where e is a Σ-term. The Kleene algebras with tests that arise in this way play a role in dynamic model theory akin to the role played by Lindenbaum algebras in classical first-order model theory. Given a first-order theory T over Σ, we exhibit a Kripke frame U whose trace algebra TrU is universal for the equational theory of Tarskian trace algebras over Σ satisfying T, although U itself is not Tarskian in general. The corresponding relation algebra RelU is not universal for the equational theory of relation algebras of Tarskian frames, but it is so modulo observational equivalence.