Portal de Periódicos da CAPES

Branching-Time Model Checking of One-Counter Processes and Timed Automata

2013; Society for Industrial and Applied Mathematics; Volume: 42; Issue: 3 Linguagem: Inglês

10.1137/120876435

1095-7111

Stefan Göller, Markus Lohrey,

Logic, programming, and type systems

One-counter automata (OCA) are pushdown automata which operate only on a unary stack alphabet. We study the computational complexity of model checking computation tree logic (${\mathsf{CTL}}$) on transition systems induced by OCA. A ${\mathsf{PSPACE}}$ upper bound is inherited from the modal $\mu$-calculus for this problem proved by Serre. First, we analyze the periodic behavior of ${\mathsf{CTL}}$ over OCA 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. In particular, model checking fixed OCA against ${\mathsf{CTL}}$ formulas with a fixed leftward until depth is in $\mathsf{P}$. This generalizes a corresponding recent result of Göller, Mayr, and To for the expression complexity of ${\mathsf{CTL}}$'s fragment ${\mathsf{EF}}$. Second, we prove that already over some fixed OCA, ${\mathsf{CTL}}$ model checking is ${\mathsf{PSPACE}}$-hard, i.e., expression complexity is ${\mathsf{PSPACE}}$-hard. Third, we show that there already exists a fixed ${\mathsf{CTL}}$ formula for which model checking of OCA is ${\mathsf{PSPACE}}$-hard, i.e., data complexity is ${\mathsf{PSPACE}}$-hard as well. To obtain the latter result, we employ two results from complexity theory: (i) Converting a natural number in Chinese remainder presentation into binary presentation is in logspace-uniform ${\mathsf{NC}}^1$ and (ii) ${\mathsf{PSPACE}}$ is $\mathsf{AC}^0$-serializable. We demonstrate that our approach can be used to obtain further results. We show that model checking ${\mathsf{CTL}}$'s fragment ${\mathsf{EF}}$ over OCA is hard for $\mathsf{P}^{\mathsf{NP}}$, thus establishing a matching lower bound. Moreover, we show that the following problem is hard for ${\mathsf{PSPACE}}$: Given a one-counter Markov decision process, a set of target states with counter value zero each, and an initial state, to decide whether the probability that the initial state will eventually reach one of the target states is arbitrarily close to $1$. This improves a recently proved lower bound for every level of the boolean hierarchy shown by Brázdil et al. Finally, we prove that there is a fixed ${\mathsf{CTL}}$ formula for which model checking 2-clock timed automata is ${\mathsf{PSPACE}}$-hard, generalizing a ${\mathsf{PSPACE}}$-hardness result for the combined complexity by Laroussinie, Markey, and Schnoebelen.