{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T07:47:57Z","timestamp":1743148077187,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642198045"},{"type":"electronic","value":"9783642198052"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19805-2_12","type":"book-chapter","created":{"date-parts":[[2011,3,14]],"date-time":"2011-03-14T09:05:14Z","timestamp":1300093514000},"page":"168-183","source":"Crossref","is-referenced-by-count":2,"title":["Alternation Elimination for Automata over Nested Words"],"prefix":"10.1007","author":[{"given":"Christian","family":"Dax","sequence":"first","affiliation":[]},{"given":"Felix","family":"Klaedtke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"IEEE standard for property specification language (PSL). IEEE Std 1850TM (October 2005)"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Arenas, M., Barcel\u00f3, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. Log. Methods Comput. Sci. 4(4) (2008)","DOI":"10.2168\/LMCS-4(4:11)2008"},{"issue":"4","key":"12_CR3","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1145\/1075382.1075387","volume":"27","author":"R. Alur","year":"2005","unstructured":"Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis, M.: Analysis of recursive state machines. ACM Trans. Progr. Lang. Syst.\u00a027(4), 786\u2013818 (2005)","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-24730-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Alur","year":"2004","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 467\u2013481. Springer, Heidelberg (2004)"},{"key":"12_CR5","first-page":"202","volume-title":"ACM Symposium on Theory of Computing (STOC)","author":"R. Alur","year":"2004","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: ACM Symposium on Theory of Computing (STOC), pp. 202\u2013211. ACM Press, New York (2004)"},{"issue":"3","key":"12_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1516512.1516518","volume":"56","author":"R. Alur","year":"2009","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM\u00a056(3), 1\u201343 (2009)","journal-title":"J. ACM"},{"key":"12_CR7","unstructured":"Ball, T., Rajamani, S.K.: Boolean programs: A model and process for software analysis. Technical Report MSR-TR-2000-14, Microsoft Research (2000)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-51803-7_22","volume-title":"Temporal Logic in Specification","author":"B. Banieqbal","year":"1989","unstructured":"Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol.\u00a0398, pp. 62\u201374. Springer, Heidelberg (1989)"},{"key":"12_CR9","unstructured":"Ben-David, S., Bloem, R., Fisman, D., Griesmayer, A., Pill, I., Ruah, S.: Automata construction algorithms optimized for PSL. Technical report, The Prosyd Project (2005), \n                    \n                      http:\/\/www.prosyd.org"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-540-74407-8_32","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"L. Bozzelli","year":"2007","unstructured":"Bozzelli, L.: Alternating automata and a temporal fixpoint calculus for visibly pushdown languages. In: Caires, L., Li, L. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 476\u2013491. Springer, Heidelberg (2007)"},{"key":"12_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-89439-1_16","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Dax","year":"2008","unstructured":"Dax, C., Klaedtke, F.: Alternation elimination by complementation. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 214\u2013229. Springer, Heidelberg (2008)"},{"issue":"4","key":"12_CR12","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s00236-010-0118-3","volume":"47","author":"C. Dax","year":"2010","unstructured":"Dax, C., Klaedtke, F., Lange, M.: On regular temporal logics with past. Acta Inform.\u00a047(4), 251\u2013277 (2010)","journal-title":"Acta Inform."},{"issue":"3","key":"12_CR13","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log.\u00a02(3), 408\u2013429 (2001)","journal-title":"ACM Trans. Comput. Log."},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-540-31980-1_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: Complementation constructions for nondeterministic automata on infinite words. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 206\u2013221. Springer, Heidelberg (2005)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-540-74407-8_7","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"M. Lange","year":"2007","unstructured":"Lange, M.: Linear time logics around PSL: Complexity, expressiveness, and a little bit of succinctness. In: Caires, L., Li, L. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 90\u2013104. Springer, Heidelberg (2007)"},{"issue":"3","key":"12_CR16","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on \u03c9-words. Theoret. Comput. Sci.\u00a032(3), 321\u2013330 (1984)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"12_CR17","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/0304-3975(92)90076-R","volume":"97","author":"D. Muller","year":"1992","unstructured":"Muller, D., Saoudi, A., Schupp, P.: Alternating automata, the weak monadic theory of trees and its complexity. Theoret. Comput. Sci.\u00a097(2), 233\u2013244 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"2\u20133","key":"12_CR18","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D. Muller","year":"1987","unstructured":"Muller, D., Schupp, P.: Alternating automata on infinite trees. Theoret. Comput. Sci.\u00a054(2\u20133), 267\u2013276 (1987)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"12_CR19","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1147\/rd.32.0198","volume":"3","author":"J.C. Shepherdson","year":"1959","unstructured":"Shepherdson, J.C.: The reduction of two-way automata to one-way automata. IBM Journal of Research and Development\u00a03(2), 198\u2013200 (1959)","journal-title":"IBM Journal of Research and Development"},{"key":"12_CR20","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1145\/73560.73582","volume-title":"ACM Symposium on Principles of Programming Languages (POPL)","author":"M.Y. Vardi","year":"1988","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 250\u2013259. ACM Press, New York (1988)"},{"issue":"5","key":"12_CR21","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/0020-0190(89)90205-6","volume":"30","author":"M.Y. Vardi","year":"1989","unstructured":"Vardi, M.Y.: A note on the reduction of two-way automata to one-way automata. Inform. Process. Lett.\u00a030(5), 261\u2013264 (1989)","journal-title":"Inform. Process. Lett."},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"628","DOI":"10.1007\/BFb0055090","volume-title":"Automata, Languages and Programming","author":"M.Y. Vardi","year":"1998","unstructured":"Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 628\u2013641. Springer, Heidelberg (1998)"},{"key":"12_CR23","first-page":"332","volume-title":"Symposium on Logic in Computer Science (LICS)","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Symposium on Logic in Computer Science (LICS), pp. 332\u2013344. IEEE Computer Society, Los Alamitos (1986)"},{"issue":"1-2","key":"12_CR24","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Information and Control\u00a056(1-2), 72\u201399 (1983)","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19805-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,10,12]],"date-time":"2018-10-12T10:45:55Z","timestamp":1539341155000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19805-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198045","9783642198052"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19805-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}