{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:15:47Z","timestamp":1784232947822,"version":"3.55.0"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,3,11]],"date-time":"2017-03-11T00:00:00Z","timestamp":1489190400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Spanish MINECO","award":["TIN2012-39391-C04-01 STRONGSOFT"],"award-info":[{"award-number":["TIN2012-39391-C04-01 STRONGSOFT"]}]},{"name":"Spanish MINECO","award":["TIN2012-38137-C02 VIVAC"],"award-info":[{"award-number":["TIN2012-38137-C02 VIVAC"]}]},{"name":"EU COST","award":["IC1402 ArVi"],"award-info":[{"award-number":["IC1402 ArVi"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,2]]},"DOI":"10.1007\/s10817-017-9410-z","type":"journal-article","created":{"date-parts":[[2017,3,11]],"date-time":"2017-03-11T10:02:19Z","timestamp":1489226539000},"page":"177-220","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Visibly Linear Temporal Logic"],"prefix":"10.1007","volume":"60","author":[{"given":"Laura","family":"Bozzelli","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3927-4773","authenticated-orcid":false,"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,3,11]]},"reference":[{"key":"9410_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R.: Marrying words and trees. In: Proceedings of 26th PODS, pp. 233\u2013242. ACM (2007)","DOI":"10.1145\/1265530.1265564"},{"key":"9410_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. In: Proceedings of 22nd LICS, pp. 151\u2013160. IEEE Computer Society (2007)","DOI":"10.1109\/LICS.2007.19"},{"key":"9410_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Proceedings of 10th TACAS. LNCS, vol. 2988, pp. 467\u2013481. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24730-2_35"},{"key":"9410_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of 36th STOC, pp. 202\u2013211. ACM (2004)","DOI":"10.1145\/1007352.1007390"},{"issue":"3","key":"9410_CR5","doi-asserted-by":"crossref","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 56(3), 1\u201343 (2009)","journal-title":"J. ACM"},{"key":"9410_CR6","doi-asserted-by":"crossref","unstructured":"Arenas, M., Barcel\u00f3, P., Libkin, L.: Regular languages of nested words: fixed points, automata, and synchronization. In: Proceedings of 34th ICALP. LNCS, vol. 4596, pp. 888\u2013900. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73420-8_76"},{"key":"9410_CR7","doi-asserted-by":"crossref","unstructured":"Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y.: The ForSpec temporal logic: a new temporal property-specification language. In: Proceedings of TACAS. LNCS, vol. 2280, pp. 296\u2013211. Springer, Berlin (2002)","DOI":"10.1007\/3-540-46002-0_21"},{"key":"9410_CR8","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Bebop: a symbolic model checker for boolean programs. In: Proceedings of 7th SPIN. LNCS, vol. 1885, pp. 113\u2013130. Springer, Berlin (2000)","DOI":"10.1007\/10722468_7"},{"key":"9410_CR9","doi-asserted-by":"crossref","unstructured":"Bollig, B., Cyriac, A., Gastin, P., Zeitoun, M.: Temporal logics for concurrent recursive programs: satisfiability and model checking. In: Proceedings 36th MFCS. LNCS, vol. 6907, pp. 132\u2013144. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22993-0_15"},{"key":"9410_CR10","doi-asserted-by":"crossref","unstructured":"Bozzelli, L.: Alternating automata and a temporal fixpoint calculus for visibly pushdown languages. In: Proceedings of 18th CONCUR. LNCS, vol. 4703, pp. 476\u2013491. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-74407-8_32"},{"key":"9410_CR11","unstructured":"Bozzelli, L., S\u00e1nchez, C.: Visibly rational expressions. In: Proceedings of FSTTCS, LIPIcs 18, pp. 211\u2013223 (2012)"},{"issue":"1","key":"9410_CR12","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/s00236-013-0190-6","volume":"51","author":"L Bozzelli","year":"2014","unstructured":"Bozzelli, L., S\u00e1nchez, C.: Visibly rational expressions. Acta Inf. 51(1), 25\u201349 (2014)","journal-title":"Acta Inf."},{"key":"9410_CR13","doi-asserted-by":"crossref","unstructured":"Dax, C., Klaedtke, F.: Alternation elimination for automata over nested words. In: Proceedings of 14th FOSSACS. LNCS, vol. 6604, pp. 168\u2013183. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-19805-2_12"},{"key":"9410_CR14","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/s00236-010-0118-3","volume":"47","author":"C Dax","year":"2010","unstructured":"Dax, C., Klaetke, F., Lange, M.: On regular temporal logic with past. Acta Inf. 47, 251\u2013277 (2010)","journal-title":"Acta Inf."},{"issue":"2","key":"9410_CR15","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1\u20133","key":"9410_CR16","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"JG Henriksen","year":"1999","unstructured":"Henriksen, J.G., Thiagarajan, P.S.: Dynamic linear time temporal logic. Ann. Pure Appl. Log. 96(1\u20133), 187\u2013207 (1999)","journal-title":"Ann. Pure Appl. Log."},{"key":"9410_CR17","unstructured":"IEEE Standard for Property Specification Language (PSL): IEEE Standard 1850\u20132010, (2010)"},{"key":"9410_CR18","doi-asserted-by":"crossref","unstructured":"Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C. E., McCarthy, J. (eds.) Automata Studies, vol. 34, pp. 3\u201341. Princeton University Press, Princeton (1956)","DOI":"10.1515\/9781400882618-002"},{"issue":"3","key":"9410_CR19","doi-asserted-by":"crossref","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. 2(3), 408\u2013429 (2001)","journal-title":"ACM Trans. Comput. Log."},{"issue":"2","key":"9410_CR20","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"9410_CR21","doi-asserted-by":"crossref","unstructured":"Leucker, M., S\u00e1nchez, C.: Regular linear temporal logic. In: Proceedings of 4th ICTAC. LNCS, vol. 4711, pp. 291\u2013305. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-75292-9_20"},{"key":"9410_CR22","doi-asserted-by":"crossref","unstructured":"L\u00f6ding, C., Serre, O.: Propositional dynamic logic with recursive programs. In: Proceedings of 9th FoSSaCS. LNCS, vol. 3921, pp. 292\u2013306. Springer, Berlin (2006)","DOI":"10.1007\/11690634_20"},{"key":"9410_CR23","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Viswanathan, M.: Query automata for XML nested words. In: Proceedings of 34th MFCS. LNCS, vol. 5734, pp. 561\u2013573. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03816-7_48"},{"key":"9410_CR24","doi-asserted-by":"crossref","unstructured":"Mehlhorn, K.: Pebbling moutain ranges and its application of dcfl-recognition. In: Proceedings of 7th ICALP. LNCS, vol. 85, pp. 422\u2013435. Springer, Berlin (1980)","DOI":"10.1007\/3-540-10003-2_89"},{"key":"9410_CR25","doi-asserted-by":"crossref","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 $$\\omega $$ \u03c9 -words. Theor. Comput. Sci. 32, 321\u2013330 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"9410_CR26","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 54, 267\u2013276 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"9410_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th FOCS, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"9410_CR28","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez, C., Leucker, M.: Regular linear temporal logic with past. In: Proceedings of 11th VMCAI. LNCS, vol. 5944, pp. 295\u2013311. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-11319-2_22"},{"key":"9410_CR29","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez, C., Samborski-Forlese, J.: Efficient regular linear temporal logic using dualization and stratification. In: Proceedings of 19th TIME, pp. 13\u201320 (2012)","DOI":"10.1109\/TIME.2012.25"},{"key":"9410_CR30","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: preliminary report. In: Proceedings of 5th STOC, pp. 1\u20139. ACM (1973)","DOI":"10.1145\/800125.804029"},{"key":"9410_CR31","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115, 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"9410_CR32","unstructured":"Weinert, A., Zimmermann, M.: Visibly linear dynamic logic. In: Proceedings of 36th FSTTCS, LIPIcs (2016) (To appear)"},{"key":"9410_CR33","doi-asserted-by":"crossref","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. Inf. Control 56, 72\u201399 (1983)","journal-title":"Inf. Control"},{"issue":"1\u20132","key":"9410_CR34","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1\u20132), 135\u2013183 (1998)","journal-title":"Theor. Comput. Sci."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9410-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9410-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9410-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,19]],"date-time":"2019-09-19T12:47:45Z","timestamp":1568897265000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9410-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,11]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,2]]}},"alternative-id":["9410"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9410-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,11]]}}}