Model-checking hierarchical structures

Alur, 2005, Analysis of recursive state machines, ACM Trans. Programm. Lang. Syst. (TOPLAS), 27, 786, 10.1145/1075382.1075387 Alur, 2001, Model checking of hierarchical state machines, ACM Trans. Programm. Lang. Syst. (TOPLAS), 23, 273, 10.1145/503502.503503 Àlvarez, 1993, A very hard log-space counting class, Theoret. Comput. Sci., 107, 3, 10.1016/0304-3975(93)90252-O Babai, 1991, Non-deterministic exponential time has two-prover interactive protocols, Comput. Complexity, 1, 3, 10.1007/BF01200056 Barrington, 1990, On uniformity within NC1, J. Comput. System Sci., 41, 274, 10.1016/0022-0000(90)90022-D Borchert, 1996, Succinct circuit representations and leaf language classes are basically the same concept, Inform. Process. Lett., 59, 211, 10.1016/0020-0190(96)00096-8 Chandra, 1981, Alternation, J. ACM, 28, 114, 10.1145/322234.322243 Compton, 1990, A uniform method for proving lower bounds on the computational complexity of logical theories, Ann. Pure Appl. Logic, 48, 1, 10.1016/0168-0072(90)90080-L Courcelle, 1990, Graph rewriting: An algebraic and logic approach, 193 Courcelle, 1990, The monadic second-order logic of graphs. I. Recognizable sets of finite graphs, Inform. and Comput., 85, 12, 10.1016/0890-5401(90)90043-H Ebbinghaus, 1991 Engelfriet, 1997, Context-free graph grammars, 125 Fagin, 1974, Generalized first-order spectra and polynomial-time recognizable sets, 43 Feferman, 1959, The first order properties of products of algebraic systems, Fund. Math., 47, 57, 10.4064/fm-47-1-57-103 Feigenbaum, 1999, The complexity of problems on graphs represented as OBDDs, Chic. J. Theoret. Comput. Sci., 1999 Frick, 2001, Deciding first-order properties of locally tree-decomposable structures, J. ACM, 48, 1184, 10.1145/504794.504798 Frick, 2004, The complexity of first-order and monadic second-order logic revisited, Ann. Pure Appl. Logic, 130, 3, 10.1016/j.apal.2004.01.007 Gaifman, 1982, On local and nonlocal properties, 105 Galperin, 1983, Succinct representations of graphs, Information and Control, 56, 183, 10.1016/S0019-9958(83)80004-7 Göller, 2005, Fixpoint logics on hierarchical structures, vol. 3821, 483 Gottlob, 2004, Existential second-order logic over graphs: Charting the tractability frontier, J. ACM, 51, 312, 10.1145/972639.972646 Gottlob, 1999, Succinctness as a source of complexity in logical formalisms, Ann. Pure Appl. Logic, 97, 231, 10.1016/S0168-0072(98)00057-8 Habel, 1992, Hyperedge Replacement: Grammars and Languages, vol. 643 Immerman, 1988, Nondeterministic space is closed under complementation, SIAM J. Comput., 17, 935, 10.1137/0217058 Immerman, 1989, Expressibility and parallel complexity, SIAM J. Comput., 18, 625, 10.1137/0218043 Immerman, 1999 Ladner, 1977, Application of model theoretic games to discrete linear orders and finite automata, Inform. and Comput., 33, 281 Lengauer, 1989, Hierarchical planarity testing algorithms, J. ACM, 36, 474, 10.1145/65950.65952 Lengauer, 1992, The correlation between the complexities of the nonhierarchical and hierarchical versions of graph problems, J. Comput. System Sci., 44, 63, 10.1016/0022-0000(92)90004-3 Lengauer, 1988, Efficient solution of connectivity problems on hierarchically defined graphs, SIAM J. Comput., 17, 1063, 10.1137/0217068 Libkin, 2004 Lohrey, 2005, Model-checking hierarchical structures, 168 Lynch, 1982, Complexity classes and theories of finite models, Math. Systems Theory, 15, 127, 10.1007/BF01786976 Makowsky, 2004, Algorithmic aspects of the Feferman–Vaught theorem, Ann. Pure Appl. Logic, 126, 159, 10.1016/j.apal.2003.11.002 Makowsky, 1996, Arity and alternation in second-order logic, Ann. Pure Appl. Logic, 78, 189, 10.1016/0168-0072(95)00013-5 Marathe, 1994, The complexity of approximation PSPACE-complete problems for hierarchical specifications, Nordic J. Comput., 1, 275 Marathe, 1998, Approximation algorithms for PSPACE-hard hierarchically and periodically specified problems, SIAM J. Comput., 27, 1237, 10.1137/S0097539795285254 Marathe, 1997, Hierarchically specified unit disk graphs, Theoret. Comput. Sci., 174, 23, 10.1016/S0304-3975(96)00008-4 Markey, 2003, Model checking a path, vol. 2761, 248 Papadimitriou, 1994 Papadimitriou, 1986, A note on succinct representations of graphs, Information and Control, 71, 181, 10.1016/S0019-9958(86)80009-2 Savitch, 1970, Relationships between nondeterministic and deterministic tape complexities, J. Comput. System Sci., 4, 177, 10.1016/S0022-0000(70)80006-X Stirling, 2001 Stockmeyer, 1976, The polynomial-time hierarchy, Theoret. Comput. Sci., 3, 1, 10.1016/0304-3975(76)90061-X Straubing, 1994 Szelepcsényi, 1988, The method of forced enumeration for nondeterministic automata, Acta Inform., 26, 279, 10.1007/BF00299636 Thomas, 1997, Languages, automata, and logic, 389 Vardi, 1982, The complexity of relational query languages (extended abstract), 137 Vardi, 1995, On the complexity of bounded-variable queries, 266 Veith, 1997, Languages represented by Boolean formulas, Inform. Process. Lett., 63, 251, 10.1016/S0020-0190(97)00134-8 Veith, 1998, How to encode a logical structure by an OBDD, 122 Veith, 1998, Succinct representation, leaf languages, and projection reductions, Inform. and Comput., 142, 207, 10.1006/inco.1997.2696 Wrathall, 1976, Complete sets and the polynomial-time hierarchy, Theoret. Comput. Sci., 3, 23, 10.1016/0304-3975(76)90062-1