{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T11:18:23Z","timestamp":1781090303926,"version":"3.54.1"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2012,6,1]],"date-time":"2012-06-01T00:00:00Z","timestamp":1338508800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2012,6]]},"abstract":"<jats:p>\n            We define when a linear-time temporal property is a\n            <jats:italic>fairness property<\/jats:italic>\n            with respect to a given system. This captures the essence shared by most fairness assumptions that are used in the specification and verification of reactive and concurrent systems, such as weak fairness, strong fairness,\n            <jats:italic>k<\/jats:italic>\n            -fairness, and many others. We provide three characterizations of fairness: a language-theoretic, a game-theoretic, and a topological characterization. It turns out that the fairness properties are the sets that are \u201clarge\u201d from a topological point of view, that is, they are the\n            <jats:italic>co-meager<\/jats:italic>\n            sets in the natural topology of runs of a given system.\n          <\/jats:p>\n          <jats:p>\n            This insight provides a link to probability theory where a set is \u201clarge\u201d when it has measure 1. While these two notions of largeness are similar, they do not coincide in general. However, we show that they coincide for\n            <jats:italic>\u03c9<\/jats:italic>\n            -regular properties and bounded Borel measures. That is, an\n            <jats:italic>\u03c9<\/jats:italic>\n            -regular temporal property of a finite-state system has measure 1 under a bounded Borel measure if and only if it is a fairness property with respect to that system.\n          <\/jats:p>\n          <jats:p>\n            The definition of fairness leads to a generic relaxation of correctness of a system in linear-time semantics. We define a system to be\n            <jats:italic>fairly correct<\/jats:italic>\n            if there exists a fairness assumption under which it satisfies its specification. Equivalently, a system is fairly correct if the set of runs satisfying the specification is topologically large. We motivate this notion of correctness and show how it can be verified in a system.\n          <\/jats:p>","DOI":"10.1145\/2220357.2220360","type":"journal-article","created":{"date-parts":[[2012,7,10]],"date-time":"2012-07-10T16:40:44Z","timestamp":1341938444000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Defining Fairness in Reactive and Concurrent Systems"],"prefix":"10.1145","volume":"59","author":[{"given":"Hagen","family":"V\u00f6lzer","sequence":"first","affiliation":[{"name":"IBM Research---Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniele","family":"Varacca","sequence":"additional","affiliation":[{"name":"PPS-CNRS and Univ Paris Diderot, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 16th International Colloquium on Automata, Languages and Programming. Springer-Verlag, 1--17","author":"Abadi M.","unstructured":"Abadi , M. , Lamport , L. , and Wolper , P . 1989. Realizable and unrealizable specifications of reactive systems . In Proceedings of the 16th International Colloquium on Automata, Languages and Programming. Springer-Verlag, 1--17 . Abadi, M., Lamport, L., and Wolper, P. 1989. Realizable and unrealizable specifications of reactive systems. In Proceedings of the 16th International Colloquium on Automata, Languages and Programming. Springer-Verlag, 1--17."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of 9th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 52--61","author":"Alur R.","unstructured":"Alur , R. and Henzinger , T. A . 1994. Finitary fairness . In Proceedings of 9th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 52--61 . Alur, R. and Henzinger, T. A. 1994. Finitary fairness. In Proceedings of 9th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 52--61."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/647764.735679"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01872848"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_6"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02242712"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(98)00038-6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.25"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0010"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39813-4_16"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(84)90114-5"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90390-2"},{"key":"e_1_2_1_17_1","unstructured":"Dugundji J. 1966. Topology. Allyn and Bacon. Dugundji J. 1966. Topology . Allyn and Bacon."},{"key":"e_1_2_1_18_1","volume-title":"Handbook of Theoretical Computer Science","author":"Emerson E. A.","unstructured":"Emerson , E. A. 1990. Temporal and modal logic . In Handbook of Theoretical Computer Science , Volume B: Formal Models and Sematics (B). MIT Press and Elsevier, 995-- 1072 . Emerson, E. A. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B). MIT Press and Elsevier, 995--1072."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-003-0091-y"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Francez N. 1986. Fairness. Springer. Francez N. 1986. Fairness . Springer.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 28th FSTTCS. LIPIcs 2 Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik.","author":"Gr\u00e4del E.","year":"2008","unstructured":"Gr\u00e4del , E. 2008 . Banach-Mazur games on graphs . In Proceedings of the 28th FSTTCS. LIPIcs 2 Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik. Gr\u00e4del, E. 2008. Banach-Mazur games on graphs. In Proceedings of the 28th FSTTCS. LIPIcs 2 Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.01.005"},{"key":"e_1_2_1_23_1","series-title":"Lecture Notes in Computer Science Series","volume-title":"Proceedings of 10th CONCUR","author":"Joung Y.-J.","unstructured":"Joung , Y.-J. 1999. Localizability of fairness constraints and their distributed implementations . In Proceedings of 10th CONCUR . Lecture Notes in Computer Science Series , vol. 1664 , Springer , 336--351. Joung, Y.-J. 1999. Localizability of fairness constraints and their distributed implementations. In Proceedings of 10th CONCUR. Lecture Notes in Computer Science Series, vol. 1664, Springer, 336--351."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.3014"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/9.2.135"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.34"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0950-5849(89)90159-6"},{"key":"e_1_2_1_28_1","volume-title":"Topology and Category Theory in Computer Science","author":"Kwiatkowska M. Z.","unstructured":"Kwiatkowska , M. Z. 1991. On topological characterization of behavioural properties . In Topology and Category Theory in Computer Science , G. Reed, A. Roscoe, and R. Wachter Eds., Oxford University Press , 153--177. Kwiatkowska, M. Z. 1991. On topological characterization of behavioural properties. In Topology and Category Theory in Computer Science, G. Reed, A. Roscoe, and R. Wachter Eds., Oxford University Press, 153--177."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/PL00008921"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01691063"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(82)91022-1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/646235.682695"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/648065.747612"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/93385.93442"},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A. 1992. The Temporal Logic of Reactive and Concurrent Systems -- Specification. Springer. Manna Z. and Pnueli A. 1992. The Temporal Logic of Reactive and Concurrent Systems -- Specification . Springer.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_2_1_37_1","volume-title":"The Scottish Book: Mathematics from the Scottish Cafe","author":"Mauldin R. D.","unstructured":"Mauldin , R. D. 1981. The Scottish Book: Mathematics from the Scottish Cafe . Birkh\u00e4user . Mauldin, R. D. 1981. The Scottish Book: Mathematics from the Scottish Cafe. Birkh\u00e4user."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_2_1_39_1","volume-title":"Contributions to the Theory of Games","author":"Oxtoby J. C.","unstructured":"Oxtoby , J. C. 1957. The Banach-Mazur game and Banach category theorem . In Contributions to the Theory of Games , Vol. III . Annals of Mathematical Studies Series, vol. 39, Princeton University Press , 159--163. Oxtoby, J. C. 1957. The Banach-Mazur game and Banach category theorem. In Contributions to the Theory of Games, Vol. III. Annals of Mathematical Studies Series, vol. 39, Princeton University Press, 159--163."},{"key":"e_1_2_1_40_1","volume-title":"A Survey of the Analogies between Topological and Measure Spaces","author":"Oxtoby J. C.","unstructured":"Oxtoby , J. C. 1971. Measure and Category. A Survey of the Analogies between Topological and Measure Spaces . Springer . Oxtoby, J. C. 1971. Measure and Category. A Survey of the Analogies between Topological and Measure Spaces. Springer."},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of 18th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 234--243","author":"Pistore M.","unstructured":"Pistore , M. and Vardi , M. Y . 2003. The planning spectrum - one, two, three, infinity . In Proceedings of 18th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 234--243 . Pistore, M. and Vardi, M. Y. 2003. The planning spectrum - one, two, three, infinity. In Proceedings of 18th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 234--243."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808757"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/3405"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/1781794.1781840"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_39"},{"key":"e_1_2_1_47_1","series-title":"Handbook of Logic in Computer Science","volume-title":"Background: Mathematical Structures","author":"Smyth M. B.","unstructured":"Smyth , M. B. 1992. Topology . In Handbook of Logic in Computer Science , S. Abramsky, D. M. Gabbay, and T. Maibaum Eds. Vol. 1 : Background: Mathematical Structures . Oxford University Press , 641--761. Smyth, M. B. 1992. Topology. In Handbook of Logic in Computer Science, S. Abramsky, D. M. Gabbay, and T. Maibaum Eds. Vol. 1: Background: Mathematical Structures. Oxford University Press, 641--761."},{"key":"e_1_2_1_48_1","volume-title":"Principles of Random Walk","author":"Spitzer F.","unstructured":"Spitzer , F. 2001. Principles of Random Walk . Springer . Spitzer, F. 2001. Principles of Random Walk. Springer."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1216\/RMJ-1987-17-2-227"},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","unstructured":"Thomas W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science J. van Leeuwen Ed. Vol. B: Formal Models and Semantics. Elsevier. Thomas W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science J. van Leeuwen Ed. Vol. B: Formal Models and Semantics. Elsevier.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.49"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.12"},{"key":"e_1_2_1_53_1","series-title":"Lecture Notes in Computer Science Series","volume-title":"Proceedings of 13th CONCUR","author":"V\u00f6lzer H.","unstructured":"V\u00f6lzer , H. 2002. Refinement-robust fairness . In Proceedings of 13th CONCUR . Lecture Notes in Computer Science Series , vol. 2421 , Springer , 547--561. V\u00f6lzer, H. 2002. Refinement-robust fairness. In Proceedings of 13th CONCUR. Lecture Notes in Computer Science Series, vol. 2421, Springer, 547--561."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/11561927_5"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_35"},{"key":"e_1_2_1_56_1","volume-title":"Probability with Martingales","author":"Williams D.","unstructured":"Williams , D. 1991. Probability with Martingales . Cambridge University Press . Williams, D. 1991. Probability with Martingales. Cambridge University Press."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/646541.696191"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2220357.2220360","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2220357.2220360","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:00:46Z","timestamp":1750276846000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2220357.2220360"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6]]},"references-count":56,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,6]]}},"alternative-id":["10.1145\/2220357.2220360"],"URL":"https:\/\/doi.org\/10.1145\/2220357.2220360","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6]]},"assertion":[{"value":"2011-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-06-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}