{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:45Z","timestamp":1761611205914},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540436317"},{"type":"electronic","value":"9783540478133"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-47813-2_20","type":"book-chapter","created":{"date-parts":[[2007,5,30]],"date-time":"2007-05-30T22:35:31Z","timestamp":1180564531000},"page":"289-301","source":"Crossref","is-referenced-by-count":5,"title":["Approximating ATL* in ATL"],"prefix":"10.1007","author":[{"given":"Aidan","family":"Harding","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Ryan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Yves","family":"Schobbens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,4,10]]},"reference":[{"key":"20_CR1","unstructured":"R. Alur, T. A. Henzinger, S. C. Krishnan, et al. Mocha User Manual. Computer and Information Science Department, University of Pennsylvania and Electrical Engineering and Computer Sciences Department, University of California, Nov. 1999."},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science, pages 100\u2013109. IEEE Computer Society Press, 1997.","DOI":"10.1109\/SFCS.1997.646098"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"F. Cassez, M. D. Ryan, and P.-Y. Schobbens. Proving feature non-interaction with alternating-time temporal logic. In S. Gilmore and M. D. Ryan, editors, Language Constructs for Describing Features. Springer-Verlag, 2000.","DOI":"10.1007\/978-1-4471-0287-8_6"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. In Proceedings of the 21st International Conference on Software Engineering, May 1999.","DOI":"10.1145\/302405.302672"},{"issue":"1","key":"20_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E. A. Emerson","year":"1985","unstructured":"E. A. Emerson and J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences, 30(1):1\u201325, Feb. 1985.","journal-title":"Journal of Computer and System Sciences"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"L. Lamport. \u201cSometimes\u201d is sometimes \u201cnot never\u201d \u2014 on the temporal logic of programs. In Proc. 7th ACM Symposium on Principles of Programming Languages, pages 174\u2013185, Jan. 1980.","DOI":"10.1145\/567446.567463"},{"key":"20_CR7","unstructured":"L. Lamport. What good is temporal logic? In R. E. A. Mason, editor, Proceedings of the IFIP Congress on Information Processing, pages 657\u2013667. North-Holland, 1983."},{"key":"20_CR8","unstructured":"T. Laureys. From event based semantics to linear temporal logic. Master\u2019s thesis, School of Cognitive Science \u2014 University of Edinburgh, 2 Buccleuch Place, Edinburgh, UK, 1999."},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"F. Somenzi and R. Bloem. Efficient B\u00fcchi automata from LTL formulae. In Proceedings of 10th International Conference on Computer Aided Verification, pages 248\u2013263. Springer-Verlag, 2000.","DOI":"10.1007\/10722167_21"},{"key":"20_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/3-540-46691-6_9","volume-title":"Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"T. Wilke","year":"1999","unstructured":"T. Wilke. CTL+ is exponentially more succinct than CTL. In C. P. R. et al., editor, Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 1738 of Lecture Notes in Computer Science, pages 110\u2013121. Springer Verlag, 1999."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-47813-2_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T09:36:15Z","timestamp":1556444175000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47813-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540436317","9783540478133"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-47813-2_20","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}