Branching-time Model Checking of One-counter Processes

Stefan GöLler & Markus Lohrey
One-counter processes (OCPs) are pushdown processes which operate only on a unary stack alphabet. We study the computational complexity of model checking computation tree logic ($\CTL$) over OCPs. A $\PSPACE$ upper bound is inherited from the modal $\mu$-calculus for this problem. First, we analyze the periodic behaviour of $\CTL$ over OCPs and derive a model checking algorithm whose running time is exponential only in the number of control locations and a syntactic notion of the...