Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · cs/0703079

Automata with Nested Pebbles Capture First-Order Logic with Transitive Closure

Joost Engelfriet·Hendrik Jan Hoogeboom
View original source ↗Read source document ↗Export metadata ↓

Abstract

String languages recognizable in (deterministic) log-space are characterized either by two-way (deterministic) multi-head automata, or following Immerman, by first-order logic with (deterministic) transitive closure. Here we elaborate this result, and match the number of heads to the arity of the transitive closure. More precisely, first-order logic with k-ary deterministic transitive closure has the same power as deterministic automata walking on their input with k heads, additionally using a finite set of nested pebbles. This result is valid for strings, ordered trees, and in general for families of graphs having a fixed automaton that can be used to traverse the nodes of each of the graphs in the family. Other examples of such families are grids, toruses, and rectangular mazes. For nondeterministic automata, the logic is restricted to positive occurrences of transitive closure. The special case of k=1 for trees, shows that single-head deterministic tree-walking automata with nested pebbles are characterized by first-order logic with unary deterministic transitive closure. This refines our earlier result that placed these automata between first-order and monadic second-order logic on trees.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Joost Engelfriet, Hendrik Jan Hoogeboom. 2007-04-26. Automata with Nested Pebbles Capture First-Order Logic with Transitive Closure. https://doi.org/10.2168/lmcs-3(2%3A3)2007

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

The Yoneda embedding in simplicial type theory

Riehl and Shulman introduced simplicial type theory (STT), a variant of homotopy type theory which aimed to study not just homotopy theory, but its fusion with category theory: $(\infty,1)$-category theory. While notoriously technical, manipulating $\infty$-categories in simplicial type theory is often easier than working with ordinary categories, with the type theory handling infinite stacks of coherences in the background. We capitalize on recent work by Gratzer et al. defining the $(\infty,1)$-category of $\infty$-groupoids in STT to define presheaf categories within STT and systematically develop their theory. In particular, we construct the Yoneda embedding, prove the universal property of presheaf categories, refine the theory of adjunctions in STT, introduce the theory of Kan extensions, and prove Quillen's Theorem A.

cs.LO↗
arXiv2026

The Program Logic of Abstract Interpretation

Hoare-style program logics and abstract interpretation are two of the principal frameworks for reasoning about programs, and their affinity has long been recognised informally: both derive over-approximate judgements about program behaviour by structural, syntax-directed reasoning. Turning this analogy into a formal correspondence runs into two challenges. First, the disjunction (or join) rule, sound and admissible in Hoare logic, becomes unsound over non-additive abstract semantics. Second, the extrapolation operators that make abstract interpretation effective on unbounded computations, i.e. widening and narrowing, have no analogue in the derivations of existing program logics. We introduce APPL (Abstract Program Property Logic), a Hoare-style program logic that provides a proof-theoretic foundation for abstract interpretation while addressing both challenges. The key technical idea is density: abstract semantics is additive over dense families of logical assertions. This leads to a density-guarded join rule that enables sound disjunctive reasoning over arbitrary abstract domains. We also internalise the application of widening and narrowing through inference rules for iterative commands. As a result, an entire analysis by abstract interpretation can be viewed as a logical derivation in APPL. The logic is sound over any abstract domain and, when the assertion language is expressive enough, it is also relatively complete. Finally, by interpreting nondeterminism through a monoidal operator, APPL provides a single logical framework that uniformly subsumes Hoare logic, incorrectness logic, and Hoare-style logics for hyperproperties, thereby enabling their abstraction. Remarkably, the density-guarded join rule introduced to handle non-additive abstract semantics is also fundamental in guaranteeing completeness for hyperproperties.

cs.LO↗
arXiv2026

Optimal Probabilistic Answer Set Programming: Complexity and Implementations

Probabilistic Answer Set Programming (PASP) extends Answer Set Programming with the possibility of representing uncertain data. Among the possible available semantics, we focus here on the credal semantics. In this setting, prior work has focused exclusively on plain ASP programs, i.e., programs without optimization constructs. However, many real world tasks define optimality criteria over the possible solutions, which cannot be conveniently modeled with existing probabilistic ASP frameworks. In this paper, we close this gap and propose optimal Probabilistic Answer Set Programming, which extends PASP by also allowing weak constraints, which are the standard optimization construct of ASP. We define the semantics of such programs, study the computational complexity of the inference and most probable explanation tasks, and propose practical implementations based on Algebraic Model Counting and Answer Set Programming with Quantifiers. An empirical evaluation of the proposed approach on three real world tasks confirms the applicability of our framework.

cs.LO↗