Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard

The entailment between separation logic formulæ with inductive predicates, also known as sym- bolic heaps, has been shown to be decidable for a large class of inductive definitions [7]. Recently, a 2-EXPTIME algorithm was proposed [10, 14] and an EXPTIME-hard bound was established in [8]; however no precise lower bound is known. In this paper, we show that deciding entailment between predicate atoms is 2-EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines [5].

Alternating Turing machines and the analytical hierarchy

We use notions originating in Computational Complexity to provide insight into the analogies between computational complexity and Higher Recursion Theory. We consider alternating Turing machines, but with a modified, global, definition of acceptance. We show that a language is accepted by such a machine iff it is Pi-1-1. Moreover, total alternating machines, which either accept or reject each input, accept precisely the hyper-arithmetical (Delta-1-1) languages. Also, bounding the permissible number of alternations we obtain a characterization of the levels of the arithmetical hierarchy..The novelty of these characterizations lies primarily in the use of finite computing devices, with finitary, discrete, computation steps. We thereby elucidate the correspondence between the polynomial-time and the arithmetical hierarchies, as well as that between the computably-enumerable, the inductive (Pi-1-1), and the PSpace languages.

PDL with intersection and converse: satisfiability and infinite-state model checking

We study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this paper are that (i) satisfiability is in 2ΕΧΡΤΙΜΕ, thus 2ΕΧΡΤΙΜΕ-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2ΕΧΡΤΙΜΕ-complete. Both upper bounds are obtained by polynomial time computable reductions to ω-regular tree satisfiability in ICPDL, a reasoning problem that we introduce specifically for this purpose. This problem is then reduced to the emptiness problem for alternating two-way automata on infinite trees. Our approach to (i) also provides a shorter and more elegant proof of Danecki's difficult result that satisfiability in IPDL is in 2ΕΧΡΤΙΜΕ. We prove the lower bound(s) for infinite-state model checking using an encoding of alternating Turing machines.

WIRELESS MOBILE COMPUTING AND ITS LINKS TO DESCRIPTIVE COMPLEXITY

The Wireless Parallel Turing Machine (WPTM) is a new computational model recently introduced and studied by the authors. Its design captures important features of wireless mobile computing. In this paper we survey some results related to the descriptive complexity aspects of the new model. In particular, we show a tight relationship about (a) wireless parallel computing, (b) alternating, and (c) synchronized alternating Turing machines. This relationship opens, e.g., the road to circuit complexity by offering an elegant WPTM characterization of bounded-fan-in uniform circuit families, such as NC and NCi. The structural properties of computational graphs of WPTM computations inspire definitions of new complexity measures capturing important aspects of wireless computations: energy consumption and the number of broadcasting channels used during computation. These measures do not seem to have direct counterparts in alternating computations. We mention results related to these new structural measures, e.g., a polynomial time–bounded complexity hierarchy based on channel complexity, lying between P and PSPACE which seems to be incomparable to the standard polynomial–time alternating hierarchy.

TESTING THE DESCRIPTIONAL POWER OF SMALL TURING MACHINES ON NONREGULAR LANGUAGE ACCEPTANCE

We study lower bounds on space and input head reversals for deterministic, nondeterministic, and alternating Turing machines accepting nonregular languages. Three notions of space, namely strong, middle, weak are considered, and another notion, called accept, is introduced. In all cases, we obtain tight lower bounds. Moreover, we show that, while for determinism and nondeterminism such lower bounds are optimal even with respect to unary languages, for alternation optimal lower bounds for unary languages turn out to be strictly higher than those for languages over alphabets with two or more symbols.