Logical and schematic characterization of complexity classes (Q1323362)

We consider classes of well-known program schemes from a complexity theoretic viewpoint. We define logics which express all those problems solvable using our program schemes and show that the class of problems so solved or expressed coincides exactly with the complexity class of PSPACE (our problems are viewed as sets of finite structures over some vocabulary and, hence, they need not be encoded for input to our program schemes). We derive normal form theorems for our logics and use these normal form theorems to show that certain problems concerning acceptance and termination of our program schemes and satisfiability of our logical formulae are PSPACE-complete. Moreover, we show that a naturally-defined game problem, seemingly disjoint from logic and program schemes, is PSPACE-complete using the results described above. We also highlight similarities between the results of this paper and the literature, so providing the reader with an introduction to this area of research.