Labelled transition systems as a Stone space

摘要

A fully abstract and universal domain model for modal transition systems andrefinement is shown to be a maximal-points space model for the bisimulationquotient of labelled transition systems over a finite set of events. In thisdomain model we prove that this quotient is a Stone space whose compact,zero-dimensional, and ultra-metrizable Hausdorff topology measures the degreeof bisimilarity such that image-finite labelled transition systems are dense.Using this compactness we show that the set of labelled transition systems thatrefine a modal transition system, its ''set of implementations'', is compactand derive a compactness theorem for Hennessy-Milner logic on suchimplementation sets. These results extend to systems that also have partiallyspecified state propositions, unify existing denotational, operational, andmetric semantics on partial processes, render robust consistency measures formodal transition systems, and yield an abstract interpretation of compact setsof labelled transition systems as Scott-closed sets of modal transitionsystems.