Göller, Stefan ;
Lohrey, Markus
Branchingtime Model Checking of Onecounter Processes
Abstract
Onecounter 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 logspaceuniform $\NC^1$ and (ii) $\PSPACE$ is $\AC^0$serializable. We demonstrate that our approach can be used to answer further open questions.
BibTeX  Entry
@InProceedings{gller_et_al:LIPIcs:2010:2472,
author = {Stefan G{\"o}ller and Markus Lohrey},
title = {{Branchingtime Model Checking of Onecounter Processes}},
booktitle = {27th International Symposium on Theoretical Aspects of Computer Science},
pages = {405416},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897163},
ISSN = {18688969},
year = {2010},
volume = {5},
editor = {JeanYves Marion and Thomas Schwentick},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2010/2472},
URN = {urn:nbn:de:0030drops24722},
doi = {10.4230/LIPIcs.STACS.2010.2472},
annote = {Keywords: Model checking, computation tree logic, complexity theory}
}
2010
Keywords: 

Model checking, computation tree logic, complexity theory 
Seminar: 

27th International Symposium on Theoretical Aspects of Computer Science

Issue date: 

2010 
Date of publication: 

2010 