Beyond image-finiteness: labelled transition systems as a Stone space

The bisimulation quotient of labelled transition systems over a finite set of events is a Stone space whose compact, zero-dimensional, and ultra-metrizable Hausdorff topology measures the degree of bisimilarity such that image-finite labelled transition systems are dense. A fully abstract domain for modal transition systems, modulo refinement, realizes this Stone space as a ´maximal-points space´. Therefore, we extend our results to those systems; unify existing denotational, operational, and metric semantics; and obtain consistency measures for modal transition systems.