{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T10:11:13Z","timestamp":1781086273848,"version":"3.54.1"},"reference-count":17,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1991,10,1]],"date-time":"1991-10-01T00:00:00Z","timestamp":686275200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":7960,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1991,10]]},"DOI":"10.1016\/0304-3975(90)90110-4","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T03:47:37Z","timestamp":1027655257000},"page":"161-177","source":"Crossref","is-referenced-by-count":141,"title":["Local model checking in the modal mu-calculus"],"prefix":"10.1016","volume":"89","author":[{"given":"Colin","family":"Stirling","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Walker","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(90)90110-4_BIB1","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1007\/BF00264284","article-title":"Tableau-based model checking in the propositional mu-calculus","volume":"27","author":"Cleaveland","year":"1990","journal-title":"Acta Inform."},{"key":"10.1016\/0304-3975(90)90110-4_BIB2","series-title":"Proc. IFIP","article-title":"The concurrency workbench","author":"Cleaveland","year":"1989"},{"key":"10.1016\/0304-3975(90)90110-4_BIB3","series-title":"Proc. Symp. on Logic in Computer Science","first-page":"267","article-title":"Efficient model checking in fragments of the propositional mu-calculus","author":"Emerson","year":"1986"},{"key":"10.1016\/0304-3975(90)90110-4_BIB4","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/S0019-9958(86)80031-6","article-title":"A modal characterization of observational congruence of finite terms of CCS","volume":"68","author":"Graf","year":"1986","journal-title":"Inform. and Control"},{"key":"10.1016\/0304-3975(90)90110-4_BIB5","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","article-title":"Algebraic laws for nondeterminism and concurrency","volume":"32","author":"Hennessy","year":"1985","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(90)90110-4_BIB6","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/BF01887208","article-title":"Hennessy-Milner logic with recursion as a specification language, and a refinement calculus based on it","volume":"1","author":"Holmstr\u00f6m","year":"1989","journal-title":"Formal Aspects Comput."},{"issue":"5","key":"10.1016\/0304-3975(90)90110-4_BIB7","doi-asserted-by":"crossref","DOI":"10.1145\/355592.365595","article-title":"Additional comments on a problem in concurrent programming control","volume":"9","author":"Knuth","year":"1966","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(90)90110-4_BIB8","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional mu-calculus","volume":"27","author":"Kozen","year":"1983","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(90)90110-4_BIB9","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","article-title":"Proof systems for satisfiability in Hennessy-Milner logic with recursion","volume":"72","author":"Larsen","year":"1990","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(90)90110-4_BIB10","series-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/0304-3975(90)90110-4_BIB11","series-title":"Information Processing '86","first-page":"54","article-title":"Specification and development of reactive systems","author":"Pnueli","year":"1986"},{"key":"10.1016\/0304-3975(90)90110-4_BIB12","series-title":"Proc. 22nd. FOCS","first-page":"421","article-title":"A decidable \u03bc-calculus","author":"Pratt","year":"1981"},{"key":"10.1016\/0304-3975(90)90110-4_BIB13","series-title":"Proc. ICALP","article-title":"Characteristic formulae","author":"Steffen","year":"1989"},{"key":"10.1016\/0304-3975(90)90110-4_BIB14","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/0304-3975(87)90012-0","article-title":"Modal logics for communicating systems","volume":"49","author":"Stirling","year":"1987","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(90)90110-4_BIB15","series-title":"Proc. of REX Workshop","article-title":"Temporal logics for CCS","author":"Stirling","year":"1988"},{"key":"10.1016\/0304-3975(90)90110-4_BIB16","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/BF01887209","article-title":"Automated analysis of mutual exclusion algorithms using CCS","volume":"1","author":"Walker","year":"1989","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/0304-3975(90)90110-4_BIB17","series-title":"Proc. ICALP","article-title":"Model checking the modal nu-calculus","author":"Winskel","year":"1989"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397590901104?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397590901104?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T03:55:37Z","timestamp":1555127737000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0304397590901104"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,10]]},"references-count":17,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1991,10]]}},"alternative-id":["0304397590901104"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(90)90110-4","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1991,10]]}}}