{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T14:58:52Z","timestamp":1780930732848,"version":"3.54.1"},"reference-count":18,"publisher":"World Scientific Pub Co Pte Lt","issue":"04","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2003,8]]},"abstract":"<jats:p> Distributed protocols are often composed of similar processes connected in a unidirectional ring network. Processes communicate by passing a token in a fixed direction; the process that holds the token is allowed to perform certain actions. Usually, correctness properties are expected to hold irrespective of the size of the ring. We show that the question of checking many useful correctness properties for rings of all sizes can be reduced to checking them on ring of sizes up to a small cutoff size. We apply our results to the verification of a mutual exclusion protocol and Milner's scheduler protocol. <\/jats:p>","DOI":"10.1142\/s0129054103001881","type":"journal-article","created":{"date-parts":[[2003,9,19]],"date-time":"2003-09-19T10:19:32Z","timestamp":1063966772000},"page":"527-549","source":"Crossref","is-referenced-by-count":62,"title":["On Reasoning About Rings"],"prefix":"10.1142","volume":"14","author":[{"given":"E. Allen","family":"Emerson","sequence":"first","affiliation":[{"name":"Computer Sciences Department and Computer Engineering Research Center, University of Texas at Austin, Austin, Texas 78712, United States of America"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[{"name":"Bell Laboratories, Lucent Technologies, 600-700 Mountain Avenue, Murray Hill, NJ 07074, United States of America"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"reference":[{"key":"rf1","first-page":"307","volume":"15","author":"Apt K.","journal-title":"IPL"},{"key":"rf2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"rf3","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90026-6"},{"key":"rf5","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"rf9","first-page":"455","author":"Clarke E. M.","journal-title":"Computer Science Today"},{"key":"rf10","series-title":"LNCS 407","volume-title":"Automatic Verification Methods for Finite State Systems","author":"Cleaveland R."},{"key":"rf11","series-title":"Prentice-Hall International Series in Computer Science","volume-title":"Mathematical Logic and Programming Languages","author":"Dijkstra E. W."},{"key":"rf12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"rf13","volume-title":"Handbook of Theoretical Computer Science","author":"Emerson E. A.","year":"1991"},{"key":"rf14","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"rf18","volume":"39","author":"German S. M.","journal-title":"J. ACM"},{"key":"rf19","author":"Keller R. M.","journal-title":"CACM"},{"key":"rf21","volume":"20","author":"Li J.","journal-title":"IEEE Trans. Soft. Engg."},{"key":"rf22","series-title":"Prentice-Hall International Series in Computer Science","volume-title":"Communication and Concurrency","author":"Milner R."},{"key":"rf23","volume-title":"Computation : Finite and Infinite Machines","author":"Minsky M.","year":"1962"},{"key":"rf25","volume-title":"Parallel Program Design : A Foundation","author":"Misra J.","year":"1988"},{"key":"rf26","doi-asserted-by":"crossref","unstructured":"Z.\u00a0Manna and A.\u00a0Pnueli, Specification and Validation Methods, ed. E.\u00a0Borger (Oxford University Press, 1994)\u00a0pp. 167\u2013230.","DOI":"10.1007\/978-1-4612-4222-2_3"},{"key":"rf34","series-title":"LNCS 407","volume-title":"Automatic Verification Methods for Finite State Systems","author":"Wolper P."}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054103001881","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T00:37:45Z","timestamp":1565138265000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129054103001881"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":18,"journal-issue":{"issue":"04","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[2003,8]]}},"alternative-id":["10.1142\/S0129054103001881"],"URL":"https:\/\/doi.org\/10.1142\/s0129054103001881","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}