Model checking FO(R) over one-counter processes and beyond

Abstract

One-counter processes are pushdown processes over a singleton stack alphabet (plus a stack-bottom symbol). We study the problems of model checking asynchronous products of one-counter processes against 1) first-order logic FO(R) with reachability predicate, 2) the finite variable fragments FO k (R) (k ≥ 2) of FO(R), 3) EF-logic which is a fragment of FO 2(R), and 4) all these logics extended with simple component-wise synchronizing predicates. We give a rather complete picture of their combined, expression, and data complexity. To this end, we show that these problems are poly-time reducible to two syntactic restrictions of Presburger Arithmetic, which are equi-expressive with first-order modulo counting theory of (