Branching-time model checking of one-counter processes

TL;DR

This paper investigates the computational complexity of model checking CTL over one-counter processes, revealing both tractable cases and PSPACE-hardness results, thereby advancing understanding of verification limits for these models.

Contribution

It provides a detailed complexity analysis of CTL model checking on OCPs, including algorithms for fixed formulas and control locations, and establishes PSPACE-hardness results for general cases.

Findings

Model checking fixed OCPs with fixed formulas is in P.

CTL model checking over some fixed OCP is PSPACE-hard.

Existence of a fixed CTL formula making model checking PSPACE-hard.

Abstract

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 formula that we call leftward until depth. Thus, model checking fixed OCPs against CTL formulas with a fixed leftward until depth is in P. This generalizes a result of the first author, Mayr, and To for the expression complexity of CTL's fragment EF. Second, we prove that already over some fixed OCP, CTL model checking is PSPACE-hard. Third, we show that there already exists a fixed CTL formula for which model checking of OCPs is PSPACE-hard. For the latter, we employ two results from complexity theory: (i) Converting a natural number in Chinese remainder presentation into binary presentation is in logspace-uniform NC^1 and (ii) PSPACE is AC^0-serializable. We demonstrate that our approach can be used to answer further open questions.