The number of quantifiers needed to express first-order (FO) properties is captured by two-player combinatorial games called multi-structural games. We analyze these games on binary strings with an ordering relation, using a technique we call parallel play, which significantly reduces the number of quantifiers needed in many cases. Ordered structures such as strings have historically been notoriously difficult to analyze in the context of these and similar games. Nevertheless, in this paper, we provide essentially tight bounds on the number of quantifiers needed to characterize different-sized subsets of strings. The results immediately give bounds on the number of quantifiers necessary to define several different classes of Boolean functions. One of our results is analogous to Lupanov’s upper bounds on circuit size and formula size in propositional logic: we show that every Boolean function on n-bit inputs can be defined by a FO sentence having (1+ε)n/log(n) + O(1) quantifiers, and that this is essentially tight. We reduce this number to (1 + ε)log(n) + O(1) when the Boolean function in question is sparse.

Multi-structural (MS) games are combinatorial games that capture the number of quantifiers of first-order sentences. On the face of their definition, MS games differ from Ehrenfeucht-Fraisse (EF) games in two ways: first, MS games are played on two sets of structures, while EF games are played on a pair of structures; second, in MS games, Duplicator can make any number of copies of structures. In the first part of this paper, we perform a finer analysis of MS games and develop a closer comparison of MS games with EF games. In particular, we point out that the use of sets of structures is of the essence and that when MS games are played on pairs of structures, they capture Boolean combinations of first-order sentences with a fixed number of quantifiers. After this, we focus on another important difference between MS games and EF games, namely, the necessity for Spoiler to play on top of a previous move in order to win some MS games. Via an analysis of the types realized during MS games, we delineate the expressive power of the variant of MS games in which Spoiler never plays on top of a previous move. In the second part we focus on simultaneously capturing number of quantifiers and number of variables in first-order logic. We show that natural variants of the MS game do *not* achieve this. We then introduce a new game, the quantifier-variable tree game, and show that it simultaneously captures the number of quantifiers and number of variables. We conclude by generalizing this game to a family of games, the *syntactic games*, that simultaneously capture reasonable syntactic measures and the number of variables.

Abstract Some of the most significant high-level properties of currencies are the sums of certain account balances. Properties of such sums can ensure the integrity of currencies and transactions. For example, the sum of balances should not be changed by a transfer operation. Currencies manipulated by code present a verification challenge to mathematically prove their integrity by reasoning about computer programs that operate over them, e.g., in Solidity. The ability to reason about sums is essential: even the simplest ERC-20 token standard of the Ethereum community provides a way to access the total supply of balances. Unfortunately, reasoning about code written against this interface is non-trivial: the number of addresses is unbounded, and establishing global invariants like the preservation of the sum of the balances by operations like transfer requires higher-order reasoning. In particular, automated reasoners do not provide ways to specify summations of arbitrary length. In this paper, we present a generalization of first-order logic which can express the unbounded sum of balances. We prove the decidablity of one of our extensions and the undecidability of a slightly richer one. We introduce first-order encodings to automate reasoning over software transitions with summations. We demonstrate the applicability of our results by using SMT solvers and first-order provers for validating the correctness of common transitions in smart contracts.

Quantified first-order formulas, often with quantifier alternations, are increasingly used in the verification of complex systems. While automated theorem provers for first-order logic are becoming more robust, invariant inference tools that handle quantifiers are currently restricted to purely universal formulas. We define and analyze first-order quantified separators and their application to inferring quantified invariants with alternations. A separator for a given set of positively and negatively labeled structures is a formula that is true on positive structures and false on negative structures. We investigate the problem of finding a separator from the class of formulas in prenex normal form with a bounded number of quantifiers and show this problem is NP-complete by reduction to and from SAT. We also give a practical separation algorithm, which we use to demonstrate the first invariant inference procedure able to infer invariants with quantifier alternations.

The resilience of a Boolean query on a database is the minimum number of tuples that need to be deleted from the input tables in order to make the query false. A solution to this problem immediately translates into a solution for the more widely known problem of deletion propagation with source-side effects. In this paper, we give several novel results on the hardness of the resilience problem for conjunctive queries with self-joins, and, more specifically, we present a dichotomy result for the class of single-self-join binary queries with exactly two repeated relations occurring in the query. Unlike in the self-join free case, the concept of triad is not enough to fully characterize the complexity of resilience. We identify new structural properties, namely chains, confluences and permutations, which lead to various NP-hardness results. We also give novel involved reductions to network flow to show certain cases are in P. Although restricted, our results provide important insights into the problem of self-joins that we hope can help solve the general case of all conjunctive queries with self-joins in the future.

