  The classical Hennessy-Milner theorem is an important tool in the analysis of
concurrent processes; it guarantees that any two non-bisimilar states in
finitely branching labelled transition systems can be distinguished by a modal
formula. Numerous variants of this theorem have since been established for a
wide range of logics and system types, including quantitative versions where
lower bounds on behavioural distance (e.g.~in weighted, metric, or
probabilistic transition systems) are witnessed by quantitative modal formulas.
Both the qualitative and the quantitative versions have been accommodated
within the framework of coalgebraic logic, with distances taking values in
quantales, subject to certain restrictions, such as being so-called value
quantales. While previous quantitative coalgebraic Hennessy-Milner theorems
apply only to liftings of set functors to (pseudo-)metric spaces, in the
present work we provide a quantitative coalgebraic Hennessy-Milner theorem that
applies more widely to functors native to metric spaces; notably, we thus
cover, for the first time, the well-known Hennessy-Milner theorem for
continuous probabilistic transition systems, where transitions are given by
Borel measures on metric spaces, as an instance. In the process, we also relax
the restrictions imposed on the quantale, and additionally parametrize the
technical account over notions of closure and, hence, density, providing
associated variants of the Stone-Weierstrass theorem; this allows us to cover,
for instance, behavioural ultrametrics.
