{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:10:22Z","timestamp":1761610222898,"version":"build-2065373602"},"reference-count":17,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3893,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,12]]},"DOI":"10.1016\/s1571-0661(04)80411-0","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"178-193","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":15,"title":["Stuttering-Insensitive Automata for On-the-fly Detection of Livelock Properties"],"prefix":"10.1016","volume":"66","author":[{"given":"Henri","family":"Hansen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antti","family":"Valmari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"year":"1999","series-title":"Model checking","author":"Clarke","key":"10.1016\/S1571-0661(04)80411-0_NEWBIB1"},{"year":"1990","series-title":"Introduction to algorithms","author":"Cormen","key":"10.1016\/S1571-0661(04)80411-0_NEWBIB2"},{"key":"10.1016\/S1571-0661(04)80411-0_NEWBIB3","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","article-title":"\u201cMemory-efficient algorithms for the verification of temporal properties\u201d","volume":"vol. 1","author":"Courcoubetis","year":"1992","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1571-0661(04)80411-0_NEWBIB4","doi-asserted-by":"crossref","unstructured":"Etessami K. and Holzmann G.: \u201cOptimizing B\u00fcchi Automata\u201d, in Proc. of CONCUR'00, LNCS 1877, 2000.","DOI":"10.1007\/3-540-44618-4_13"},{"key":"10.1016\/S1571-0661(04)80411-0_NEWBIB5","doi-asserted-by":"crossref","unstructured":"Etessami K.: \u201cStutter-invariant Languages, \u03c9-Automata, and Temporal Logic\u201d, in Proc. of CAV'99, pp. 236\u2013248, LNCS 1633, 1999.","DOI":"10.1007\/3-540-48683-6_22"},{"key":"10.1016\/S1571-0661(04)80411-0_NEWBIB6","doi-asserted-by":"crossref","unstructured":"Gastin P. and Oddoux D.: \u201cFast LTL to B\u00fcchi Automata Translation\u201d, in Proc. of CAV'01, pp. 53\u201365, 2001.","DOI":"10.1007\/3-540-44585-4_6"},{"key":"10.1016\/S1571-0661(04)80411-0_NEWBIB7","doi-asserted-by":"crossref","unstructured":"Gerth R., Peled D., Vardi M., and Wolper P.: \u201cSimple on-the-fly automatic verification of linear temporal logic\u201d, in Proc. of PSTV'95, pp. 3\u201318, 1995.","DOI":"10.1007\/978-0-387-34892-6_1"},{"year":"1991","series-title":"Design and Validation of Computer Protocols","author":"Holzmann","key":"10.1016\/S1571-0661(04)80411-0_NEWBIB8"},{"issue":"1","key":"10.1016\/S1571-0661(04)80411-0_NEWBIB9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/7351.7352","article-title":"\u201cA fast mutual exclusion algorithm\u201d","volume":"5","author":"Lamport","year":"1987","journal-title":"ACM Transactions on Computer Systems"},{"key":"10.1016\/S1571-0661(04)80411-0_NEWBIB10","unstructured":"Lamport L.: \u201cWhat good is temporal logic.\u201d. Proc. IFIP 9th World Congress, R.E.A. Mason (editor), North-Holland, pp 657 \u2013 668, 1983."},{"year":"1991","series-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Manna","key":"10.1016\/S1571-0661(04)80411-0_NEWBIB11"},{"key":"10.1016\/S1571-0661(04)80411-0_NEWBIB12","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00121262","article-title":"\u201cCombining partial order reductions with on-the-fly model-checking\u201d","volume":"8","author":"Peled","year":"1996","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1571-0661(04)80411-0_NEWBIB13","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1023\/A:1011202615884","article-title":"\u201cRelaxed Visibility Enhances Partial Order Reduction\u201d","volume":"19","author":"Peled","year":"2001","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1571-0661(04)80411-0_NEWBIB14","doi-asserted-by":"crossref","unstructured":"Somenzi F. and Bloem R.: \u201cEfficient Buchi Automata form LTL formulae\u201d, in Proc. of CAV'00, LNCS 1855, pp. 247\u2013263, 2000.","DOI":"10.1007\/10722167_21"},{"key":"10.1016\/S1571-0661(04)80411-0_NEWBIB15","series-title":"Handbook of Formal Languages","first-page":"389","article-title":"\u201cLanguages, Automata, and Logic\u201d","author":"Thomas","year":"1997"},{"key":"10.1016\/S1571-0661(04)80411-0_NEWBIB16","series-title":"Modelling and Verification of Parallel Processes","first-page":"58","article-title":"\u201cComposition and Abstraction\u201d","volume":"2067","author":"Valmari","year":"2001"},{"key":"10.1016\/S1571-0661(04)80411-0_NEWBIB17","doi-asserted-by":"crossref","unstructured":"Valmari A.: \u201cOn-the-fly Verification with Stubborn Sets\u201d. Proc. ComputerAided Verification (CAV) '93, Lecture Notes in Computer Science 697, pp. 397\u2013408, Springer-Verlag 1993.","DOI":"10.1007\/3-540-56922-7_33"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804110?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804110?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:05:00Z","timestamp":1761609900000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104804110"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12]]},"references-count":17,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,12]]}},"alternative-id":["S1571066104804110"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80411-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Stuttering-Insensitive Automata for On-the-fly Detection of Livelock Properties","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80411-0","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}