{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:56Z","timestamp":1761611156891,"version":"3.32.0"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1993,4,1]],"date-time":"1993-04-01T00:00:00Z","timestamp":733622400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1993,4]]},"DOI":"10.1007\/bf01383878","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T03:29:35Z","timestamp":1112412575000},"page":"121-147","source":"Crossref","is-referenced-by-count":103,"title":["A linear-time model-checking algorithm for the alternation-free modal mu-calculus"],"prefix":"10.1007","volume":"2","author":[{"given":"Rance","family":"Cleaveland","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"CR1","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications.ACM TOPLAS, 8(2):244?263 (1986).","journal-title":"ACM TOPLAS"},{"key":"CR2","unstructured":"J.-C. Fernandez.Ald\u00e9baran: Une Syst\u00e8me de V\u00e9rification par R\u00e9duction de Processus Communicants. Ph.D. Thesis, Universit\u00e9 de Grenoble, (1988)."},{"key":"CR3","unstructured":"J. Malhotra, S.A. Smolka, A. Giacalone, and R. Shapiro. Winston: A tool for hierarchical design and simulation of concurrent systems.Proceedings of the Workshop on Specification and Verification of Concurrent Systems, University of Stirling, Scotland, pp. 140?152 (1988)."},{"key":"CR4","unstructured":"J. Richier, C. Rodriguez, J. Sifakis, and J. Voiron. Verification in Xesar of the sliding window protocol. InProceedings 7th Symp. on Protocol Specification, Testing, and Verification, Zurich, pp. 235?250 (1987)."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"V. Roy and R. de Simone. Auto\/Autograph. InComputer-Aided Verification '90, Piscataway, NJ, pp. 477?491 (1990).","DOI":"10.1090\/dimacs\/003\/29"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"R. Cleaveland and B. Steffen. When is ?partial? complete? A logic-based proof technique using partial specifications.Proceedings of the Fifth Symposium on Logic in Computer Science, Philadelphia, PA, pp. 440?449 (1990).","DOI":"10.1109\/LICS.1990.113768"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"S. Graf and B. Steffen. Using interface specifications for compositional reduction.Computer-Aided Verification '90, pp. 57?76 (1990).","DOI":"10.1090\/dimacs\/003\/06"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench.Proceedings Workshop on Automatic Verification Methods for Finite-State Systems, Lecture Notes in Computer Science, 407:24?37 (1989). Also to appear inACM TOPLAS.","DOI":"10.1007\/3-540-52148-8_3"},{"key":"CR9","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. A semantics-based verification tool for finite-state systems.Proceedings of the 9th Symposium on Protocol Specification, Testing, and Verification, Enschede, Holland, pp. 287?302 (1989)."},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"R. Cleaveland and B. Steffen. ?Computing Behavioural Relations, Logically.? InProceedings of the Eighteenth International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, 510:127?138 (1991).","DOI":"10.1007\/3-540-54233-7_129"},{"key":"CR11","unstructured":"B.U. Steffen and A. Ing\u00f3lfsd\u00f3ttir. Characteristic formulae for CCS with divergence. To appear inInformation and Computation."},{"key":"CR12","unstructured":"E.A. Emerson, and C.-L. Lei, Efficient model checking in fragments of the propositional mucalculus.Proceedings of the First Symposium on Logic in Computer Science, Cambridge, MA, pp. 267?278 (1986)."},{"key":"CR13","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. Fischer","year":"1979","unstructured":"M. Fischer and R. Ladner. Propositional dynamic logic of regular programs.Journal of Computer and System Sciences, 18:194?211 (1979).","journal-title":"Journal of Computer and System Sciences"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional ?-calculus.Theoretical Computer Science, 27:333?354 (1983).","journal-title":"Theoretical Computer Science"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"K. Larsen. Proof systems for Hennessy-Milner logic with recursion.Proceedings of Colloque sur Alg\u00e8bre et Arbres en Programmation, Nancy, France, pp. 215?230 (1988).","DOI":"10.1007\/BFb0026106"},{"issue":"2","key":"CR16","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"25","author":"A. Tarski","year":"1955","unstructured":"A. Tarski. A lattice-theoretical fixpoint theorem and its applications.Pacific Journal of Mathematics 25(2):285?309 (1955).","journal-title":"Pacific Journal of Mathematics"},{"key":"CR17","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0020-0190(88)90029-4","volume":"29","author":"A. Arnold","year":"1988","unstructured":"A. Arnold and P. Crubille. A linear algorithm to solve fixed-point equations on transition systems.Information Processing Letters, 29:57?66 (September 1988).","journal-title":"Information Processing Letters"},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"D. Walker. Bisimulations and divergence.Proceedings of the Third Symposium on Logic in Computer Science, Edinburgh, Scotland, pp. 186?192 (1988).","DOI":"10.1109\/LICS.1988.5117"},{"key":"CR19","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/3-540-52148-8_2","volume":"407","author":"R. Cleaveland","year":"1989","unstructured":"R. Cleaveland and M.C.B. Hennessy. Testing equivalence as a bisimulation equivalence.Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, Lecture Notes in Computer Science, 407:11?23 (1989). Also to appear inFundamental Aspects of Computing.","journal-title":"Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, Lecture Notes in Computer Science"},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"B.U. Steffen. Characteristic formulae. InProceedings of the Sixteenth International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, 372:723?733 (1989).","DOI":"10.1007\/BFb0035794"},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, M. Dreim\u00fcller, and B. Steffen. Faster model-checking for the modal mu-calculus. To appear inProceedings of the 1992 Workshop on Computer-Aided Verification. Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-56496-9_32"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"H. Andersen. Model checking and Boolean graphs.Proceedings of ESOP '92, Rennes, France, pp. 1?19, Springer-Verlag (1992).","DOI":"10.1007\/3-540-55253-7_1"},{"key":"CR23","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"R. Cleaveland. Tableau-based model-checking in the propositional mu-calculus.Acta Information, 27:725?747 (1990).","journal-title":"Acta Information"},{"key":"CR24","doi-asserted-by":"crossref","unstructured":"C. Stirling and D. Walker. Local model checking in the modal mu-calculus. InProceedings of TAPSOFT '89, Lecture Notes in Computer Science, 351:369?383 (1989).","DOI":"10.1007\/3-540-50939-9_144"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"G. Winskel. ?Model checking in the modalv-calculus.? InProceedings of the Sixteenth International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, 372:761?772 (1989).","DOI":"10.1007\/BFb0035797"},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"K. Larsen. Efficient local correctness checking. To appear inProceedings of the 1992 Workshop on Computer-Aided Verification.","DOI":"10.1007\/3-540-55179-4"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383878.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01383878\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383878","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T03:27:07Z","timestamp":1735529227000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01383878"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,4]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993,4]]}},"alternative-id":["BF01383878"],"URL":"https:\/\/doi.org\/10.1007\/bf01383878","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1993,4]]}}}