{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:00:22Z","timestamp":1754485222005},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600459"},{"type":"electronic","value":"9783540494133"}],"license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_49","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:36:08Z","timestamp":1330277768000},"page":"166-179","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Local liveness for compositional modeling of fair reactive systems"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"M. Abadi, L. Lamport. Composing specifications. ACM TOPLAS, 15(1):73\u2013132, 1993.","journal-title":"ACM TOPLAS"},{"key":"15_CR2","unstructured":"M. Abadi, L. Lamport. Conjoining Specifications. Technical Report 118, DEC-SRC, 1993."},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"M. Abadi, L. Lamport, P. Wolper. Realizable and unrealizable specifications of reactive systems. Automata, Languages, and Programming, LNCS 372, pp. 1\u201317. Springer, 1989.","DOI":"10.1007\/BFb0035748"},{"key":"15_CR4","unstructured":"R. Alur, T.A. Henzinger. Fair Reactive Systems. Technical Report, Computer Science Department, Cornell University, 1995."},{"issue":"4","key":"15_CR5","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/BF01872848","volume":"2","author":"K. Apt","year":"1988","unstructured":"K. Apt, N. Francez, S. Katz. Appraising fairness in languages for distributed programming. Distributed Computing, 2(4):226\u2013241, 1988.","journal-title":"Distributed Computing"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"D. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. MIT Press, 1989.","DOI":"10.7551\/mitpress\/6874.001.0001"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, C. Lei. Modalities for model checking: branching time strikes back. Symp. Principles of Programming Languages, pp. 84\u201395. ACM, 1985.","DOI":"10.1145\/318593.318620"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"R. Gawlick, R. Segala, J. Sogaard-Andersen, N. Lynch. Liveness in timed and untimed systems. Technical Report MIT\/LCS\/TR-587, MIT, 1993.","DOI":"10.1007\/3-540-58201-0_66"},{"issue":"3","key":"15_CR9","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg, D. Long. Model checking and modular verification. ACM TOPLAS, 16(3):843\u2013871, 1994.","journal-title":"ACM TOPLAS"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"R. Kurshan. Computer-aided Verification: The Automata-theoretic Approach. Princeton University Press, 1994.","DOI":"10.1007\/978-1-4615-3556-0"},{"key":"15_CR11","unstructured":"L. Lamport. The Temporal Logic of Actions. Technical Report 79, DEC-SRC, 1991."},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"H. Lescow. On polynomial-size programs winning finite-state games. Computer-aided Verification, LNCS. Springer, 1995.","DOI":"10.1007\/3-540-60045-0_54"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"N. Lynch, M. Tuttle. Hierarchical correctness proofs for distributed algorithms. Symp. Principles of Distributed Computing, pp. 137\u2013151. ACM, 1987.","DOI":"10.1145\/41840.41852"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"issue":"4","key":"15_CR15","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J. Misra","year":"1981","unstructured":"J. Misra, K. Chandy. Proofs of networks of processes. IEEE Trans. Software Engineering, 7(4):417\u2013426, 1981.","journal-title":"IEEE Trans. Software Engineering"},{"issue":"1","key":"15_CR16","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/BF02311231","volume":"5","author":"P. Pandya","year":"1991","unstructured":"P. Pandya, M. Joseph. P-A logic\u2014a compositional proof system for distributed programs. Distributed Computing, 5(1):37\u201354, 1991.","journal-title":"Distributed Computing"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs. Logics and Models of Concurrent Systems. pp. 123\u2013144. Springer, 1984.","DOI":"10.1007\/978-3-642-82453-1_5"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_49","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:19:57Z","timestamp":1558268397000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_49","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}