{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:34:25Z","timestamp":1784241265460,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540572084","type":"print"},{"value":"9783540479680","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-57208-2_31","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:18:46Z","timestamp":1330258726000},"page":"447-461","source":"Crossref","is-referenced-by-count":24,"title":["A linear local model checking algorithm for CTL"],"prefix":"10.1007","author":[{"given":"Bart","family":"Vergauwen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Johan","family":"Lewi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,5,27]]},"reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"Andersen, H. R.: Model Checking and Boolean Graphs, ESOP'92, LNCS 582, 1992","DOI":"10.1007\/3-540-55253-7_1"},{"key":"31_CR2","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0020-0190(88)90029-4","volume":"29","author":"A. Arnold","year":"1988","unstructured":"Arnold, A., Crubille, P.: A linear algorithm to solve fixed-points equations on transition systems, Information Processing Letters, vol. 29, 57\u201366, 1988","journal-title":"Information Processing Letters"},{"issue":"No.12","key":"31_CR3","doi-asserted-by":"crossref","first-page":"1035","DOI":"10.1109\/TC.1986.1676711","volume":"C-35","author":"M. C. Brown","year":"1986","unstructured":"Brown, M.C., Clarke, E.M., Dill, D.L., Mishra, B.: Automatic verification of sequential circuits using temporal logic, IEEE Transactions on Computers, C-35, No. 12, pp. 1035\u20131044, 1986","journal-title":"IEEE Transactions on Computers"},{"key":"31_CR4","volume-title":"NATO ASI Series, Vol. F13, Logics and Models of Concurrent Systems","author":"E. M. Clarke","year":"1985","unstructured":"Clarke, E.M., Browne, M.C., Emerson, E.A., Sistla, A.P.: Using Temporal Logic for Automatic Verification of Finite State Systems, in NATO ASI Series, Vol. F13, Logics and Models of Concurrent Systems, ed. K.R.Apt, Springer-Verlag Berlin Heidelberg, 1985"},{"issue":"No.2","key":"31_CR5","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finitestate concurrent systems using temporal logic specifications, ACM Transactions on Progr. Languages and Systems, Vol. 8, No. 2, pp. 244\u2013263, April 1986","journal-title":"ACM Transactions on Progr. Languages and Systems"},{"key":"31_CR6","doi-asserted-by":"crossref","unstructured":"Cleaveland, R.: Tableau-Based Model hecking in the Propositional Mu-Calculus, Acta Informatica, 1990","DOI":"10.1007\/BF00264284"},{"key":"31_CR7","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/3-540-54233-7_129","volume-title":"Automata, Languages and Programming","author":"Rance Cleaveland","year":"1991","unstructured":"Cleaveland, R., Steffen, B.: Computing Behavioural Relations, Logically, ICALP 91, pp. 127\u2013138, LNCS 510"},{"key":"31_CR8","unstructured":"Cleaveland, R., Lein, M., Steffen, B.: Faster Model Checking for the Modal Mu-Calculus, CAV'92, Forthcoming"},{"key":"31_CR9","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/0304-3975(86)90034-4","volume":"46","author":"A. Dicky","year":"1986","unstructured":"Dicky, A.: An algebraic and algorithmic method of analysing transition systems, TCS, 46, 285\u2013303, 1986","journal-title":"TCS"},{"key":"31_CR10","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional \u03bc-calculus, LICS, 267\u2013278, 1986"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Results on the propositional mu-calculus, TCS 17, 1983","DOI":"10.7146\/dpb.v11i146.7420"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Larsen, K.G.: Proof systems for Hennessy-Milner logic with recursion, CAAP, 1988","DOI":"10.1007\/BFb0026106"},{"key":"31_CR13","unstructured":"Larsen, K.G.: Efficient local correctness checking, CAV'92, Forthcoming"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification, (Proc.) 12th ACM annual Symposium on Principles of Programming Languages, pp. 97\u2013107, 1985","DOI":"10.1145\/318593.318622"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"Stirling, C., Walker, D.: Local model checking in the modal mu-calculus, TCS, October 1991, see also LNCS 351, 369\u2013383, CAAP 1989","DOI":"10.1007\/3-540-50939-9_144"},{"key":"31_CR16","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/3-540-55251-0_18","volume-title":"CAAP '92","author":"Bart Vergauwen","year":"1992","unstructured":"Vergauwen, B., Lewi, J.: A linear algorithm for solving fixed points equations on transition systems, CAAP'92, LNCS 581, 322\u2013341"},{"issue":"1","key":"31_CR17","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/0304-3975(91)90043-2","volume":"83","author":"Glynn Winskel","year":"1991","unstructured":"Winskel, G.: A note on model checking the modal \u03bd-calculus, ICALP, LNCS 372, 1989, see also TCS 83, 1991","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","CONCUR'93"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57208-2_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:09:19Z","timestamp":1605647359000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57208-2_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540572084","9783540479680"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-57208-2_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}