This paper addresses the complexity of SAT-based invariant inference, a prominent approach to safety verification. We consider the problem of inferring an inductive invariant of polynomial length given a transition system and a safety property. We analyze the complexity of this problem in a black-box model, called the Hoare-query model, which is general enough to capture algorithms such as IC3/PDR and its variants. An algorithm in this model learns about the system's reachable states by querying the validity of Hoare triples. We show that in general an algorithm in the Hoare-query model requires an exponential number of queries. Our lower bound is information-theoretic and applies even to computationally unrestricted algorithms, showing that no choice of generalization from the partial information obtained in a polynomial number of Hoare queries can lead to an efficient invariant inference procedure in this class. We then show, for the first time, that by utilizing rich Hoare queries, as done in PDR, inference can be exponentially more efficient than approaches such as ICE learning, which only utilize inductiveness checks of candidates. We do so by constructing a class of transition systems for which a simple version of PDR with a single frame infers invariants in a polynomial number of queries, whereas every algorithm using only inductiveness checks and counterexamples requires an exponential number of queries. Our results also shed light on connections and differences with the classical theory of exact concept learning with queries, and imply that learning from counterexamples to induction is harder than classical exact learning from labeled examples. This demonstrates that the convergence rate of Counterexample-Guided Inductive Synthesis depends on the form of counterexamples.

We consider the problem of checking whether a proposed invariant $\varphi$ expressed in first-order logic with quantifier alternation is inductive, i.e. preserved by a piece of code. While the problem is undecidable, modern SMT solvers can sometimes solve it automatically. However, they employ powerful quantifier instantiation methods that may diverge, especially when $\varphi$ is not preserved. A notable difficulty arises due to counterexamples of infinite size. This paper studies Bounded-Horizon instantiation, a natural method for guaranteeing the termination of SMT solvers. The method bounds the depth of terms used in the quantifier instantiation process. We show that this method is surprisingly powerful for checking quantified invariants in uninterpreted domains. Furthermore, by producing partial models it can help the user diagnose the case when $\varphi$ is not inductive, especially when the underlying reason is the existence of infinite counterexamples. Our main technical result is that Bounded-Horizon is at least as powerful as instrumentation, which is a manual method to guarantee convergence of the solver by modifying the program so that it admits a purely universal invariant. We show that with a bound of 1 we can simulate a natural class of instrumentations, without the need to modify the code and in a fully automatic way. We also report on a prototype implementation on top of Z3, which we used to verify several examples by Bounded-Horizon of bound 1.

Induction is a successful approach for verification of hardware and software systems. A common practice is to model a system using logical formulas, and then use a decision procedure to verify that some logical formula is an inductive safety invariant for the system. A key ingredient in this approach is coming up with the inductive invariant, which is known as invariant inference. This is a major difficulty, and it is often left for humans or addressed by sound but incomplete abstract interpretation. This paper is motivated by the problem of inductive invariants in shape analysis and in distributed protocols. This paper approaches the general problem of inferring first-order inductive invariants by restricting the language L of candidate invariants. Notice that the problem of invariant inference in a restricted language L differs from the safety problem, since a system may be safe and still not have any inductive invariant in L that proves safety. Clearly, if L is finite (and if testing an inductive invariant is decidable), then inferring invariants in L is decidable. This paper presents some interesting cases when inferring inductive invariants in L is decidable even when L is an infinite language of universal formulas. Decidability is obtained by restricting L and defining a suitable well-quasi-order on the state space. We also present some undecidability results that show that our restrictions are necessary. We further present a framework for systematically constructing infinite languages while keeping the invariant inference problem decidable. We illustrate our approach by showing the decidability of inferring invariants for programs manipulating linked-lists, and for distributed protocols.

Software-defined networking (SDN) is a new paradigm for operating and managing computer networks. SDN enables logically-centralized control over network devices through a "controller" --- software that operates independently of the network hardware. Network operators can run both in-house and third-party SDN programs on top of the controller, e.g., to specify routing and access control policies.

