There is a misconception in comparing these three logics.
The temporal logic in both TLA+ and LTL is linear. TLA+ includes set theory, and the axioms of TLA+ are based on Zermelo-Fraenkel set theory. TLA+ syntactically enforces stutter-invariance (for ensuring that refinement is practical). LTL is a propositional logic.
CTL is drastically different from LTL, because CTL is a branching time logic, whereas LTL a linear time logic. A single sequence is a model for a linear-time formula. In contrast, a tree is a model for a branching-time formula. A sequence represents a single execution, whereas a tree represents many executions, that start at some state.
Path quantification is available in CTL, whereas absent from LTL. There's a common subset of LTL and CTL, but they are incomparable (= some properties are expressible in LTL only, others in CTL only). CTL* is their common superset.
For the application that you sketch, linear-time semantics appears more suitable. I would recommend using TLA+, because it offers a good discipline for describing systems, and is temporally sufficiently expressive that you probably won't need LTL (the other way around: if you can't specify the system with a stutter-invariant formula in TLA+, then it's more likely that the system needs revision, rather than the full expressive power of LTL being necessary).
The TLA+ book is a very readable introduction.