Synchronized CTL over One-Counter Automata

TL;DR

This paper investigates the decidability and complexity of model-checking a synchronized extension of CTL over one-counter automata, revealing non-elementary upper bounds and identifying a tractable fragment with exponential space complexity.

Contribution

It proves that model-checking CTL+Sync over OCAs is decidable with a non-elementary upper bound and identifies a fragment with EXPSPACE complexity.

Findings

Model-checking CTL+Sync over OCAs is decidable.

The problem has a non-elementary upper bound.

A fragment of CTL+Sync is in EXPSPACE.

Abstract

We consider the model-checking problem of Synchronized Computation-Tree Logic (CTL+Sync) over One-Counter Automata (OCAs). CTL+Sync augments CTL with temporal operators that require several paths to satisfy properties in a synchronous manner, e.g., the property "all paths should eventually see $p$ at the same time". The model-checking problem for CTL+Sync over finite-state Kripke structures was shown to be in $\mathsf{P}^{\mathsf{NP}^{\mathsf{NP}}}$. OCAs are labelled transition systems equipped with a non-negative counter that can be zero-tested. Thus, they induce infinite-state systems whose computation trees are not regular. The model-checking problem for CTL over OCAs was shown to be $\mathsf{PSPACE}$-complete. We show that the model-checking problem for CTL+Sync over OCAs is decidable. However, the upper bound we give is non-elementary. We therefore proceed to study the problem for a central fragment of CTL+Sync, extending CTL with operators that require all paths to satisfy properties in a synchronous manner, and show that it is in $\mathsf{EXP}^\mathsf{NEXP}$ (and in particular in $\mathsf{EXPSPACE}$), by exhibiting a certain "segmented periodicity" in the computation trees of OCAs.