Several research thrusts in the area of data management have focused on understanding how changes in the data affect the output of a view or standing query. Example applications are explaining query results, propagating updates through views, and anonymizing datasets. An important aspect of this analysis is the problem of deleting a minimum number of tuples from the input tables to make a given Boolean query false, which we refer to as " the resilience of a query. " In this paper, we study the complexity of resilience for self-join-free conjunctive queries with arbitrary functional dependencies. The cornerstone of our work is the novel concept of triads, a simple structural property of a query that leads to the several dichotomy results we show in this paper. The concepts of triads and resilience bridge the connections between the problems of deletion propagation and causal responsibility, and allow us to substantially advance the known complexity results in these topics. Specifically, we show a dichotomy for the complexity of resilience, which identifies previously unknown tractable families for deletion propagation with source side-effects, and we extend this result to account for functional dependencies. Further, we identify a mistake in a previous dichotomy for causal responsibility, and offer a revised characterization based purely on the structural form of the query (presence or absence of triads). Finally, we extend the dichotomy for causal responsibility in two ways: (a) we account for functional dependencies in the input tables, and (b) we compute responsibility for sets of tuples specified via wildcards.

First order logic with transitive closure, and separation logic enable elegant interactive verification of heap-manipulating programs. However, undecidabilty results and high asymptotic complexity of checking validity preclude complete automatic verification of such programs, even when loop invariants and procedure contracts are specified as formulas in these logics. This paper tackles the problem of procedure-modular verification of reachability properties of heap-manipulating programs using efficient decision procedures that are complete: that is, a SAT solver must generate a counterexample whenever a program does not satisfy its specification. By (a) requiring each procedure modifies a fixed set of heap partitions and creates a bounded amount of heap sharing, and (b) restricting program contracts and loop invariants to use only deterministic paths in the heap, we show that heap reachability updates can be described in a simple manner. The restrictions force program specifications and verification conditions to lie within a fragment of first-order logic with transitive closure that is reducible to effectively propositional logic, and hence facilitate sound, complete and efficient verification. We implemented a tool atop Z3 and report on preliminary experiments that establish the correctness of several programs that manipulate linked data structures.

Pattern queries are widely used in complex event processing (CEP) systems. Existing pattern matching techniques, however, can provide only limited performance for expensive queries in real-world applications, which may involve Kleene closure patterns, flexible event selection strategies, and events with imprecise timestamps. To support these expensive queries with high performance, we begin our study by analyzing the complexity of pattern queries, with a focus on the fundamental understanding of which features make pattern queries more expressive and at the same time more computationally expensive. This analysis allows us to identify performance bottlenecks in processing those expensive queries, and provides key insights for us to develop a series of optimizations to mitigate those bottlenecks. Microbenchmark results show superior performance of our system for expensive pattern queries while most state-of-the-art systems suffer from poor performance. A thorough case study on Hadoop cluster monitoring further demonstrates the efficiency and effectiveness of our proposed techniques.

We consider a new class of planning problems involving a set of non-negative real variables, and a set of non-deterministic actions that increase or decrease the values of these variables by some arbitrary amount. The formulas specifying the initial state, goal state, or action preconditions can only assert whether certain variables are equal to zero or not. Assuming that the state of the variables is fully observable, we obtain two results. First, the solution to the problem can be expressed as a policy mapping qualitative states into actions, where a qualitative state includes a Boolean variable for each original variable, indicating whether its value is zero or not. Second, testing whether any such policy, that may express nested loops of actions, is a solution to the problem, can be determined in time that is polynomial in the qualitative state space, which is much smaller than the original infinite state space. We also report experimental results using a simple generate-and-test planner to illustrate these findings.

Given a high-level specification and a low-level programming language, our goal is to automatically synthesize an efficient program that meets the specification. In this paper, we present a new algorithmic methodology for inductive synthesis that allows us to do this.

We present the DeAL language for heap assertions that are efficiently evaluated during garbage collection time. DeAL is a rich, declarative, logic-based language whose programs are guaranteed to be executable with good whole-heap locality, i.e., within a single traversal over every live object on the heap and a finite neighborhood around each object. As a result, evaluating DeAL programs incurs negligible cost: for simple assertion checking at each garbage collection, the end-to-end execution slowdown is below 2%. DeAL is integrated into Java as a VM extension and we demonstrate its efficiency and expressiveness with several applications and properties from the past literature.

