Model Checking FO(R) over One-Counter Processes and beyond

10 years 10 days ago
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...
Anthony Widjaja To
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where CSL
Authors Anthony Widjaja To
Comments (0)