Computer Science – Logic in Computer Science
Scientific paper
2009-12-21
Computer Science
Logic in Computer Science
Scientific paper
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.
Göller Stefan
Lohrey Markus
No associations
LandOfFree
Branching-time model checking of one-counter processes does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Branching-time model checking of one-counter processes, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Branching-time model checking of one-counter processes will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-302147