Large-scale event systems are becoming increasingly popular in a variety of domains. Event pattern evaluation plays a key role in monitoring applications in these domains. Existing work on pattern evaluation, however, assumes that the occurrence time of each event is known precisely and the events from various sources can be merged into a single stream with a total or partial order. We observe that in real-world applications event occurrence times are often unknown or imprecise. Therefore, we propose a temporal model that assigns a time interval to each event to represent all of its possible occurrence times and revisit pattern evaluation under this model. In particular, we propose the formal semantics of such pattern evaluation, two evaluation frameworks, and algorithms and optimizations in these frameworks. Our evaluation results using both real traces and synthetic systems show that the event-based framework always outperforms the point-based framework and with optimizations, it achieves high efficiency for a wide range of workloads tested.

Complex event patterns involving Kleene closure are finding application in a variety of stream environments for tracking and monitoring purposes. In this paper, we propose a compact language, SASE+, that can be used to define a wide variety of Kleene closure patterns, analyze the expressive power of the language, and outline an automata-based implementation for efficient Kleene closure evaluation over event streams.

Pattern matching over event streams is increasingly being employed in many areas including financial services, RFIDbased inventory management, click stream analysis, and electronic health systems. While regular expression matching is well studied, pattern matching over streams presents two new challenges: Languages for pattern matching over streams are significantly richer than languages for regular expression matching. Furthermore, efficient evaluation of these pattern queries over streams requires new algorithms and optimizations: the conventional wisdom for stream query processing (i.e., using selection-join-aggregation) is inadequate.

Nested words are a structured model of execution paths in procedural programs, reflecting their call and return nesting structure. Finite nested words also capture the structure of parse trees and other tree-structured data, such as XML. We provide new temporal logics for finite and infinite nested words, which are natural extensions of LTL, and prove that these logics are first-order expressively-complete. One of them is based on adding a "within" modality, evaluating a formula on a subword, to a logic CaRet previously studied in the context of verifying properties of recursive state machines (RSMs). The other logic, NWTL, is based on the notion of a summary path that uses both the linear and nesting structures. For NWTL we show that satisfiability is EXPTIME-complete, and that model-checking can be done in time polynomial in the size of the RSM model and exponential in the size of the NWTL formula (and is also EXPTIME-complete). Finally, we prove that first-order logic over nested words has the three-variable property, and we present a temporal logic for nested words which is complete for the two-variable fragment of first-order.

Nested words are a structured model of execution paths in procedural programs, reflecting their call and return nesting structure. Finite nested words also capture the structure of parse trees and other tree-structured data, such as XML. We provide new temporal logics for finite and infinite nested words, which are natural extensions of LTL, and prove that these logics are first-order expressively- complete. One of them is based on adding a "within" modality, evaluating a formula on a subword, to a logic CaRet previously studied in the context of verifying properties of recursive state machines. The other logic is based on the notion of a summary path that combines the linear and nesting structures. For that logic, both model-checking and satisfiability are shown to be EXPTIME-complete. Finally, we prove that first-order logic over nested words has the three-variable property, and we present a temporal logic for nested words which is complete for the two- variable fragment of first-order.

We introduce a new Ehrenfeucht--Fraïssé game for proving lower bounds on the size of first-order formulas. Up until now, such games have only been used to prove bounds on the operator depth of formulas, not their size. We use this game to prove that the CTL + formula, Occur n ≡ E[F p 1 ∧ F p 2 ∧ … ∧ F p n ], which says that there is a path along which the predicates p 1 through p n all occur, requires size n ! to express in CTL. Our lower bound is optimal. It follows that the succinctness of CTL + with respect to CTL is exactly Θ( n )!. Wilke had shown that the succinctness was at least exponential [Wilke 1999].We also use our games to prove an optimal Ω( n ) lower bound on the number of boolean variables needed for forward reachability logic (RL f ) to polynomially embed the language CTL + . The number of booleans needed for full reachability logic RL and the transitive closure logic FO 2 (TC) remain open [Immerman and Vardi 1997; Alechina and Immerman 2000].

