  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.
