  Verification of temporal logic properties plays a crucial role in proving the
desired behaviors of hybrid systems. In this paper, we propose an interval
method for verifying the properties described by a bounded linear temporal
logic. We relax the problem to allow outputting an inconclusive result when
verification process cannot succeed with a prescribed precision, and present an
efficient and rigorous monitoring algorithm that demonstrates that the problem
is decidable. This algorithm performs a forward simulation of a hybrid
automaton, detects a set of time intervals in which the atomic propositions
hold, and validates the property by propagating the time intervals. A
continuous state at a certain time computed in each step is enclosed by an
interval vector that is proven to contain a unique solution. In the
experiments, we show that the proposed method provides a useful tool for formal
analysis of nonlinear and complex hybrid systems.