We present the first complete problems for dynamic complexity classes including the classes Dyn-FO and Dyn-ThC/sup 0/, the dynamic classes corresponding to relational calculus and (polynomially bounded) SQL, respectively. The first problem we show complete for Dyn-FO is a single-step version of the circuit value problem (SSCV). Of independent interest, our construction also produces a first-order formula, /spl zeta/, that is in a sense universal for all first-order formulas. Since first-order formulas are stratified by quantifier depth, the first-order formula /spl zeta/ emulates formulas of greater depth by iterated application. As a corollary we obtain a fixed quantifier block, QBC, that is complete for all first-order quantifier blocks.

We introduce a new Ehrenfeucht-Fraisse game for proving lower bounds on the size of first-order formulas. Up until now such games have only been used to prove bounds on the operator depth of formulas, not their size. We use this game to prove that the CTL/sup +/ formula Occur/sub n//spl equiv/E[Fp/sub 1//spl and/Fp/sub 2//spl and//spl middot//spl middot//spl middot//spl and/F/sub n/] which says that there is a path along which the predicates p/sub 1/ through p/sub n/ occur in some order; requires size n! to express in CTL. Our lower bound is optimal. It follows that the succinctness of CTL+ with respect to CTL is exactly /spl Theta/(n). Wilke (1999) had shown that the succinctness was at least exponential. We also use our games to prove all optimal /spl Theta/(n) lower bound on the number of boolean variables needed for a weak reachability logic (/spl Rscr//spl Lscr//sup w/) to polynomially embed the language LTL. The number of booleans needed for full reachability logic RC and the transitive closure logic FO/sup 2/(TC) remain open (Immerman and Vardi, 1997; Alechina and Immerman, 2000).

A language L over an alphabet A is said to have a neutral letter if there is a letter e/spl isin/A such that inserting or deleting e's from any word in A* does not change its membership (or non-membership) in L. The presence of a neutral letter affects the definability of a language in first-order logic. It was conjectured that it renders all numerical predicates apart from the order predicate useless, i.e., that if a language L with a neutral letter is not definable in first-order logic with linear order then it is not definable in first-order. Logic with any set /spl Nscr/ of numerical predicates. We investigate this conjecture in detail, showing that it fails already for /spl Nscr/={+, *}, or possibly stronger for any set /spl Nscr/ that allows counting up to the m times iterated logarithm, 1g/sup (m)/, for any constant m. On the positive side, we prove the conjecture for the case of all monadic numerical predicates, for /spl Nscr/={+}, for the fragment BC(/spl Sigma/) of first-order logic, and for binary alphabets.

Abstract We prove that the set of properties describable by a uniform sequence of first-order sentences using at most k + 1 distinct variables is exactly equal to the set of properties checkable by a Turing machine in DSPACE[nk] (where n is the size of the universe). This set is also equal to the set of properties describable using an iterative definition for a finite set of relations of arity k. This is a refinement of the theorem PSPACE = VAR[O[1]] [8]. We suggest some directions for exploiting this result to derive trade-offs between the number of variables and the quantifier depth in descriptive complexity.

We show that for most complexity classes of interest, all sets complete under first-order projections (fops) are isomorphic under first-order isomorphisms. That is, a very restricted version of the Berman--Hartmanis conjecture holds. Since "natural" complete problems seem to stay complete via fops, this indicates that up to first-order isomorphism there is only one "natural" complete problem for each "nice" complexity class.

Fagin's theorem characterizes NP as the set of decision problems that are expressible as second-order existential sentences, i.e., in the form (/spl exist//spl Pi/)/spl phi/, where /spl Pi/ is a new predicate symbol, and /spl phi/ is first-order. In the presence of a successor relation, /spl phi/ may be assumed to be universal, i.e., /spl phi//spl equiv/(/spl forall/x~)/spl alpha/ where /spl alpha/ is quantifier-free. The PCP theorem characterizes NP as the set of problems that may be proved in a way that can be checked by probabilistic verifiers using O(log n) random bits and reading O(1) bits of the proof: NP=PCP[log n, 1]. Combining these theorems, we show that every problem D/spl isin/NP may be transformed in polynomial time to an algebraic version D/spl circ//spl isin/NP such that D/spl circ/ consists of the set of structures satisfying a second-order existential formula of the form (/spl exist//spl Pi/)(R/spl tilde/x~)/spl alpha/ where R/spl tilde/ is a majority quantifier-the dual of the R quantifier in the definition of RP-and /spl alpha/ is quantifier-free. This is a generalization of Fagin's theorem and is equivalent to the PCP theorem.

