{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:10:34Z","timestamp":1771024234487,"version":"3.50.1"},"reference-count":35,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2016,12,1]],"date-time":"2016-12-01T00:00:00Z","timestamp":1480550400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2020,12,20]],"date-time":"2020-12-20T00:00:00Z","timestamp":1608422400000},"content-version":"vor","delay-in-days":1480,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2016,12]]},"DOI":"10.1016\/j.tcs.2016.08.012","type":"journal-article","created":{"date-parts":[[2016,8,26]],"date-time":"2016-08-26T01:12:11Z","timestamp":1472173931000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":9,"special_numbering":"PA","title":["Ordered multi-stack visibly pushdown automata"],"prefix":"10.1016","volume":"656","author":[{"given":"Dario","family":"Carotenuto","sequence":"first","affiliation":[]},{"given":"Aniello","family":"Murano","sequence":"additional","affiliation":[]},{"given":"Adriano","family":"Peron","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2016.08.012_br0050","series-title":"STOC'04","first-page":"202","article-title":"Visibly pushdown languages","author":"Alur","year":"2004"},{"key":"10.1016\/j.tcs.2016.08.012_br0040","first-page":"1","article-title":"Pushdown module checking with imperfect information","volume":"213","author":"Aminof","year":"2013","journal-title":"J. Inf. Comput. Sci."},{"key":"10.1016\/j.tcs.2016.08.012_br0060","series-title":"CONCUR'10","first-page":"117","article-title":"From multi to single stack automata","volume":"vol. 6269","author":"Atig","year":"2010"},{"issue":"3","key":"10.1016\/j.tcs.2016.08.012_br0070","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-8(3:20)2012","article-title":"Model-checking of ordered multi-pushdown automata","volume":"8","author":"Atig","year":"2012","journal-title":"Log. Methods Comput. Sci."},{"key":"10.1016\/j.tcs.2016.08.012_br0010","series-title":"DLT'08","first-page":"121","article-title":"Emptiness of multi-pushdown automata is 2ETIME-Complete","volume":"vol. 5257","author":"Atig","year":"2008"},{"issue":"8","key":"10.1016\/j.tcs.2016.08.012_br0030","doi-asserted-by":"crossref","first-page":"1083","DOI":"10.1142\/S0129054114400255","article-title":"Adjacent ordered multi-pushdown systems","volume":"25","author":"Atig","year":"2014","journal-title":"Internat. J. Found. Comput. Sci."},{"issue":"4:16","key":"10.1016\/j.tcs.2016.08.012_br0110","article-title":"On the expressive power of 2-stack visibly pushdown automata","volume":"4","author":"Bollig","year":"2008","journal-title":"Log. Methods Comput. Sci."},{"key":"10.1016\/j.tcs.2016.08.012_br0090","series-title":"CONCUR'97","first-page":"135","article-title":"Reachability analysis of pushdown automata: application to model-checking","volume":"vol. 1243","author":"Bouajjani","year":"1997"},{"issue":"2\u20133","key":"10.1016\/j.tcs.2016.08.012_br0100","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1016\/j.tcs.2008.06.012","article-title":"Verification of well-formed communicating recursive state machines","volume":"403","author":"Bozzelli","year":"2008","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"10.1016\/j.tcs.2016.08.012_br0190","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/s10703-010-0093-x","article-title":"Pushdown module checking","volume":"36","author":"Bozzelli","year":"2010","journal-title":"Form. Methods Syst. Des."},{"issue":"3","key":"10.1016\/j.tcs.2016.08.012_br0080","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1142\/S0129054196000191","article-title":"Multi-push-down languages and grammars","volume":"7","author":"Breveglieri","year":"1996","journal-title":"Internat. J. Found. Comput. Sci."},{"key":"10.1016\/j.tcs.2016.08.012_br0150","series-title":"DLT'07","first-page":"132","article-title":"2-Visibly pushdown automata","volume":"vol. 4588","author":"Carotenuto","year":"2007"},{"key":"10.1016\/j.tcs.2016.08.012_br0130","series-title":"LP'81","first-page":"52","article-title":"Design and verification of synchronization skeletons using branching time temporal logic","volume":"vol. 131","author":"Clarke","year":"1981"},{"key":"10.1016\/j.tcs.2016.08.012_br0140","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/j.tcs.2016.08.012_br0120","author":"Comon"},{"issue":"3","key":"10.1016\/j.tcs.2016.08.012_br0350","article-title":"Enriched \u03bc-Calculi Module Checking","volume":"4","author":"Ferrante","year":"2008","journal-title":"Log. Methods Comput. Sci."},{"issue":"3","key":"10.1016\/j.tcs.2016.08.012_br0020","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-8(3:23)2012","article-title":"Reachability analysis of communicating pushdown systems","volume":"8","author":"Heu\u00dfner","year":"2012","journal-title":"Log. Methods Comput. Sci."},{"key":"10.1016\/j.tcs.2016.08.012_br0160","series-title":"Introduction to Automata Theory, Languages, and Computation","author":"Hopcroft","year":"1979"},{"issue":"1","key":"10.1016\/j.tcs.2016.08.012_br0170","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/322047.322058","article-title":"Reversal-bounded multicounter machines and their decision problems","volume":"25","author":"Ibarra","year":"1978","journal-title":"J. ACM"},{"key":"10.1016\/j.tcs.2016.08.012_br0180","series-title":"LPAR'02","first-page":"262","article-title":"Pushdown specifications","volume":"vol. 2514","author":"Kupferman","year":"2002"},{"key":"10.1016\/j.tcs.2016.08.012_br0200","author":"La Torre"},{"key":"10.1016\/j.tcs.2016.08.012_br0210","series-title":"LICS'07","first-page":"161","article-title":"A robust class of context-sensitive languages","author":"La Torre","year":"2007"},{"key":"10.1016\/j.tcs.2016.08.012_br0220","series-title":"LATIN 2010: Theoretical Informatics, 9th Latin American Symposium","first-page":"96","article-title":"The language theory of bounded context-switching","volume":"vol. 6034","author":"La Torre","year":"2010"},{"key":"10.1016\/j.tcs.2016.08.012_br0230","series-title":"CONCUR'11","first-page":"203","article-title":"Reachability of multistack pushdown systems with scope-bounded matching relations","volume":"vol. 6901","author":"La Torre","year":"2011"},{"key":"10.1016\/j.tcs.2016.08.012_br0240","series-title":"DLT'14","first-page":"116","article-title":"Scope-bounded pushdown languages","volume":"vol. 8633","author":"La Torre","year":"2014"},{"key":"10.1016\/j.tcs.2016.08.012_br0250","series-title":"MFCS'14","first-page":"377","article-title":"A unifying approach for multistack pushdown automata","volume":"vol. 8634","author":"La Torre","year":"2014"},{"key":"10.1016\/j.tcs.2016.08.012_br0260","series-title":"Computation: Finite and Infinite Machines","author":"Minsky","year":"1967"},{"key":"10.1016\/j.tcs.2016.08.012_br0270","series-title":"IJCAI'15","first-page":"1090","article-title":"Pushdown multi-agent system verification","author":"Murano","year":"2015"},{"key":"10.1016\/j.tcs.2016.08.012_br0280","series-title":"Symposium on Programming'81","first-page":"337","article-title":"Specification and verification of concurrent programs in CESAR","volume":"vol. 137","author":"Queille","year":"1981"},{"issue":"1\u20132","key":"10.1016\/j.tcs.2016.08.012_br0290","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1016\/S0019-9958(84)80043-1","article-title":"Can message buffers be axiomatized in linear temporal logic","volume":"63","author":"Sistla","year":"1984","journal-title":"Inf. Control"},{"key":"10.1016\/j.tcs.2016.08.012_br0300","series-title":"Distributed Systems: Principles and Paradigms","author":"Van Steen","year":"2002"},{"key":"10.1016\/j.tcs.2016.08.012_br0310","series-title":"CONCUR'11","first-page":"434","article-title":"Efficient ctl model-checking for pushdown systems","volume":"vol. 6901","author":"Song","year":"2011"},{"key":"10.1016\/j.tcs.2016.08.012_br0320","series-title":"Languages, Automata and Logic, Handbook of Formal Languages, vol. 3","first-page":"389","author":"Thomas","year":"1997"},{"issue":"2","key":"10.1016\/j.tcs.2016.08.012_br0330","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/0022-0000(86)90026-7","article-title":"Automata-theoretic techniques for modal logics of programs","volume":"32","author":"Vardi","year":"1986","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/j.tcs.2016.08.012_br0340","series-title":"CAV'96","first-page":"62","article-title":"Pushdown processes: games and model checking","volume":"vol. 1102","author":"Walukiewicz","year":"1996"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397516304200?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397516304200?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,12,20]],"date-time":"2020-12-20T03:04:47Z","timestamp":1608433487000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397516304200"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12]]},"references-count":35,"alternative-id":["S0304397516304200"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2016.08.012","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2016,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Ordered multi-stack visibly pushdown automata","name":"articletitle","label":"Article Title"},{"value":"Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.tcs.2016.08.012","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2016 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}