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


Editors: Andrei Voronkov, Leonid Libkin

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

Grohe, Martin ; Schweikardt, Nicole.
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

Seshia, Sanjit A. ; Bryant, Randal E..
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

Esparza, Javier ; Kucera, Antonin ; Mayr, Richard.
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

Nguyen, Phuong ; Cook, Stephen.
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

Khoussainov, Bakhadyr ; Nies, Andre ; Rubin, Sasha ; Stephan, Frank.
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 […]