{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T20:12:55Z","timestamp":1729627975466,"version":"3.28.0"},"reference-count":48,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/lics.2003.1210078","type":"proceedings-article","created":{"date-parts":[[2003,12,22]],"date-time":"2003-12-22T12:34:10Z","timestamp":1072096450000},"page":"381-390","source":"Crossref","is-referenced-by-count":0,"title":["Micro-macro stack systems: a new frontier of elementary decidability for sequential systems"],"prefix":"10.1109","author":[{"given":"N.","family":"Piterman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-53832-1_51"},{"journal-title":"Computer Aided Verification of Coordinating Processes","year":"1994","author":"kurshan","key":"35"},{"key":"18","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","volume":"131","author":"clarke","year":"1981","journal-title":"LNCS"},{"key":"36","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318622"},{"key":"15","article-title":"On infinite transition graphs having a decidable monadic theory","volume":"1099","author":"caucal","year":"1996","journal-title":"LNCS"},{"key":"33","first-page":"36","article-title":"An automata-theoretic approach to reasoning about infinite-state systems","volume":"1855","author":"kupferman","year":"2000","journal-title":"LNCS"},{"key":"16","first-page":"165","article-title":"On infinite terms having a decidable monadic theory","volume":"2420","author":"caucal","year":"2002","journal-title":"LNCS"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"13","doi-asserted-by":"crossref","DOI":"10.1016\/S0304-3975(99)00034-1","article-title":"Model checking the full modal ?-calculus for infinite sequential processes","volume":"221","author":"burkart","year":"1999","journal-title":"TCS"},{"key":"39","article-title":"Specification and verification of concurrent systems in Cesar","volume":"137","author":"queille","year":"1981","journal-title":"LNCS"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80534-6"},{"key":"11","article-title":"Model checking of infinite graphs defined by graph grammers","author":"burkart","year":"1996","journal-title":"1st Infinity"},{"key":"37","first-page":"252","article-title":"On rational graphs","volume":"1784","author":"morvan","year":"2000","journal-title":"LNCS"},{"key":"12","first-page":"89","article-title":"Composition, decomposition and model checking of pushdown processes","volume":"2","author":"burkart","year":"1995","journal-title":"Nordic J Comut"},{"key":"38","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90087-8"},{"key":"21","article-title":"Benefits of bounded model checking at an industrial setting","volume":"2102","author":"copty","year":"2001","journal-title":"LNCS"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"20"},{"key":"43","first-page":"628","article-title":"Reasoning about the past with two-way automata","volume":"1443","author":"vardi","year":"1998","journal-title":"LNCS"},{"key":"42","first-page":"130","article-title":"A short introduction to infinite automata","volume":"2295","author":"thomas","year":"2001","journal-title":"LNCS"},{"key":"41","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"journal-title":"Decidability of Bisimulation Equivalence for Pushdown Processes","year":"2000","author":"stirgling","key":"40"},{"key":"48","first-page":"110","article-title":"CTL+ is exponentially more succinct than CTL","volume":"1738","author":"wilke","year":"1999","journal-title":"LNCS"},{"key":"45","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"44","first-page":"332","article-title":"An automata-theoretic approach to automatic program verification","author":"vardi","year":"1986","journal-title":"9th LICS"},{"key":"47","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00185-2"},{"key":"46","first-page":"62","article-title":"Pushdown processes: Games and model checking","volume":"1102","author":"walukiewicz","year":"1996","journal-title":"LNCS"},{"key":"22","first-page":"281","article-title":"Timed alternating tree automata: The automata-theoretic solution to the TCTL model checking problem","volume":"1644","author":"dickhfer","year":"1999","journal-title":"LNCS"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1991.185392"},{"key":"24","article-title":"A direct symbolic approach to model checking pushdown automata","author":"finkel","year":"1997","journal-title":"1st Infinity"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1145\/321386.321403"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1145\/321371.321385"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1073"},{"journal-title":"Introduction to Automata Theory Languages and Computation","year":"1979","author":"hopcroft","key":"28"},{"key":"29","article-title":"Automata for the modal ?-calculus and related results","author":"janin","year":"1995","journal-title":"20th MFCS"},{"key":"3","article-title":"Prefix-recognisable graphs and monadic second-order logic","author":"blumensath","year":"2001","journal-title":"Tech Report"},{"key":"2","first-page":"454","article-title":"Finding bugs in an alpha microprocessors using satisfiability solvers","volume":"2102","author":"biesse","year":"2001","journal-title":"LNCS"},{"key":"10","article-title":"More infinite results","volume":"6","author":"burkart","year":"1996","journal-title":"ENTCS"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055804"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-69678-4"},{"key":"30","first-page":"205","article-title":"Higher-order pushdown trees are easy","volume":"2303","author":"knapik","year":"2003","journal-title":"LNCS"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19600060105"},{"key":"5","first-page":"1","article-title":"On a decision method in restricted second order arithmetic","author":"bu?chi","year":"1962","journal-title":"Proc Internat Congr Logic Method and Philos Sci 1960"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36078-6_18"},{"key":"4","first-page":"135","article-title":"Reachability analysis of pushdown automata: Application to model-checking","volume":"1243","author":"bouajjani","year":"1997","journal-title":"LNCS"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_31"},{"journal-title":"Verification on Infinite Structures","year":"2000","author":"burkart","key":"9"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80424-4"}],"event":{"name":"18th Annual IEEE Symposium on Logic in Computer Science","acronym":"LICS-03","location":"Ottawa, Ont., Canada"},"container-title":["18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8592\/27231\/01210078.pdf?arnumber=1210078","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,15]],"date-time":"2017-06-15T22:58:19Z","timestamp":1497567499000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1210078\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":48,"URL":"https:\/\/doi.org\/10.1109\/lics.2003.1210078","relation":{},"subject":[]}}