Monadic Quantifiers Recognized by Deterministic Pushdown Automata

Abstract

I characterize the class of type 1 quantifiers (or, equivalently, type 11 quantifiers satisfying Conservativity and Extension) that are recognized by deterministic pushdown automata in terms of the associated semilinear sets of vectors in N2. These semilinear sets are nite unions of linear sets with at most two generators each, which are taken from a common three-element set of the form (k0) (0 l) (mn) . This answers a question that was left open by Mostowski (1998). A consequence of my characterization is that the type 1 quantifiers recognized by deterministic pushdown automata are already recognized by deterministic one-counter machines with zero tests, i.e., deterministic pushdown automata whose stack alphabet contains just one symbol (besides the bottom-of-stack symbol).