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...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.