  We consider temporal logic verification of (possibly nonlinear) dynamical
systems evolving over continuous state spaces. Our approach combines
automata-based verification and the use of so-called barrier certificates.
Automata-based verification allows the decomposition the verification task into
a finite collection of simpler constraints over the continuous state space. The
satisfaction of these constraints in turn can be (potentially conservatively)
proved by appropriately constructed barrier certificates. As a result, our
approach, together with optimization-based search for barrier certificates,
allows computational verification of dynamical systems against temporal logic
properties while avoiding explicit abstractions of the dynamics as commonly
done in literature.
