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.
Document type :
Conference papers
Jean-Yves Marion and Thomas Schwentick. 27th International Symposium on Theoretical Aspects of Computer Science - STACS 2010, Mar 2010, Nancy, France. pp.405-416, 2010, Proceedings of the 27th Annual Symposium on the Theoretical Aspects of Computer Science
Liste complète des métadonnées


https://hal.inria.fr/inria-00455367
Contributor : Publications Loria <>
Submitted on : Wednesday, February 10, 2010 - 11:27:58 AM
Last modification on : Wednesday, February 10, 2010 - 11:40:33 AM
Document(s) archivé(s) le : Friday, June 18, 2010 - 7:54:30 PM

File

goeller.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00455367, version 1

Collections

Citation

Stefan Göller, Markus Lohrey. Branching-time model checking of one-counter processes. Jean-Yves Marion and Thomas Schwentick. 27th International Symposium on Theoretical Aspects of Computer Science - STACS 2010, Mar 2010, Nancy, France. pp.405-416, 2010, Proceedings of the 27th Annual Symposium on the Theoretical Aspects of Computer Science. <inria-00455367>

Share

Metrics

Record views

110

Document downloads

96