{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T02:38:22Z","timestamp":1770431902526,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540654933","type":"print"},{"value":"9783540492139","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49213-5_2","type":"book-chapter","created":{"date-parts":[[2007,12,9]],"date-time":"2007-12-09T12:03:39Z","timestamp":1197201819000},"page":"23-60","source":"Crossref","is-referenced-by-count":46,"title":["Alternating-time Temporal Logic"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,5,21]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger. Reactive modules. In Proc. 11th IEEE Symposium on Logic in Computer Science, pages 207\u2013218, 1996.","DOI":"10.1109\/LICS.1996.561320"},{"issue":"1","key":"2_CR2","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73\u2013132, 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0035748","volume-title":"Proc. 16th Lnt. Colloquium on Automata, Languages, and Programming","author":"M. Abadi","year":"1989","unstructured":"M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable concurrent program specifications. In Proc. 16th Lnt. Colloquium on Automata, Languages, and Programming, volume 372 of Lecture Notes in Computer Science, Springer-Verlag, pages 1\u201317, 1989."},{"key":"2_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/3-540-58179-0_53","volume-title":"Proc. 6th Conference on Computer-aided Verification","author":"B.B.G.+.9.4._.I. Beer","year":"1994","unstructured":"[BBG+94]_I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In Proc. 6th Conference on Computer-aided Verification, volume 818 of Lecture Notes in Computer Science, Springer-Verlag, pages 182\u2013193, 1994."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"[BCM+90]_J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th Symposium on Logic in Computer Science, pages 428\u2013439, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"key":"2_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-58179-0_50","volume-title":"Proc. 6th Conference on Computer-aided Verification","author":"O. Bernholtz","year":"1994","unstructured":"O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In Proc. 6th Conference on Computer-aided Verification, volume 818 of Lecture Notes in Computer Science, Springer-Verlag, pages 142\u2013155, 1994."},{"key":"2_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proc. Workshop on Logic of Programs","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proc. Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science, Springer-Verlag, pages 52\u201371, 1981."},{"issue":"2","key":"2_CR8","doi-asserted-by":"publisher","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 Transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"2_CR9","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114\u2013133, 1981.","journal-title":"Journal of the ACM"},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland. A linear-time model-checking algorithm for the alternation-free modal \u03bc-calculus. Formal Methods in System Design, 2:121\u2013147, 1993.","journal-title":"Formal Methods in System Design"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"D.L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. MIT Press, 1989.","DOI":"10.7551\/mitpress\/6874.001.0001"},{"issue":"1","key":"2_CR12","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. Halpern. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM, 33(1):151\u2013178, 1986.","journal-title":"Journal of the ACM"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proc. 29th LEEE Symposium on Foundations of Computer Science, pages 368\u2013377, 1988.","DOI":"10.1109\/SFCS.1988.21949"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C.-L. Lei. Modalities for model checking: Branching time logic strikes back. In Proc. 20th ACM Symposium on Principles of Programming Languages, pages 84\u201396, 1985.","DOI":"10.1145\/318593.318620"},{"key":"2_CR15","unstructured":"E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional \u03bc-calculus. In Proc. 1st Symposium on Logic in Computer Science, pages 267\u2013278, 1986."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and A.P. Sistla. Deciding branching-time logic. In Proc. 16th ACM Symposium on Theory of Computing, 1984.","DOI":"10.1145\/800057.808661"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and Systems Sciences, 18:194\u2013211, 1979.","journal-title":"Journal of Computer and Systems Sciences"},{"key":"2_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-58201-0_66","volume-title":"Proc. 23rd Int. Colloquium on Automata, Languages, and Programming","author":"R. Gawlick","year":"1994","unstructured":"R. Gawlick, R. Segala, J. Sogaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. In Proc. 23rd Int. Colloquium on Automata, Languages, and Programming, volume 820 of Lecture Notes in Computer Science, Springer-Verlag, pages 166\u2013177, 1994."},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"issue":"5","key":"2_CR20","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"G.J. Holzmann. The model checker SPIN. LEEE Transactions on Software Engineering, 23(5):279\u2013295, 1997.","journal-title":"LEEE Transactions on Software Engineering"},{"issue":"3","key":"2_CR21","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1016\/0022-0000(81)90039-8","volume":"22","author":"N. Immerman","year":"1981","unstructured":"N. Immerman. Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences, 22(3):384\u2013406, 1981.","journal-title":"Journal of Computer and System Sciences"},{"key":"2_CR22","doi-asserted-by":"publisher","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 \u03bc-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"2_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/3-540-60218-6_31","volume-title":"Proc. 6th Conferance on Concurrency Theory","author":"O. Kupferman","year":"1995","unstructured":"O. Kupferman and M.Y. Vardi. On the complexity of branching modular model checking. In Proc. 6th Conferance on Concurrency Theory, volume 962 of Lecture Notes in Computer Science, Springer-Verlag, pages 408\u2013422, 1995."},{"key":"2_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-61474-5_59","volume-title":"Proc. 8th Conference on Computer-aided Verification","author":"O. Kupferman","year":"1996","unstructured":"O. Kupferman and M.Y. Vardi. Module checking. In Proc. 8th Conference on Computer-aided Verification, volume 1102 of Lecture Notes in Computer Science, Springer-Verlag, pages 75\u201386, 1996."},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite-state concurrent programs satisfy their linear specification. In Proc. 12th ACM Symposium on Principles of Programming Languages, pages 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"2_CR26","unstructured":"N.A. Lynch. Distributed Algorithms. Morgan-Kaufmann, 1996."},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"R. Parikh. Propositional game logic. In Proc. 24th LEEE Symposium on Foundation of Computer Science, pages 195\u2013200, 1983.","DOI":"10.1109\/SFCS.1983.47"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proc. 18th LEEE Symposium on Foundation of Computer Science, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"G.L. Peterson and J.H. Reif. Multiple-person alternation. In Proc. 20th LEEE Symposium on Foundation of Computer Science, pages 348\u2013363, 1979.","DOI":"10.1109\/SFCS.1979.25"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th ACM Symposium on Principles of Programming Languages, 1989.","DOI":"10.1145\/75277.75293"},{"key":"2_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/BFb0035790","volume-title":"Proc. 16th Lnt. Colloquium on Automata, Languages, and Programming","author":"A. Pnueli","year":"1989","unstructured":"A. Pnueli and R. Rosner. On the synthesis of an asynchronous reactive module. In Proc. 16th Lnt. Colloquium on Automata, Languages, and Programming, volume 372 of Lecture Notes in Computer Science, Springer-Verlag, pages 652\u2013671, 1989."},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"A. Pnueli and R. Rosner. Distributed reactive systems are hard to synthesize. In Proc. 31st LEEE Symposium on Foundation of Computer Science, pages 746\u2013757, 1990.","DOI":"10.1109\/FSCS.1990.89597"},{"key":"2_CR34","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Proc. 5th International Symposium on Programming","author":"J.P. Queille","year":"1981","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symposium on Programming, volume 137 of Lecture Notes in Computer Science, Springer-Verlag, pages 337\u2013351, 1981."},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"M.O. Rabin. Weakly definable relations and special automata. In Proc. Symposium on Mathematical Logic and Foundations of Set Theory, pages 1\u201323. North Holland, 1970.","DOI":"10.1016\/S0049-237X(08)71929-3"},{"key":"2_CR36","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1016\/0022-0000(84)90034-5","volume":"29","author":"J.H. Reif","year":"1984","unstructured":"J.H. Reif. The complexity of two-player games of incomplete information. Lournal on Computer and System Sciences, 29:274\u2013301, 1984.","journal-title":"Lournal on Computer and System Sciences"},{"key":"2_CR37","series-title":"PhD thesis","volume-title":"Modular Synthesis of Reactive Systems","author":"R. Rosner","year":"1992","unstructured":"R. Rosner. Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science, Rehovot, Israel, 1992."},{"key":"2_CR38","first-page":"81","volume":"77","author":"P.J.G. Ramadge","year":"1989","unstructured":"P.J.G. Ramadge and W.M. Wonham. The control of descrete event systems. LEEE Transactions on Control Theory, 77:81\u201398, 1989.","journal-title":"LEEE Transactions on Control Theory"},{"key":"2_CR39","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-60275-5","volume-title":"Proc. 12th Symposium on Theoretical Aspects of Computer Science","author":"W. Thomas","year":"1995","unstructured":"W. Thomas. On the synthesis of strategies in infinite games. In Proc. 12th Symposium on Theoretical Aspects of Computer Science, volume 900 of Lecture Notes in Computer Science, Springer-Verlag, pages 1\u201313, 1995."},{"key":"2_CR40","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st LEEE Symposium on Logic in Computer Science, pages 322\u2013331, 1986."},{"issue":"2","key":"2_CR41","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2):182\u2013221, 1986.","journal-title":"Journal of Computer and System Science"},{"key":"2_CR42","unstructured":"M. Yannakakis. Synchronous multi-player gaines with incomplete information are undecidable. Personal communication, 1997."}],"container-title":["Lecture Notes in Computer Science","Compositionality: The Significant Difference"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49213-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T13:14:21Z","timestamp":1737638061000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49213-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540654933","9783540492139"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/3-540-49213-5_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1998]]}}}