We prove that tree isomorphism is not expressible in the language (FO+TC+COUNT). This is surprising since in the presence of ordering the language captures NL, whereas tree isomorphism and canonization are in L (Lindell, 1992). Our proof uses an Ehrenfeucht-Fraisse game for transitive closure logic with counting. As a corresponding upper bound, we show that tree canonization is expressible in (FO+COUNT)[log n]. The best previous upper bound had been (FO+COUNT)[n/sup 0(1)/] (Dublish and Maheshwari, 1990). The lower bound remains true for bounded-degree trees, and we show that for bounded-degree trees counting is not needed in the upper bound. These results are the first separations of the unordered versions of the logical languages for NL, AC/sup 1/, and ThC/sup 1/. Our results were motivated by a conjecture in (Etessami and Immerman, 1995) that (FO+TC+COUNT+1LO)=NL, i.e., that a one-way local ordering sufficed to capture NL. We disprove this conjecture, but we prove that a two-way local ordering does suffice, i.e., (FO+TC+COUNT+2LO)=NL.

G. McColm (1990) conjectured that positive elementary inductions are bounded in a class K of finite structures if every (FO+LFP) formula is equivalent to a first-order formula in K. Here (FO+LFP) is the extension of first-order logic with the least fixed point operator. We disprove the conjecture. Our main results are two model-theoretic constructions, one deterministic and the other randomized, each of which refutes McColm's conjecture.>

Fagin (1974) proved that NP is equal to the set of problems expressible in second-order existential logic (SO/spl exist/). We consider problems that are NP-complete via first-order projections (fops). These low-level reductions are known to have nice properties, including the fact that every pair of problems that are NP-complete via fops are isomorphic via a first-order definable isomorphism (E. Allender et al., 1993). However, before this paper, fewer than five natural problems had actually been shown to be NP-complete via fops. We give a necessary and sufficient syntactic condition for an SO/spl exist/ formula to represent a problem that is NP-complete via fops. Using this condition we prove syntactically that 29 natural NP-complete problems remain complete via fops.>

Traditionally, computational complexity has considered only static problems. Classical Complexity Classes such as NC, P, NP, and PSPACE are defined in terms of the complexity of checking—upon presentation of an entire input—whether the input satisfies a certain property.

In this paper we characterise exactly the complexity of a set based database language called SRL, which presents a unified framework for queries and updates.By imposing simple synt act ic restrictions on it, we are able to express exactly the classes, P and L OGSPA CE.We also discuss the role of ordering in database query languages and show that the hom operator of Machiavelli language in [OBB89]does not capture all the order-independent properties.Complexity

It is shown that Omega (n) variables are needed for first-order logic with counting to identify graphs on n vertices. This settles a long-standing open problem. The lower bound remains true over a set of graphs of color class size 4. This contrasts sharply with the fact that three variables suffice to identify all graphs of color class size 3, and two variables suffice to identify almost all graphs. The lower bound is optimal up to multiplication by a constant because n variables obviously suffice to identify graphs on n vertices.>

