What is Temporal Logic with Next Operator Called

Question

I am looking into a temporal logic whose only temporal operator is next (often denoted as a circle $\circ$). What is this called? Is it studied by some branch of modal logic? I am, of course, familiar with LTL and CTL but they are too expressive for my purposes.

Answer 1

While there may not be a logic directly designed this way, I would steer you in the direction of Mission-Time Temporal Logic (MLTL), which, much like Metric Temporal Logic (MTL), bounds the time over which an operator reasons. MTL operators have bounds that are either $\infty$ or the positive reals. MLTL limits this with finite, integer bounds. As you can imagine, this essentially means that every MLTL formula can easily be expressed in LTL with only next time operators. Consider the following examples:

\begin{matrix} MLTL & English & LTL\\ \mathcal{F}_{[0,5]} a = & \textrm{" } a \textrm{ occurs within 5 time steps from now"} & = a | \mathcal{X}a | \mathcal{XX}a | \mathcal{XXX}a|\mathcal{XXXX}a|\mathcal{XXXXX}a\\ \mathcal{G}_{[2,5]} a = & \textrm{" } a \textrm{ occurs cont. from 2 to 5 time steps in the future"} & = \mathcal{XX}a \wedge \mathcal{XXX}a \wedge \mathcal{XXXX}a \wedge \mathcal{XXXXX}a\\ \end{matrix}

Thus, it is similar to LTL, but definitely less expressive, as all properties are essentially safety.