On Pebble Automata for Data Languages with Decidable Emptiness Problem

TL;DR

This paper introduces top view weak pebble automata, a subclass with decidable emptiness, and demonstrates their robustness and expressive power for certain data languages, including those expressible in LTL with freeze quantifiers.

Contribution

The paper defines top view weak pebble automata, proves their decidable emptiness, and shows their equivalence across deterministic, nondeterministic, and alternating variants, extending their expressive power.

Findings

Decidability of emptiness for top view weak PA.

Equivalence of deterministic, nondeterministic, and alternating top view weak PA.

Expressiveness includes all data languages in LTL with freeze quantifiers.

Abstract

In this paper we study a subclass of pebble automata (PA) for data languages for which the emptiness problem is decidable. Namely, we introduce the so-called top view weak PA. Roughly speaking, top view weak PA are weak PA where the equality test is performed only between the data values seen by the two most recently placed pebbles. The emptiness problem for this model is decidable. We also show that it is robust: alternating, nondeterministic and deterministic top view weak PA have the same recognition power. Moreover, this model is strong enough to accept all data languages expressible in Linear Temporal Logic with the future-time operators, augmented with one register freeze quantifier.