A theory satisfies the k-variable property if every first-order formula is equivalent to a formula with at most k bound variables (possibly reused). Gabbay has shown that a model of temporal logic satisfies the k-variable property for some k if and only if there exists a finite basis for the temporal connectives over that model. We give a model-theoretic method for establishing the k-variable property, involving a restricted Ehrenfeucht-Fraisse game in which each player has only k pebbles. We use the method to unify and simplify results in the literature for linear orders. We also establish new k-variable properties for various theories of bounded-degree trees, and in each case obtain tight upper and lower bounds on k. This gives the first finite basis theorems for branching-time models of temporal logic. 1 Introduction A first-order theory \\Sigma satisfies the k-variable property if every first-order formula is equivalent under \\Sigma to a formula with at most k bound variables (pos...

It is shown that the time needed by a concurrent-read, concurrent-write parallel random access machine (CRAM) to check if an input has a certain property is the same as the minimal depth of a first-order inductive definition of the property. This in turn is equal to the number of “iterations” of a first-order sentence needed to express the property. The second contribution of this paper is the introduction of a purely syntactic uniformity notion for circuits. It is shown that an equivalent definition for the uniform circuit classes ${\text{AC}}^i ,i \geqslant 1$ is given by first-order sentences “iterated” $\log ^i n$ times. Similarly, uniform ${\text{AC}}^0 $ is defined to be the first-order expressible properties (which in turn is equal to constant time on a CRAM by our main theorem). A corollary of our main result is a new characterization of the Polynomial-Time Hierarchy (PH): PH is equal to the set of languages accepted by a CRAM using exponentially many processors and constant time.

In this paper we show that nondeterministic space $s(n)$ is closed under complementation for $s(n)$ greater than or equal to $\log n$. It immediately follows that the context-sensitive languages are closed under complementation, thus settling a question raised by Kuroda [Inform. and Control, 7 (1964), pp. 207–233].

We present a series of operators of apparently increasing power which when added to first-order logic produce a series of languages in which exactly the properties checkable in a certain complexity class may be expressed. We thus give alternate characterizations of most important complexity classes. We also introduce reductions appropriate for our setting: first-order translations, and a restricted, quantifier free version of these called projection translations. We show that projection translations are a uniform version of Valiant’s projections, and that the usual complete problems remain complete via these very restrictive reductions.

The main result of this note shows that there exist sparse sets in $NP$ that are not in $P$ if and only if NEXPTIME differs from EXPTIME. Several other results are derived about the complexity of very sparse sets in $NP-P$ and an interpretation of the meaning of these results is given in terms of the complexity of solving "individual instances" of problems in $NP-P$.

We present in this paper a series of languages adequate for expressing exactly those properties checkable in a series of computational complexity classes. For example, we show that a graph property is in polynomial time if and only if it is expressible in the language of first order graph theory together with a least fixed point operator. As another example, a group theoretic property is in the logspace hierarchy if and only if it is expressible in the language of first order group theory together with a transitive closure operator.

Query languages for relational databases have received considerable attention. In 1972 Codd [Cod72] showed that two natural mathematical languages for queries—one algebraic and the other a version of first order predicate calculus—had identical powers of expressibility. Query languages which are as expressive as Codd's Relational Calculus are sometimes called complete. This term is misleading, however, because many interesting queries are not expressible in “complete” languages.

We continue the study of first order expressibility as a measure of complexity, introducing the new class Var &Sz[v(n),z(n)] of languages expressible with v(n) variables in sentences of size z(n). We show that when the variables are restricted to boolean values: BVar &Sz[v(n),z(n)] = ASPACE&TIME[v(n),t(n)] That is variables and size correspond precisely to alternating space and time respectively. Returning to variables ranging over an n element universe, it follows that: Var[O(1)] = ASPACE[log n] = PTIME That is the family of properties uniformly expressible with a constant number of variables is just PTIME. These results hold for languages with an ordering on the objects in question, e.g. for graphs a successor relation on the vertices. We introduce an "alternating pebbling game" to prove lower bounds on the number of variables and size needed to express properties without successor. We show, for example, that k variables are needed to express Clique(k), suggesting that this problem requires DTIME[nk].

We introduce a new complexity measure, QR[f(n)], which clocks the size of formulas from predicate calculus needed to express a given property. Techniques from logic are used to prove sharp lower bounds in the measure. These results demonstrate space requirements for computations and may provide techniques for seperating Time and Space complexity classes because we show that: NSPACE[f(n)] ⊆ QR[(f(n))2/log(n)] ⊆ DSPACE[f(n)2].

One-way log-tape (1-L) reductions are mappings defined by log-tape Turing machines whose read head on the input can only move to the right. The 1-L reductions provide a more refined tool for studying the feasible complexity classes than the P-time [2,7] or log-tape [4] reductions. Although the 1-L computations are provably weaker than the feasible classes L, NL, P and NP, the known complete sets for those classes are complete under 1-L reductions. However, using known techniques of counting arguments and recursion theory we show that certain log-tape reductions cannot be 1-L and we construct sets that are complete under log-tape reductions but not under 1-L reductions.