Labelled transition systems as a stone space
File(s)
Published version
OA Location
Author(s)
Huth,M.
Type
Journal Article
Abstract
A fully abstract and universal domain model for modal transition systems and refinement is shown to be a maximal-points space model for the bisimulation quotient of labelled transition systems over a finite set of events. In this domain model we prove that this quotient 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. Using this compactness we show that the set of labelled transition systems that refine a modal transition system, its ''set of implementations'', is compact and derive a compactness theorem for Hennessy-Milner logic on such implementation sets. These results extend to systems that also have partially specified state propositions, unify existing denotational, operational, and metric semantics on partial processes, render robust consistency measures for modal transition systems, and yield an abstract interpretation of compact sets of labelled transition systems as Scott-closed sets of modal transition systems.
Editor(s)
Escardó, Martín
Date Issued
2005
Date Acceptance
2004-09-01
Citation
Logical Methods in Computer Science, 2005, 1, 1 (1), pp.1-28
ISSN
1860-5974
Start Page
1
End Page
28
Journal / Book Title
Logical Methods in Computer Science
Volume
1
Issue
1
Copyright Statement
© 2005 M. Huth. 28
M. HUTH
[42] I. Sommerville, P. Sawyer, and S. Viller. Viewpoints fo
r requirements elicitation: a practical ap-
proach. In
Proc. of the 1998 International Conference on Requirements
Engineering
, Colorado
Springs, Colorado, April 6-10 1998. IEEE Computer Society P
ress.
[43] S. Vickers.
Topology via Logic
. Cambridge Tracts in Theoretical Computer Science 5, 1989.
This work is licensed under the Creative Commons Attributio
n-NoDerivs License. To view
a copy of this license, visit
http://creativecommons.org/licenses/by-nd/2.0/
M. HUTH
[42] I. Sommerville, P. Sawyer, and S. Viller. Viewpoints fo
r requirements elicitation: a practical ap-
proach. In
Proc. of the 1998 International Conference on Requirements
Engineering
, Colorado
Springs, Colorado, April 6-10 1998. IEEE Computer Society P
ress.
[43] S. Vickers.
Topology via Logic
. Cambridge Tracts in Theoretical Computer Science 5, 1989.
This work is licensed under the Creative Commons Attributio
n-NoDerivs License. To view
a copy of this license, visit
http://creativecommons.org/licenses/by-nd/2.0/
Subjects
cs.LO
F.3.2; F.4.1
0101 Pure Mathematics
0803 Computer Software
0802 Computation Theory And Mathematics
Edition
1
Publication Status
Published
Date Publish Online
2005-01-26