Monodic fragments of probabilistic first-order temporal logic with bounded semantics

We extend (type-2) probabilistic first-order logic with temporal operators, interpreted over fixed-length initial segments of (discrete) time. Given a formula φ of the resulting logic and a natural number N, we ask: is φ satisfiable over a space of length <i>N </i>+ 1 sequences of states (first-order structures)? We show the problem to be decidable for monodic fragments of the logic whose first-order part has a decidable satisfiability problem and we also establish the problem's computational complexity when the first-order part is among some well-known decidable fragments of first-order logic.