  Barrier certificates, serving as differential invariants that witness system
safety, play a crucial role in the verification of cyber-physical systems
(CPS). Prevailing computational methods for synthesizing barrier certificates
are based on semidefinite programming (SDP) by exploiting Putinar
Positivstellensatz. Consequently, these approaches are limited by the
Archimedean condition, which requires all variables to be bounded, i.e.,
systems are defined over bounded domains. For systems over unbounded domains,
unfortunately, existing methods become incomplete and may fail to identify
potential barrier certificates.
  In this paper, we address this limitation for the unbounded cases. We first
give a complete characterization of polynomial barrier certificates by using
homogenization, a recent technique in the optimization community to reduce an
unbounded optimization problem to a bounded one. Furthermore, motivated by this
formulation, we introduce the definition of homogenized systems and propose a
complete characterization of a family of non-polynomial barrier certificates
with more expressive power. Experimental results demonstrate that our two
approaches are more effective while maintaining a comparable level of
efficiency.
