  This paper concerns the verification of continuous-time polynomial spline
trajectories against linear temporal logic specifications (LTL without 'next').
Each atomic proposition is assumed to represent a state space region described
by a multivariate polynomial inequality. The proposed approach is based on
sampling the trajectories in a manner that captures all region transitions, to
yield a discrete word called a trace, which is amenable to established formal
methods for path checking. The continuous-time trajectory is shown to satisfy
the specification if and only if the trace does. General topological conditions
on the sample points are derived that ensure a trace is recorded for arbitrary
continuous paths, given arbitrary region descriptions. Using techniques from
computer algebra, a trace generation algorithm is developed to satisfy these
conditions when the path and region boundaries are defined by polynomials. The
proposed PolyTrace algorithm has polynomial complexity in the number of atomic
propositions, and is guaranteed to produce a trace of any polynomial path. Its
performance is demonstrated via numerical simulations.
