Skip to Main content Skip to Navigation
Conference papers

Branching-time model checking of one-counter processes

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.
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Wednesday, February 10, 2010 - 11:27:58 AM
Last modification on : Wednesday, February 10, 2010 - 11:40:33 AM
Long-term archiving on: : Friday, June 18, 2010 - 7:54:30 PM


Files produced by the author(s)


  • HAL Id : inria-00455367, version 1



Stefan Göller, Markus Lohrey. Branching-time model checking of one-counter processes. 27th International Symposium on Theoretical Aspects of Computer Science - STACS 2010, Inria Nancy Grand Est & Loria, Mar 2010, Nancy, France. pp.405-416. ⟨inria-00455367⟩



Record views


Files downloads