{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,26]],"date-time":"2026-06-26T14:41:51Z","timestamp":1782484911319,"version":"3.54.5"},"publisher-location":"Berlin\/Heidelberg","reference-count":18,"publisher":"Springer-Verlag","isbn-type":[{"value":"354011212X","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0025774","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T10:23:41Z","timestamp":1132395821000},"page":"52-71","source":"Crossref","is-referenced-by-count":1037,"title":["Design and synthesis of synchronization skeletons using branching time temporal logic"],"prefix":"10.1007","author":[{"given":"Edmund M.","family":"Clarke","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"E. Allen","family":"Emerson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Ben-Ari, M., personal communication, 1981."},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Ben-Ari, M., Halpern, J., and Pnueli, A., Finite Models for Deterministic Propositional Logic. Proceedings 8th Int. Colloquium on Automata, Languages, and Programming, to appear, 1981.","DOI":"10.1007\/3-540-10843-2_21"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Ben-Ari, M., Manna, Z., and Pnueli, A., The Temporal Logic of Branching Time. 8th Annual ACM Symp. on Principles of Programming Languages, 1981.","DOI":"10.1145\/567532.567551"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Program Invariants as Fixpoints. 18th Annual Symp. on Foundations of Computer Science, 1977.","DOI":"10.1109\/SFCS.1977.25"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., and Clarke, E.M., Characterizing Correctness Properties of Parallel Programs as Fixpoints. Proceedings 7th Int. Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science #85, Springer-Verlag, 1981.","DOI":"10.1007\/3-540-10003-2_69"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., and Halpern, J., A New Decision Procedure for the Temporal Logic of Branching Time, unpublished manuscript, Harvard Univ., 1981.","DOI":"10.1145\/800070.802190"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Flon, L., and Suzuki, N., The Total Correctness of Parallel Programs. SIAM J. Comp., to appear, 1981.","DOI":"10.1137\/0210016"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., et al., The Temporal Analysis of Fairness. 7th Annual ACM Symp. on Principles of Programming Languages, 1980.","DOI":"10.1145\/567446.567462"},{"key":"5_CR9","volume-title":"An Introduction to Modal Logic","author":"G. Hughes","year":"1968","unstructured":"Hughes, G., and Cresswell, M., An Introduction to Modal Logic. Methuen, London, 1968."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Lamport, L., \"Sometime\" is Sometimes \"Not Never.\" 7th Annual ACM Symp. on Principles of Prgramming Languages, 1980.","DOI":"10.1145\/567446.567463"},{"key":"5_CR11","unstructured":"Laventhal, M., Synthesis of Synchronization Code for Data Abstractions, Ph.D. Thesis, M.I.T., June 1978."},{"key":"5_CR12","unstructured":"Park, D., Fixpoint Induction and Proofs of Program Properties, in Machine Intelligence 5 (D. Mitchie, ed.), Edinburgh University Press, 1970."},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Pratt, V., A Practical Decision Method for Propositional Dynamic Logic. 10th ACM Symp. on Theory of Computing, 1977.","DOI":"10.1145\/800133.804362"},{"key":"5_CR14","unstructured":"Ramamritham, K., and Keller, R., Specification and Synthesis of Synchronizers. 9th International Conference on Parallel Processing, 1980."},{"key":"5_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First Order Logic","author":"R.M. Smullyan","year":"1968","unstructured":"Smullyan, R.M., First Order Logic. Springer-Verlag, Berlin, 1968."},{"key":"5_CR16","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A., A Lattice-Theoretical Fixpoint Theorem and Its Applications. Pacific J. Math., 5, pp. 285\u2013309 (1955).","journal-title":"Pacific J. Math."},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. Tarjan","year":"1972","unstructured":"Tarjan, R., Depth First Search and Linear Graph Algorithms. SIAM J. Comp. 1:2, pp. 146\u2013160, 1972.","journal-title":"SIAM J. Comp."},{"key":"5_CR18","unstructured":"Wolper, P. Synthesis of Communicating Processes From Temporal Logic Specifications, unpublished manuscript, Stanford Univ., 1981."}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0025774.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T14:08:07Z","timestamp":1683295687000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0025774"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354011212X"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0025774","relation":{},"subject":[]}}