{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:50Z","timestamp":1761611150017,"version":"3.41.2"},"reference-count":40,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2005,1,26]],"date-time":"2005-01-26T00:00:00Z","timestamp":1106697600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.2168\/lmcs-1(1:1)2005","type":"journal-article","created":{"date-parts":[[2005,2,8]],"date-time":"2005-02-08T12:35:09Z","timestamp":1107866109000},"source":"Crossref","is-referenced-by-count":6,"title":["Labelled transition systems as a Stone space"],"prefix":"10.46298","volume":"Volume 1, Issue 1","author":[{"given":"Michael","family":"Huth","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2005,1,26]]},"reference":[{"key":"10.2168\/LMCS-1(1:1)2005_abramsky91","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1991.9999"},{"key":"10.2168\/LMCS-1(1:1)2005_abramsky94","doi-asserted-by":"crossref","unstructured":"S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors,Handbook of Logic in Computer Science, volume 3, pages 1--168. Oxford Univ. Press, 1994.","DOI":"10.1093\/oso\/9780198537625.003.0001"},{"key":"10.2168\/LMCS-1(1:1)2005_alessi97","doi-asserted-by":"crossref","unstructured":"F. Alessi, P. Baldan, and F. Honsell. Partializing Stone spaces using SFP domains. In M. Bidoit and M. Dauchet, editors,TAPSOFT'97 Conference Proceedings, volume 1214 ofLecture Notes in Computer Science, pages 478--489, Lille, France, 14-18 April 1997. Springer Verlag.","DOI":"10.1007\/BFb0030620"},{"key":"10.2168\/LMCS-1(1:1)2005_alessi03","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00037-3"},{"key":"10.2168\/LMCS-1(1:1)2005_bruns99","doi-asserted-by":"crossref","unstructured":"G. Bruns and P. Godefroid. Model Checking Partial State Spaces with 3-Valued Temporal Logics. InProc. of the 11th International Conference on Computer Aided Verification, volume 1633 ofLecture Notes in Computer Science, pages 274--287. Springer Verlag, July 1999.","DOI":"10.1007\/3-540-48683-6_25"},{"key":"10.2168\/LMCS-1(1:1)2005_bruns2000","doi-asserted-by":"crossref","unstructured":"G. Bruns and P. Godefroid. Generalized Model Checking: Reasoning about Partial State Spaces. InProc. of the 11th International Conference on Concurrency Theory, volume 1877 ofLecture Notes in Computer Science, pages 168--182. Springer Verlag, August 2000.","DOI":"10.1007\/3-540-44618-4_14"},{"key":"10.2168\/LMCS-1(1:1)2005_CN76","doi-asserted-by":"crossref","unstructured":"B. Courcelle and M. Nivat. Algebraic families of interpretations. InProc. of the 17th IEEE Symposium on Foundations of Computer Science, pages 137--146, October 1976.","DOI":"10.1109\/SFCS.1976.3"},{"key":"10.2168\/LMCS-1(1:1)2005_cousot77","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs. InProc. of the 4th ACM Symposium on Principles of Programming Languages, pages 238--252, Los Angeles, California. ACM Press, 1977. D. Dams.Abstract interpretation and partition refinement for model checking. PhD thesis, Technische Universiteit Eindhoven, The Netherlands, 1996.","DOI":"10.1145\/512950.512973"},{"key":"10.2168\/LMCS-1(1:1)2005_dams04","doi-asserted-by":"crossref","unstructured":"D. Dams and K. Namjoshi. The Existence of Finite Abstractions for Branching Time Model Checking. InProc. of the Nineteenth Annual IEEE Symposium on Logic in Computer Science, pages 335-344, 13-17 July, Turku, Finland. IEEE Computer Society Press, 2004.","DOI":"10.1109\/LICS.2004.1319628"},{"key":"10.2168\/LMCS-1(1:1)2005_damsGerthGrumberg97","doi-asserted-by":"crossref","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems.ACM TOPLAS, 19:253--291, 1997. J. W. de Bakker and J. I. Zucker. Denotational Semantics Of Concurrency. InProc. 14th Annual ACM Symposium on Theory of Computing, pages 153--158, New York, New York, 1982. ACM Press.","DOI":"10.1145\/244795.244800"},{"key":"10.2168\/LMCS-1(1:1)2005_BZ_acm82","doi-asserted-by":"crossref","unstructured":"J. W. de Bakker and J. I. Zucker. Denotational Semantics Of Concurrency. InProc.14th Annual ACM Symposium on Theory of Computing, pages 153-158, New York, New York, 1982. ACM Press.","DOI":"10.1145\/800070.802188"},{"key":"10.2168\/LMCS-1(1:1)2005_radha00","doi-asserted-by":"crossref","unstructured":"J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Approximating Labeled Markov Processes. InProc. of the 15th Annual IEEE Symposium on Logic in Computer Science, pages 95--106, Santa Barbara, California, 26-29 June 2000. IEEE Computer Society Press.","DOI":"10.1109\/LICS.2000.855759"},{"journal-title":"In {\\em Proc. of the 17th Annual IEEE Symposium on Logic in Computer Science}, pages 413-422, Copenhagen, Denmark, July 2002. IEEE Computer Society","author":"Desharnais","key":"10.2168\/LMCS-1(1:1)2005_radha02"},{"issue":"1","key":"10.2168\/LMCS-1(1:1)2005_dipierrojcs02","doi-asserted-by":"crossref","first-page":"37","DOI":"10.3233\/JCS-2004-12103","volume":"12","author":"Di Pierro","year":"2004","journal-title":"Journal of Computer Security"},{"key":"10.2168\/LMCS-1(1:1)2005_gause89","unstructured":"D. C. Gause and G. M. Weinberg.Exploring Requirements: Quality Before Design. Dorset House Publishing, 353 West 12th Street, New York, NY 10014, 1989."},{"key":"10.2168\/LMCS-1(1:1)2005_gierz80","doi-asserted-by":"crossref","unstructured":"G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott. A Compendium of Continuous Lattices. Springer Verlag, 1980. P. Godefroid, M. Huth, and R. Jagadeesan. Abstraction-based Model Checking using Modal Transition Systems. InProc. of the 12th International Conference on Theory and Practice of Concurrency, volume 2154 ofLecture Notes in Computer Science, pages 426-440. Springer Verlag, August 2001.","DOI":"10.1007\/3-540-44685-0_29"},{"key":"10.2168\/LMCS-1(1:1)2005_gj02","doi-asserted-by":"crossref","unstructured":"P. Godefroid and R. Jagadeesan. Automatic Abstraction Using Generalized Model Checking. In E. Brinksma and K. G. Larsen, editors,Proc. of the 14th International Conference on Computer Aided Verification, volume 2404 ofLecture Notes in Computer Science, pages 137-150, Copenhagen, Denmark, July 2002. Springer Verlag.","DOI":"10.1007\/3-540-45657-0_11"},{"key":"10.2168\/LMCS-1(1:1)2005_gj03","doi-asserted-by":"crossref","unstructured":"P. Godefroid and R. Jagadeesan. On The Expressiveness of 3-Valued Models. In L. D. Zuck, P. C. Attie, A. Cortesi, and S. Mukhopadhyay, editors,Proc. of the 4th International Conference on Verification, Model Checking and Abstract Interpretation, volume 2575 ofLNCS, pages 206-222, New York, January 2003. Springer Verlag.","DOI":"10.1007\/3-540-36384-X_18"},{"key":"10.2168\/LMCS-1(1:1)2005_GWWT77","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321997"},{"key":"10.2168\/LMCS-1(1:1)2005_gunter92a","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90017-A"},{"key":"10.2168\/LMCS-1(1:1)2005_heckmann90","doi-asserted-by":"crossref","unstructured":"R. Heckmann. Set Domains. InProc. of the 3rd European Symposium on Programming, volume 432 ofLecture Notes in Computer Science, pages 177-196. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52592-0_63"},{"key":"10.2168\/LMCS-1(1:1)2005_hennessy85","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"10.2168\/LMCS-1(1:1)2005_huth_isola04","unstructured":"A. Hussain and M. Huth. On model checking multiple hybrid views.Preliminary Proc. of the First International Symposium on Leveraging Applications of Formal Method, 15 pages, 30 October - 2 November, Paphos, Cyprus, 2004."},{"key":"10.2168\/LMCS-1(1:1)2005_hjs01","doi-asserted-by":"crossref","unstructured":"M. Huth, R. Jagadeesan, and D. A. Schmidt. Modal transition systems: a foundation for three-valued program analysis. In D. Sands, editor,Proc. of ESOP'2001, pages 155-169. Springer Verlag, April 2001.","DOI":"10.1007\/3-540-45309-1_11"},{"issue":"4","key":"10.2168\/LMCS-1(1:1)2005_hjs04","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1017\/S0960129504004268","volume":"14","author":"Huth","year":"2004","journal-title":"{\\em Mathematical Structures in Computer Science}, 14(4):469-505, Cambridge University Press, August 2004"},{"key":"10.2168\/LMCS-1(1:1)2005_huth_refinement04","unstructured":"M. Huth. Refinement is complete for implementations. Revised version submitted, 27 pages, August 2004. Under review."},{"key":"10.2168\/LMCS-1(1:1)2005_huth_lics04","doi-asserted-by":"crossref","unstructured":"M. Huth. Beyond image-finiteness: labelled transition systems as a Stone space. In:Proc. of the Nineteenth Annual IEEE Symposium on Logic in Computer Science, pages 222-231, 13-17 July, Turku, Finland, IEEE Computer Society Press, 2004.","DOI":"10.1109\/LICS.2004.1319616"},{"key":"10.2168\/LMCS-1(1:1)2005_jacksonviews95","doi-asserted-by":"publisher","DOI":"10.1145\/226241.226249"},{"key":"10.2168\/LMCS-1(1:1)2005_kozen83a","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"10.2168\/LMCS-1(1:1)2005_larsen89b","doi-asserted-by":"crossref","unstructured":"K. G. Larsen. Modal Specifications. In J. Sifakis, editor,Automatic Verification Methods for Finite State Systems, number 407 in Lecture Notes in Computer Science, pages 232-246. Springer Verlag, June 12-14 1989. International Workshop, Grenoble, France.","DOI":"10.1007\/3-540-52148-8_19"},{"key":"10.2168\/LMCS-1(1:1)2005_larsen88","doi-asserted-by":"crossref","unstructured":"K. G. Larsen and B. Thomsen. A Modal Process Logic. InProc. of the Third Annual IEEE Symposium on Logic in Computer Science, pages 203-210. IEEE Computer Society Press, 1988.","DOI":"10.1109\/LICS.1988.5119"},{"key":"10.2168\/LMCS-1(1:1)2005_lawson97","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002363"},{"year":"1989","author":"Milner","key":"10.2168\/LMCS-1(1:1)2005_milner89"},{"issue":"1","key":"10.2168\/LMCS-1(1:1)2005_mislove03","volume":"65","author":"Mislove","year":"2003","journal-title":"Electronic Notes in Theoretical Computer Science pages, 2003"},{"key":"10.2168\/LMCS-1(1:1)2005_nicola84","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"10.2168\/LMCS-1(1:1)2005_nuseibeh94","doi-asserted-by":"publisher","DOI":"10.1109\/32.328995"},{"year":"2001","author":"Ryan","key":"10.2168\/LMCS-1(1:1)2005_ryan01"},{"key":"10.2168\/LMCS-1(1:1)2005_sattler01","unstructured":"U. Sattler and M. Vardi. The Hybrid\u03bc-calculus. In R. Gor\u00e9, A. Leitsch, and T. NipkovProc. of the First International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science 2083, pages 76-91, Siena, Italy, 18-23 June, Springer Verlag, 2001. D. S. Scott.Formal semantics of programming languages, volume 2 ofCourant Computer Science Symposia, chapter:Lattice theory, data types and semantics, pages 65-106. Prentice-Hall, 1972."},{"key":"10.2168\/LMCS-1(1:1)2005_sommerville98","doi-asserted-by":"crossref","unstructured":"I. Sommerville, P. Sawyer, and S. Viller. Viewpoints for requirements elicitation: a practical approach. InProc. of the 1998 International Conference on Requirements Engineering, Colorado Springs, Colorado, April 6-10 1998. IEEE Computer Society Press.","DOI":"10.1109\/ICRE.1998.667811"},{"key":"10.2168\/LMCS-1(1:1)2005_vickers89","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Topology via Logic","author":"Vickers","year":"1989","edition":"5"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2271\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2271\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,22]],"date-time":"2024-01-22T16:46:17Z","timestamp":1705941977000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2271"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1,26]]},"references-count":40,"URL":"https:\/\/doi.org\/10.2168\/lmcs-1(1:1)2005","relation":{"is-same-as":[{"id-type":"arxiv","id":"cs\/0412063","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.cs\/0412063","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2005,1,26]]},"article-number":"2271"}}