# Selected Papers of the 2004 IEEE Symposium on Logic in Computer Science

2004

Editors: Andrei Voronkov, Leonid Libkin

### 1. The succinctness of first-order logic on linear orders

Succinctness is a natural measure for comparing the strength of different logics. Intuitively, a logic L_1 is more succinct than another logic L_2 if all properties that can be expressed in L_2 can be expressed in L_1 by formulas of (approximately) the same size, but some properties can be expressed […]

### 2. Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds

Given a formula in quantifier-free Presburger arithmetic, if it has a satisfying solution, there is one whose size, measured in bits, is polynomially bounded in the size of the formula. In this paper, we consider a special class of quantifier-free Presburger formulas in which most linear constraints […]

### 3. Model Checking Probabilistic Pushdown Automata

We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model […]

### 4. Theories for TC0 and Other Small Complexity Classes

We present a general method for introducing finitely axiomatizable "minimal" two-sorted theories for various subclasses of P (problems solvable in polynomial time). The two sorts are natural numbers and finite sets of natural numbers. The latter are essentially the finite binary strings, […]

### 5. Automatic Structures: Richness and Limitations

We study the existence of automatic presentations for various algebraic structures. An automatic presentation of a structure is a description of the universe of the structure by a regular set of words, and the interpretation of the relations by synchronised automata. Our first topic concerns […]