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 FOk (R) (k ≥ 2) of FO(R), 3) EF-logic which is a fragment of FO2 (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 (N, <), for which we give optimal quantifier elimination procedures. In particular, these problems are all shown to be in PSPACE, which is in sharp contrast to the closely related problem of model checking FO(R) over pushdown processes (with one stack) which...

• Type: Conference
• Year: 2009
• Where: CSL
• Authors: Anthony Widjaja To
• Keywords: Artificial Intelligence, CSL 2009, Model Checking, One-counter Processes, Pushdown Processes